|
|
|
|
|
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 GUI 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.
svn://svn.risc.jku.at/schreine/RISCTP