# 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 [1].

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 [2]. Its performances are generally better
than
leanseq’s.

**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 ) ) )
- "Vacuous discharge" : ((a => b) & (a => b) & (a => b)) => (c => c)
- Contrapositive : ((a => b) <=> (~ b => ~ a))
- a
- a => b
- (a | b) => (a & b)
- a & b | a & ~b | ~a & b | ~a & ~c

## 1. References

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.