ACL2 Seminar
October 10, 2012

CP Wirth, Univ. des Saarlands and King's College London

Title:

Descente infinie, weakened admissibility conditions for
recursive functions, and the automated theorem prover
QUODLIBET

Abstract:
The automated induction theorem proving system
QUODLIBET was under development by a very small group
of researchers from 1992 to 2007.

I would like to lead an open exchange of ideas on some
aspects of this system that may be relevant beyond it,
namely its weak admissibility conditions and its
free-variable calculus for descente infinie (aka lazy
induction-hypotheses generation).  The very weak
admissibility conditions for recursive function
definitions, including partiality by both irreduciblity
and non-termination, turned out to be most helpful in
the verification of the implementation of syntactical
path orderings.  Compared to a reductive free-variable
sequent calculus, the descente infinie calculus has
inference steps that can apply sequents as lemmas or as
induction hypotheses.

When a Boyer-Moore-like recursion analysis is executed,
the merging of conflicting schemata can be overcome by
descente infinie.  When a mathematical theorem is to be
proved whose induction ordering has nothing to do with
the termination orderings of its recursive functions,
interaction becomes a lot simpler by descente infinie.