Tutorial: Noetherian Induction for First-Order Reasoning


Lecturer: Dr S. Stratulat

Tutorial Description

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 [1] 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.

Topics

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.

The tutorial page can be accessed at https://sites.google.com/site/tutorialtableaux2013.

[1] S. Stratulat. A unified view of induction reasoning for first-order logic. In Andrei Voronkov, editor, Turing-100 (The Alan Turing Centenary Conference), volume 10 of EPiC Series, pages 326–352. EasyChair, 2012.

Région Lorraine Grand Nancy