author = {Günther Mayrhofer},
title = {{Symbolic Computation Prover with Induction}},
language = {english},
abstract = {An important task in automated theorem proving is computing with "arbitrary but fixed" constants. This kind of highschool proving occurs in the main part of most proofs. The current master's thesis presents an automated prover that focuses on such computations with symbols. The prover uses equalities and equivalences in the knowledge base to rewrite a goal formula. In all formulae there may be universal quantifiers and some selected logical connectives. Special syntax elements support case distinctions and sequence variables. The prover uses a specialized method for proving equalities and an important feature is proving by cases. An extension allows induction over some predefined domains. Additionally to the prover implementation in Mathematica, there is a tracer that prints a protocol of the proof flow. Since the code for this tracer is separated from the prover, there may be more than one tracer with different output. But more important is that a user can inspect the code of prover without being confused by technical details for generating some nice output. The main motivation for this prover is a new extension of the Theorema system. The aim is an environment for defining new prover in the same language as theorems. The advantage is clear, existing prover may prove facts of a new one, for example the correctness. Using this it is possible to build up a hierarchy of formally checked provers. For such reasoning about reasoners a starting point needs induction on the structure of terms and formulae. A first prover in the hierarchy will need computations with symbols in many proof branches. This may be done by the current Symbolic Computation Prover.},
year = {2009},
month = {September},
translation = {0},
school = {Johannes Kepler University},
sponsor = {SFB 013 of FWF Austrian Science Fund},
length = {100}