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

Related Items (9)

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

This page was built for publication: Inductive theorem proving based on tree grammars