# leanTAP Revisited Again

2022-09-22, updated 2022-09-29 next - previous

Another sequent calculus Prolog prover for classical propositional logic, based on Fitting’s paper .

The prover below is an optimized 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 . Its performances are generally better than leanseq’s.

A - Prolog Code:

D - Examples of Queries:

1. Excluded Middle: a | ~ a
2. Dilemma : ((~ a => b) & (a => b)) => b
3. Double Negation: ~(~a) <=> a
4. Peirce’s Law: ((a => b) => a) => a
5. Dummett Formula : (a => b)| (b => a)
6. Classical equivalence for negation : (~a => a) <=> a
7. Classical De Morgan's Law : ~((a & b)) => (~ a | ~b)
8. Pelletier Problem 17 : ( ( ( p & ( q => r ) ) => s ) <=> ( ( ~ p | q | s ) & ( ~ p | ~ r | s ) ) )
9. "Vacuous discharge" : ((a => b) & (a => b) & (a => b)) => (c => c)
10. Contrapositive : ((a => b) <=> (~ b => ~ a))
11. a
12. a => b
13. (a | b) => (a & b)
14. a & b | a & ~b | ~a & b | ~a & ~c
1.
Fitting, M. leanTAP Revisited. Journal of Logic and Computation, 1998, 8(1), 33–47, [Online]. Available: https://www.researchgate.net/publication/2240690_leanTAP_revisited.
2.
Beckert, B., Posegga, J. leanTAP: Lean Tableau-based Deduction. Journal of Automated Reasoning, 1997, 15, doi: 10.1007/BF00881804.

Made with Emacs 29.0.50 (Org mode 9.5) and with org-export-head, a blog exporter.

The css file of this blog is mainly the result of Zhitao Gong's work.