On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs

DOI10.1007/978-3-030-99461-7_15OpenAlexW4285212090MaRDI QIDQ2163179

Shujun Zhang, Naoki Nishida

Publication date: 10 August 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-99461-7_15

zbMATH Keywords

sequent calculusterm rewritinginductive theorem provingcyclic proofrewriting induction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Unnamed Item
• Sufficient completeness verification for conditional and constrained TRS
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
• Automated theorem proving by test set induction
• Automating induction for solving Horn clauses
• Operational semantics of resolution and productivity in Horn clause logic
• Term Rewriting with Logical Constraints
• Term Rewriting and All That
• The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
• One-Path Reachability Logic
• Verifying Procedural Programs via Constrained Rewriting Induction
• AC Dependency Pairs Revisited
• Ground Confluence Prover based on Rewriting Induction
• Automated Reasoning with Analytic Tableaux and Related Methods

This page was built for publication: On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs