Unprovability results for clause set cycles

DOI10.1016/j.tcs.2022.07.003OpenAlexW3203855288MaRDI QIDQ2084942

Stefan Hetzl, Jannik Vierling

Publication date: 14 October 2022

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2110.03246

zbMATH Keywords

cyclic proofsautomated inductive theorem provingweak arithmetical theories

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• VAMPIRE
• HipSpec
• Hipster
• AVATAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Mathematical induction in Otter-lambda
• Induction rules, reflection principles, and provably recursive functions
• Superposition with structural induction
• Parameter free induction and provably total computable functions
• Induction with generalization in superposition reasoning
• Combining induction and saturation-based theorem proving
• Induction in saturation-based proof search
• Induction rules in bounded arithmetic
• Herbrand analyses
• Combining Superposition and Induction: A Practical Realization
• AVATAR: The Architecture for First-Order Theorem Provers
• A note on parameter free Π₁ -induction and restricted exponentiation
• Open sentences and the induction axiom
• Reflection principles and provability algebras in formal arithmetic
• TIP: Tons of Inductive Problems
• On parameter free induction schemas
• Some observations on the logical foundations of inductive theorem proving
• Automating Inductive Proofs Using Theory Exploration
• Hipster: Integrating Theory Exploration in a Proof Assistant
• On n-quantifier induction
• Zusammenfassung von Mehreren Vollständigen Induktionen zu einer Einzigen

This page was built for publication: Unprovability results for clause set cycles