Integer induction in saturation
From MaRDI portal
Publication:2055871
DOI10.1007/978-3-030-79876-5_21OpenAlexW3166201525MaRDI QIDQ2055871
Petra Hozzová, Andrei Voronkov, Laura Kovács
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_21
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (3)
Inductive benchmarks for automated reasoning ⋮ Getting saturated with induction ⋮ Lemmaless induction in trace logic
Uses Software
Cites Work
- Superposition with structural induction
- Induction with generalization in superposition reasoning
- Making theory reasoning simpler
- Induction in saturation-based proof search
- Zeno: An Automated Prover for Properties of Recursive Data Structures
- AVATAR: The Architecture for First-Order Theorem Provers
- TIP: Tons of Inductive Problems
- Automating Inductive Proofs Using Theory Exploration
- The Imandra Automated Reasoning System (System Description)
- Induction for SMT Solvers
- Coming to terms with quantified reasoning
- Theorem Proving in Higher Order Logics
This page was built for publication: Integer induction in saturation
