=ADD=
=reftype=
14
=number=
99-19
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1999/99-19.ps.gz
=year=
1999
=month=
07
=author=
Kossak; Felix
=title=
An Interface for Interactive Proving with the Mathematical Software System Theorema
=abstract=
The Theorema project develops an integrated mathematical software
system with special focus on a natural-style language with clear
semantics and support for proving. Based on the existing automated
proving power, we developed an interface for interactive proving.

We describe the combination of automated and interactive proving in detail,
including the changes we had to make to the existing automated system. The only
difference in the proof function call is the setting of an additional option
'Interaction' with three possible values for interactive, semi-interactive and
fully-automated mode.

Two main windows give a survey over the current proof situation, the
initial proof situation, and the past proof steps. Special input
windows are created if required. The user has control over the
knowledge base and is able to determine each proof step by selecting
formulae and available inference rules. Additional input may be given,
for instance, in the form of terms for substituting variables.

In addition to the technical details, we demonstrate the use of the interactive
proving environment with examples.
=note=
Master Thesis, Polytechnical University of Upper Austria, Department for Software Engineering, A-4232 Hagenberg, Austria
=sponsor=
Austrian Science Fundation (FWF) - project FO-1302 (FB).
=keywords=
interactive proving, proof training, automated proving, ATP