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
Related Organizations
Download fromView all 3 versions
INRIA a CCSD electronic archive server
Article . 2017
Provider: INRIA a CCSD electronic archive server
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]
Related research
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
Related Organizations
Download fromView all 3 versions
INRIA a CCSD electronic archive server
Article . 2017
Provider: INRIA a CCSD electronic archive server
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]
Related research
Powered by OpenAIRE Research GraphAny information missing or wrong?Report an Issue
publication . Article . 2017
Mechanically certifying formula-based Noetherian induction reasoning
Sorin Stratulat;