An Approach to Flexible Forms of Proof Control
for a First-Order Inductive Theorem Prover
(Extended Abstract)}


Ulrich Kuehler
Fachbereich Informatik, Universitaet Kaiserslautern
D-67663 Kaiserslautern
Germany
E-mail: kuehler@informatik.uni-kl.de

Abstract
We propose an approach to the problem of proof control
for our new first-order inductive theorem prover QuodLibet
that is characterized by a great deal of flexibility
w.r.t. the forms of proof control the prover supports.
The approach is based on so-called (proof) tactics,
i.e. proof control routines written in a special proof control
language named QML. QuodLibet provides a set of tactics
(in addition to the elementary inference rules), which range
from tactics for trivial simplification steps to tactics
representing comprehensive inductive proof strategies.
Moreover, QuodLibet allows new tactics that are written by the
user in QML to be integrated into the system to dynamically
extend its functionality.