This is an implementation of a tableau theorem prover for propositional logic in the C programming language. The program is able to parse propositional formulas and construct a tableau with the formula at the root which works by manipulating and analysing its syntax in order to find out whether there is something that can falsify it. Given a formula, the tableau will tell us whether or not it is satisfiable.
- Parsing propositional logic formulas.
- Determining whether a propositional formula is satisfiable or not.
- Determining whether a propositional formula is valid or not.
prop ::= p | q | r | x | y | w
fm ::= prop | -fm | (fm v fm) | (fm > fm) | (fm ^ fm)
- is for logical negation (NOT)
v is for logical disjunction (OR)
> is for logical implication (IMPLIES)
^ is for logical conjunction (AND)
Given a valuation λ : prop → {T, ꓕ} which extends to a truth-function satisfying:
We say that:
- Φ is valid if λ(Φ) = T for all possible valuations λ
- Φ is satisfiable if λ(Φ) = T for at least one valuation λ
- Φ is valid if and only if ¬Φ is unsatisfiable
- A literal is a proposition or its negation (e.g. p, ¬p)
- A theory Σ is a set of propositional formulas
- If p,¬p ∈ Σ then the theory is contradictory, write C(Σ)
- If each formula in Σ is a literal then the theory is fully expanded, write Exp(Σ)
- A tableau is a list of theories.
The algorithm is sound (if Φ is satisfiable then its tableau will never close) and complete (if Φ is not satisfiable then its tableau will close) and is guaranteed to terminate in at most 2|Φ| steps.
- Parser and tableau algorithm for first-order logic (not guaranteed to terminate but is sound and complete).
- Parser and tableau algorithm for modal logic.