leanTAP Revisited Again
Another sequent calculus Prolog prover for classical propositional logic, based on Fitting’s paper .
The prover below is an improved version of the Prolog implementation of dirseq, that is the sequent calculus defined by Fitting when he revisited leanTAP, the prolog prover for First-Order Logic published by Beckert and Posegga . The Prolog code below (that is a prover online thanks to Tau Prolog) is an improvement of Fitting’s: for example, it provides a proof of Pelletier Problem 71 (file SYN007+1.014.p of ILTP Problems Library) and running with SWI Prolog, it gets the following statistics:
% 11,845,618 inferences, 1.268 CPU in 1.268 seconds (100% CPU, 9343626 Lips)
In comparison, leanseq prover published here proves the same formula with 54,890,489 inferences, 4.558 CPU in 4.561 seconds (100% CPU, 12042963 Lips). Therefore, this version of leanTAP can be considered as a very efficient Prolog prover for classical propositional logic.
It would be interesting to explain why this algorithm implemented in this order in Prolog is so efficient.
To be continued …
A - Prolog Code:
D - Examples of Queries:
- Excluded Middle: a | ~ a
- Dilemma : ((~ a => b) & (a => b)) => b
- Double Negation: ~(~a) <=> a
- Peirce’s Law: ((a => b) => a) => a
- Dummett Formula : (a => b)| (b => a)
- Classical equivalence for negation : (~a => a) <=> a
- Classical De Morgan's Law : ~((a & b)) => (~ a | ~b)
- Pelletier Problem 17 : ( ( ( p & ( q => r ) ) => s ) <=> ( ( ~ p | q | s ) & ( ~ p | ~ r | s ) ) )
- a => b
- (a | b) => (a & b)
- a & b | a & ~b | ~a & b | ~a & ~c