The RISCTP Theorem Proving Interface - Tutorial and Reference Manual (Version 1.0.*)

This report documents the RISCTP theorem proving interface. RISCTP 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 satisfiability modulo theories solvers such as Z3). 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 that allows its use as a theorem prover on its own. RISCTP already implements a backend that translates a proving problem into SMT-LIB and solves it by the "black box" application of Z3; in the future, RISCTP shall also provide built-in proving capabilities with greater transparency.