Automated Reasoning

Mathesis provides simple solvers (reasoners, provers) based on truth table method and on tableau method.

Reasoning in propositional logic

Solvers based on truth table method

See Truth tables.

Solvers based on tableau method

mathesis.solvers.ClassicalSolver is a solver for classical propositional logic based on tableau method.

from mathesis.grammars import BasicGrammar
from mathesis.solvers import ClassicalSolver

grammar = BasicGrammar()

fml = grammar.parse("((A → B)∧(A → C)) → (A → (B∧C))")
sol = ClassicalSolver().solve([], [fml])

print(sol.htree())
print(f"Valid: {sol.is_valid()}")

¬(((A→B)∧(A→C))→(A→(B∧C))) 1
└── (A→B)∧(A→C) 2
    └── ¬(A→(B∧C)) 3
        └── A→B 4
            └── A→C 5
                └── A 6
                    └── ¬(B∧C) 7
                        ├── ¬A 8 ×
                        └── B 9
                            ├── ¬A 10 ×
                            └── C 11
                                ├── ¬B 12 ×
                                └── ¬C 13 ×

Valid: True