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