# 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
Vijay Boyapati
under the supervision of
Rajeev
Goré.
A system description can be found
here.

## 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
Prover Comparison.

## Contact Address

Questions, suggestions, or comments can be directed to:

Rajeev
Goré

Computer Sciences Laboratory

Australian National University

Canberra, ACT, 0200, AUSTRALIA

Email: Rajeev.Gore@arp.anu.edu.au

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.

Maintainer: *rpg@arp.anu.edu.au*

*
*