Automated theorem solver using sympy which also shows steps

theorem_solver_with_steps.py

from sympy import symbols, Implies, And, Not, simplify_logic, S
from itertools import combinations
from tqdm import tqdm


# Define the function to count nodes
def count_nodes(expr):
    """Recursively count all nodes in a SymPy expression."""
    count = 1
    if hasattr(expr, "args") and expr.args:
        count += sum(count_nodes(arg) for arg in expr.args)
    return count


def combine_expressions(knowledge_base):
    combined_results = []

    # Generate combinations of expressions from the knowledge base
    kb_combinations = list(combinations(knowledge_base, 2))
    for expr1, expr2 in tqdm(kb_combinations):
        combined_expr = simplify_logic(And(expr1, expr2))
        combined_expr = combined_expr.subs(expr1, True).subs(expr2, True)
        combined_results.append((expr1, expr2, combined_expr))

    # Sort the results by the number of nodes in the combined expression
    combined_results.sort(key=lambda terms: sum([count_nodes(term) for term in terms]))

    return combined_results


def prove_by_contradiction(premises, hypothesis):
    # Initialize knowledge base and lineage tracking
    knowledge_base = set(premises)
    lineage = {expr: ("knowledge base",) for expr in premises}

    # Step 1: Negate the hypothesis and add it to the knowledge base
    neg_hypothesis = Not(hypothesis)
    knowledge_base.add(neg_hypothesis)
    lineage[neg_hypothesis] = ("negated hypothesis",)

    # Start the proof process
    while True:
        new_knowledge_base = knowledge_base.copy()

        # Step 3: Pairwise combine knowledge base items using simplify_logic
        for expr1, expr2, combined_expr in combine_expressions(knowledge_base):
            # Check for contradiction (sympy's S.false)
            if combined_expr is S.false:
                # Trace back the lineage to the root
                return trace_lineage(lineage, expr1, expr2, combined_expr)

            if combined_expr not in new_knowledge_base:
                new_knowledge_base.add(combined_expr)
                lineage[combined_expr] = (expr1, expr2)

        # Update knowledge base if new expressions have been added
        if new_knowledge_base == knowledge_base:
            break  # Exit if no new knowledge is generated
        knowledge_base = new_knowledge_base

    return "No contradiction found, proof incomplete."


def trace_lineage(lineage, expr1, expr2, final_expr):
    output = []
    expr_index_map = {}
    index = 1

    # Recursively build lineage outputs
    def build_lineage(expr):
        nonlocal index
        if expr not in expr_index_map:
            if expr in lineage:
                if len(lineage[expr]) == 1:
                    # Base knowledge or hypothesis
                    output.append(f"{index}. {expr} [Using {lineage[expr][0]}]")
                else:
                    # Derived expressions
                    for pre_expr in lineage[expr]:
                        build_lineage(pre_expr)
                    origins = ", ".join(str(expr_index_map[e]) for e in lineage[expr])
                    output.append(f"{index}. {expr} [Using {origins}]")
            else:
                # Direct knowledge base entry
                output.append(f"{index}. {expr} [Using knowledge base]")
            expr_index_map[expr] = index
            index += 1

    build_lineage(expr1)
    build_lineage(expr2)
    final_step = (
        f"{index}. False [Using {expr_index_map[expr1]} and {expr_index_map[expr2]}]"
    )
    output.append(final_step)
    return "\n".join(output)


# Define your symbols and premises
X, Y, Z, W = symbols("X Y Z W")
premises = {X, Implies(X, Y), Implies(Y, Z), Implies(And(X, Z), W)}
hypothesis = And(X, W)

# Run the proof
proof_output = prove_by_contradiction(premises, hypothesis)
print(proof_output)