RISC JKU

The RISCTP Theorem Proving Interface

July 29, 2024: RISCTP 1.8.1 (minor changes and bug fixes with respect to problem decomposition)

The RISCTP theorem proving interface consists of a language for specifying proof problems and of an associated software for solving these problems. The RISCTP language is a typed variant of first-order logic whose level of abstraction is between that of higher level formal specification languages (such as the language of the RISCAL model checker) and lower level theorem proving languages (such as the language SMT-LIB supported by various satisfability modulo theories solvers and theorem provers such as Z3, cvc5, or Vampire). Thus the RISCTP language can serve as an intermediate layer that simplifies the connection of specification and verification systems to theorem provers; in fact, it was developed to equip the RISCAL model checker with theorem proving capabilities. The RISCTP software is implemented in Java with an API that enables the implementation of such connections; however, RISCTP also provides a text-based frontend and a web-based graphical user interface that allow its use as a theorem prover on its own. RISCTP provides a backend that translates a proving problem into SMT-LIB and solves it by the "black box" application of an external SMT solver. Furthermore, RISCTP implements an internal prover for first-order logic with equality and the possibility to inspect successful proofs as well as failed proof attempts. This prover also supports reasoning in the theories of integers, arrays, tuples, and algebraic datatypes, via a corresponding axiomatization, and/or the application of an external SMT solver.

   
Click to enlarge screenshots.

Download RISCTP
This includes all the files for running the software on 64-bit GNU/Linux x86 computers; for others, the appropriate versions of Z3, cvc5, Vampire, and ExSpec have to be downloaded and installed.
See the files README, CHANGES, and COPYING.
Manual [PDF]
This is the user documentation of the software.
Subversion Repository
This is a web interface to the Subversion repository that holds the source code of the program. The repository can be read anonymously by any Subversion client from the URL
svn://svn.risc.jku.at/schreine/RISCTP

Wolfgang Schreiner
Last modified: July 15, 2024