Softwares I developed...
- 1. CTL-RP
-
CTL-RP stands for Computation Tree Logic Resolution Prover.
Computation Tree Logic (CTL) is a branching-time temporal logic. CTL-RP is a
resolution based theorem prover for CTL, which utilises a first-order theorem prover, SPASS, as a core engine for inference.
Linux platform
- Version 00.21 (15 Apr 2011)
Two optimization rules for normal form transformation, namely "GroupDisjunctions" and "GroupAGs", are implemented. - Version 00.13 (20 Jan 2010)
- Version 00.08 (08 Dec 2008)
- Version 00.06 (07 Nov 2008)
- Download all (including examples)
- Version 00.21 (15 Apr 2011)
- 2. XA
- An efficient theorem prover for a fragment of PLTL and is able to efficiently check the emptiness of Buchi automata.
