Tutorial for Tableaux 2013Lecturer: Sorin Stratulat (LITA, Univ. de Lorraine) DescriptionNoetherian induction is a powerful mathematical principle that allows to reason on Noetherian posets of unbounded number of elements. In firstorder logic, we can distinguish two instantiations of it, depending on the kind of elements we are reasoning on: (vectors of) terms or (firstorder) formulas.The termbased 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. Widelyspread among proof assistants, they can be easily integrated into sequentbased 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 formulabased induction proof techniques are issued from the Musser’s inductionless induction (or proof by consistency) method based on the KnuthBendix 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 cyclebased induction method that generalizes and keeps the best features of the term and formulabased induction methods. The application of any IH involved in a cyclic reasoning is validated by a cycle of formulas governed by a formulabased induction ordering. The induction reasoning is local (at cycle level), reductivefree, and performs efficiently mutual and lazy induction. From a theoretical point of view, the method synthesizes the overall usage of Noetherian induction reasoning in firstorder 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:
