KtSeqC: A theorem prover for the minimal tense logic Kt.
What is KtSeqC?
KtSeqC is a theorem prover for the tense logic Kt, which makes use of the
simplfication optimisation. It was developed by
under the supervision of
A system description can be found
Papers on the calculus of KtSeqC
- KtSeqC is based upon the calculus KtSeq described in
A Labelled Sequent System for Tense Logic Kt. by
Nicolette Bonnette and Rajeev Goré, in
AI98: Proceedings of the Australian Joint Conference on Artificial
Intelligence, LNAI, 12 pages, Springer, 1998, to appear.
Source Code for KtSeqC
KtSeqC is written in C and uses yacc and lex/flex. A gzipped tar file
can be found here. The
syntax used is from the 1998 Tableaux
Questions, suggestions, or comments can be directed to:
Computer Sciences Laboratory
Australian National University
Canberra, ACT, 0200, AUSTRALIA
Phone: +61 6 279 8603
Fax: +61 6 279 8645
Links to Related Pages
- ModLeanTAP: A lean
free-variable tableau-based prover for propositional modal logics.
- leanTAP: A lean tableau-based prover for first-order logic.
- ileanTAP: A lean tableau-based prover for intuitionistic first-order logic (developed by Jens Otten at TH Darmstadt).
- The Logics Workbench
(LWB) develobed at the University of Berne.