publication . Article . 2017

Mechanically certifying formula-based Noetherian induction reasoning

Sorin Stratulat;
Open Access English
  • Published: 01 Jan 2017
  • Publisher: HAL CCSD
  • Country: France
Abstract
International audience; In first-order logic, the formula-based instances of the Noetherian induction principle allow to perform effectively simultaneous, mutual and lazy induction reasoning. Compared to the term- based Noetherian induction instances, they are not directly supported by the current proof assistants.We provide general formal tools for certifying formula-based Noetherian induction proofs by the Coq proof assistant, then show how to apply them to certify proofs of conjectures about conditional specifications, built with: i) a reductive rewrite-based induction system, and ii) a reductive-free cyclic induction system. The generation of reductive proof...
Subjects
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Coq, proof certification, Noetherian induction, cyclic induction proofs, implicit induction proofs, SPIKE, [ INFO.INFO-SC ] Computer Science [cs]/Symbolic Computation [cs.SC], [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], Induction system, Automated theorem proving, Proof assistant, Algebra, Mathematics, Noetherian, Structural induction, Mathematical proof

Alouini, I., Bouhoula, A., 1997. Un langage de stratégie pour SPIKE. Working document.

Aoto, T., 2006. Dealing with non-orientable equations in rewriting induction. In: Pfenning, F. (Ed.), RTA. Vol. 4098 of Lecture Notes in Computer Science. Springer, pp. 242-256. [OpenAIRE]

Abstract
International audience; In first-order logic, the formula-based instances of the Noetherian induction principle allow to perform effectively simultaneous, mutual and lazy induction reasoning. Compared to the term- based Noetherian induction instances, they are not directly supported by the current proof assistants.We provide general formal tools for certifying formula-based Noetherian induction proofs by the Coq proof assistant, then show how to apply them to certify proofs of conjectures about conditional specifications, built with: i) a reductive rewrite-based induction system, and ii) a reductive-free cyclic induction system. The generation of reductive proof...
Subjects
ACM Computing Classification System: TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGESTheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
free text keywords: Coq, proof certification, Noetherian induction, cyclic induction proofs, implicit induction proofs, SPIKE, [ INFO.INFO-SC ] Computer Science [cs]/Symbolic Computation [cs.SC], [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], Induction system, Automated theorem proving, Proof assistant, Algebra, Mathematics, Noetherian, Structural induction, Mathematical proof

Alouini, I., Bouhoula, A., 1997. Un langage de stratégie pour SPIKE. Working document.

Aoto, T., 2006. Dealing with non-orientable equations in rewriting induction. In: Pfenning, F. (Ed.), RTA. Vol. 4098 of Lecture Notes in Computer Science. Springer, pp. 242-256. [OpenAIRE]

Any information missing or wrong?Report an Issue