Mechanical certification of \(\mathrm{FOL_{ID}}\) cyclic proofs
From MaRDI portal
Publication:6059221
DOI10.1007/s10472-023-09832-7OpenAlexW4321092854MaRDI QIDQ6059221
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
automated reasoningCoqproof certificationcyclic inductionE-\textsc{Cyclist}first-order logic with inductive definitions
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