Tutorial for Tableaux 2013 

Lecturer: Sorin Stratulat (LITA, Univ. de Lorraine)


Noetherian induction is a powerful mathematical principle that allows to reason on Noetherian posets of unbounded number of elements. In first-order logic, we can distinguish two instantiations of it, depending on the kind of elements we are reasoning on: (vectors of) terms or (first-order) formulas.

The term-based principles rely on schemas that may attach a set of formulas as induction hypotheses (IHs) to another formula, called induction conclusion, with the intention that the IHs should be used in the proof of the induction conclusion. Widely-spread among proof assistants, they can be easily integrated into sequent-based inference systems as separate inference rules. The induction reasoning is local, at schema level, and the induction orderings may change for different schemas. On the downside, the IHs should be defined (sometimes long) before their use and some IHs may happen to not be applied. Moreover, the mutual induction with other formulas from the proof is not managed conveniently.

Most of the formula-based induction proof techniques are issued from the Musser’s inductionless induction (or proof by consistency) method based on the Knuth-Bendix completion algorithm. The reasoning is lazy and allows the mutual induction in a direct way. On the other hand, the proof methods are reductive, i.e. when processing a formula in a proof, the newly derived formulas  should be smaller (and sometimes equal), at ground level, w.r.t. an induction ordering uniquely defined for the whole proof.

Noetherian induction also allows for effective cyclic reasoning. We proposed a cycle-based induction method that generalizes and keeps the best features of the term- and formula-based induction methods. The application of any IH involved in a cyclic reasoning is validated by a cycle of formulas governed by a formula-based induction ordering. The induction reasoning is local (at cycle level), reductive-free, and performs efficiently mutual and lazy induction. From a theoretical point of view, the method synthesizes the overall usage of Noetherian induction reasoning in first-order logic. From a practical point of view, it allows for less restrictive specifications, more efficient implementations and proof certification processes.


The following topics will be discussed:
  • An overview of term- and formula-based Noetherian induction principles and proof methods.
  • A methodology for building modular and sound reductive inference systems. Application: the SPIKE theorem prover
  • A certification method for formula-based induction proofs. Application: certifying SPIKE proofs by Coq.
  • The description of the new cycle-based induction method. Converting cyclic proofs into sequent-based proofs and their certification.