author = {Viktoria Langenreither},
title = {{A Saturation-Based Automated Theorem Prover for RISCAL}},
language = {english},
abstract = {The aim of this thesis is to integrate a automated theorem prover for first-order logic with equality in the RISC theorem proving (RISCTP) software. The software currently already provides a built-in first-order prover. The MESON prover (model-elimination, subgoaloriented) follows a goal oriented approach. The idea is to provide a different procedure (knowledge-based) to further extend the functionality of RISCTP, since different prove designs lead to a fast proof search for different examples. One way to achieve this is by using the saturation principle, i. e. the prover generates from a set of first-order clauses in a systematic way all logical consequences until a refutation (empty clause) is found. In this thesis we give a throughout theoretical representation of different techniques for first-order provers, based on a comprehensive literature research. In accordance to this, we developed the design of our prover. As most state of the art provers, it is based of the give-clause-algorithm using the DISCOUNT loop to organize the proof search. The inference system is based on a variation of the superposition calculus, using the so-called pure superposition for the equality reasoning (all literals represent equalities). To further extend this prover an interface to an external SMT solver is integrated as well as axioms encoding the special theories of integers and arrays. The implementation of this prover is done as an extension of the RISCTP software using the Java programming language. To evaluate the prover, we used examples that were already defined for evaluating the MESON prover.},
year = {2025},
month = {December},
note = {Also available as RISC report no. 25-11},
translation = {0},
school = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria},
keywords = {automated reasoning, formal methods, program verification},
length = {108},
url = {https://doi.org/10.35011/risc.25-11},
type = {mathesis}