Theorem Provers Based on Tableau Systems
Theorem provers based on the Analytic Tableaux
- LOTREC
- In construction…
Theorem provers based on the KE System
- KEMS
- WDTP - Wagner Dias Tableau Prover (page in Portuguese)
- leanKE
- J. V. Pitt and R. J. Cunningham. Theorem Proving and Model Building with the Calculus KE. Journal of the IGPL, 4(1):129–150, 1996
- Alternative link: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.2054
Interactive proof assistants based on the KE System
- WinKE
- WinKE is an interactive proof assistant based on the KE calculus, a refutation system which combines features from Smullyan's analytic tableaux and Gentzen's natural deduction. The software has been designed to serve as a tutoring system to support the teaching of logic and reasoning on an introductory level.
- MacKE
Variations of KE
- □KE:
- Paper descibing the system: Jeremy Pitt. Benchmark Evaluation of □KE. Automated Reasoning with Analytic Tableaux and Related Methods. 1998
- MLSS-KE
- Paper descibing the system: Experimental comparison of two tableau-based decision procedures for MLSS
page revision: 15, last edited: 18 Feb 2010 19:32