Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs

DOI10.1007/s10472-023-09832-7OpenAlexW4321092854MaRDI QIDQ6059221

Sorin Stratulat

Publication date: 2 November 2023

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10472-023-09832-7

zbMATH Keywords

automated reasoningCoqproof certificationcyclic inductionE-\textsc{Cyclist}first-order logic with inductive definitions

Mathematics Subject Classification ID

Computing methodologies and applications (68U99) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07) Software, source code, etc. for problems pertaining to computer science (68-04)

Cites Work

• Unnamed Item
• Unnamed Item
• Mechanically certifying formula-based Noetherian induction reasoning
• Isabelle/HOL. A proof assistant for higher-order logic
• Cyclic proofs with ordering constraints
• Untersuchungen über das logische Schliessen. I
• Sequent calculi for induction and infinite descent
• Certification of Automated Termination Proofs
• Büchi Complementation and Size-Change Termination
• Term Rewriting and All That
• Descente Infinie + Deduction
• The size-change principle for program termination

This page was built for publication: Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs