KtSeqC: A theorem prover for the minimal tense logic Kt.

INDEX: what is KtSeqC? papers source code contact address links


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


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


INDEX: what is KtSeqC? papers source code contact address links

Maintainer: rpg@arp.anu.edu.au