=ADD=
=reftype=
14
=number=
98-14
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1998/98-14.ps.gz
=year=
1998
=month=
07
=author=
Tomuta; Elena
=title=
An Architecture for Combining Provers and its Applications in the Theorema System
=abstract=
This thesis is the result of the author's work in the Theorema project whose aim
is to build a system integrating Computer Algebra and Logic. One part of the
system is a mixed interactive-automated theorem prover which offers support to
mathematicians by generating automatically the "easy" parts of mathematical
proofs. When generating proofs the system imitates the way in which
mathematicians work.

Within this frame, we first investigate the problems appearing when proving
with functors. In order to do this 
we design and implement a simple language allowing the user of the Theorema
system to define functors and domains and to state properties involving them.
We design a functor prover which handles the constructs of the
functor language and we carry out experiments with concrete proofs generated
automatically. The functor prover is based on a combination of basic provers in
Theorema, each carrying out a special type of reasoning step: higher order
predicate logic, simplification with respect to a set of equalities, induction.

During the implementation of the prover and our experiments, several problems
appeared related to the way the basic provers interact and to how this
interaction can be adjusted easily to the type of problem at hand.
We design and implement a mechanism for provers' interaction which
includes a language for specifying strategies and interactio patterns during
proof search. This mechanism is now being used in Theorema also outside the
functor prover. It is based on known artificial intelligence date structures and
algorithms like AND-OR graphs but has several new features which were motivated
by the particular requests of Theorema.

This thesis is practice oriented and virtually all of the language constructs
and algorithms are implemented in Theorema. 
=keywords=
automatic reasoning
=note=
PhD Thesis
=sponsor=
Austrian Science Foundation (FWF), project FO-1302 (SFB).