Validating back-links of FOL_ID cyclic pre-proofs

MaRDI QIDQ3384901zbMATH OpenFDO

Authors Sorin Stratulat

Publication date 17 December 2021

Full work available at URL https://arxiv.org/abs/1810.07374, http://eptcs.web.cse.unsw.edu.au/paper.cgi?CLC2018.4

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• Automated Reasoning with Analytic Tableaux and Related Methods
• Cyclic proofs with ordering constraints
• Local validity for circular proofs in linear logic with fixed points
• A complete cyclic proof system for inductive entailments in first order logic
• Abstract cyclic proofs

Cites work

• Automated Reasoning with Analytic Tableaux and Related Methods
• Cyclic proofs with ordering constraints
• Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs
• Mechanically certifying formula-based Noetherian induction reasoning
• Sequent calculi for induction and infinite descent
• Weak alternating automata are not that weak

Cited in

(1)

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

This page was built for publication: Validating back-links of \(\mathrm{FOL_{ID}}\) cyclic pre-proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3384901)