Inductive theorem proving based on tree grammars

DOI10.1016/j.apal.2015.01.002zbMath1386.03018OpenAlexW2006510146MaRDI QIDQ2344621

Stefan Hetzl, Sebastian Eberhard

Publication date: 15 May 2015

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

Full work available at URL: https://doi.org/10.1016/j.apal.2015.01.002

zbMATH Keywords

proof theoryinductive theorem provingHerbrand's theoremautomated deduction

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) First-order arithmetic and fragments (03F30) Grammars and rewriting systems (68Q42) Structure of proofs (03F07) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

On the Herbrand content of LK, On the generation of quantified lemmas, Unnamed Item, Anti-unification and the theory of semirings, Higher-order pattern generalization modulo equational theories, Combining induction and saturation-based theorem proving, System Description: GAPT 2.0, THE HERBRAND FUNCTIONAL INTERPRETATION OF THE DOUBLE NEGATION SHIFT, Induction and Skolemization in saturation theorem proving

Uses Software

• ACL2
• TPTP
• Zeno
• HipSpec
• MiniMaxSat
• Cyclist
• IsaCoSy

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algorithmic introduction of quantified cuts
• Conjecture synthesis for inductive theories
• Rigid tree automata and applications
• Incorporating decision procedures in implicit induction.
• On the compressibility of finite languages and formal proofs
• Untersuchungen über das logische Schliessen. I
• Applying Tree Languages in Proof Theory
• Towards Algorithmic Cut-Introduction
• Zeno: An Automated Prover for Properties of Recursive Data Structures
• The TPTP World – Infrastructure for Automated Reasoning
• Sequent calculi for induction and infinite descent
• Introducing Quantified Cuts in Logic with Equality
• Rigid Tree Automata
• Herbrand-Confluence for Cut Elimination in Classical First Order Logic
• Term Rewriting and All That
• Automating Inductive Proofs Using Theory Exploration
• MINIMAL RECOGNIZERS AND SYNTACTIC MONOIDS OF DR TREE LANGUAGES
• Rippling: Meta-Level Guidance for Mathematical Reasoning
• Compressibility of Finite Languages by Grammars
• Herbrand Sequent Extraction