Induction and Skolemization in saturation theorem proving

DOI10.1016/j.apal.2022.103167OpenAlexW3160340332WikidataQ113880318 ScholiaQ113880318MaRDI QIDQ2084957

Stefan Hetzl, Jannik Vierling

Publication date: 14 October 2022

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

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

zbMATH Keywords

inductive theorem provingskolemizationweak arithmetical theoriessaturation theorem proving

Mathematics Subject Classification ID

Logic in computer science (03B70) First-order arithmetic and fragments (03F30) Nonstandard models of arithmetic (03H15) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• VAMPIRE
• HipSpec
• CVC4
• Hipster
• Cyclist
• InKa
• AVATAR

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Conjecture synthesis for inductive theories
• Rippling: A heuristic for guiding inductive proofs
• A compact representation of proofs
• Diophantine equations in fragments in arithmetic
• Superposition with structural induction
• Induction with generalization in superposition reasoning
• Combining induction and saturation-based theorem proving
• Induction in saturation-based proof search
• Induction rules in bounded arithmetic
• Inductive theorem proving based on tree grammars
• Combining Superposition and Induction: A Practical Realization
• On the complexity of proof deskolemization
• AVATAR: The Architecture for First-Order Theorem Provers
• Classical System of Martin-Löf’s Inductive Definitions Is Not Equivalent to Cyclic Proof System
• A note on parameter free Π₁ -induction and restricted exponentiation
• Open sentences and the induction axiom
• 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
• Induction for SMT Solvers
• Automated Reasoning with Analytic Tableaux and Related Methods
• Hipster: Integrating Theory Exploration in a Proof Assistant

This page was built for publication: Induction and Skolemization in saturation theorem proving