E-Matching in RISCTP
The RISCTP theorem proving interface consists of a language for specifying proof problems and of an associated software for solving these problems; it was developed to equip the RISCAL model checker with theorem proving capabilities. Apart from interfaces to external SMT solvers, RISCTP implements an internal prover for first-order logic which also supports equality reasoning based on paramodulation. The goal of this thesis is to extend this reasoning by utilizing the principles of "E-graphs" and "E-matching" that allow to find those terms in a proof problem whose values are equal to the value of a given term; thus we can more easily determine instantiations of quantified variables that are likely to be useful in the further proof. The literature on this topic is to be investigated and the corresponding algorithms are to be implemented (in the programming language Java).