TY - INPR
A1 - Kühler, Ulrich
T1 - An Approach to Flexible Forms of Proof Control for a First-Order Inductive Theorem Prover
N2 - 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.
Y1 - 1999
UR - https://kluedo.ub.uni-kl.de/frontdoor/index/index/docId/996
UR - https://nbn-resolving.org/urn:nbn:de:hbz:386-kluedo-9509
ER -