Integer induction in saturation

DOI10.1007/978-3-030-79876-5_21OpenAlexW3166201525MaRDI QIDQ2055871FDOQ2055871

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Zeno: An Automated Prover for Properties of Recursive Data Structures
• Induction for SMT Solvers
• Automating Inductive Proofs Using Theory Exploration
• AVATAR: The Architecture for First-Order Theorem Provers
• Theorem Proving in Higher Order Logics
• Superposition with structural induction
• TIP: Tons of Inductive Problems
• Coming to terms with quantified reasoning
• Induction with generalization in superposition reasoning
• Making theory reasoning simpler
• Induction in saturation-based proof search
• The Imandra Automated Reasoning System (System Description)

Cited In (5)

• Induced saturation number
• Lemmaless induction in trace logic
• Inductive benchmarks for automated reasoning
• Title not available (Why is that?)
• Getting saturated with induction

Uses Software

• VAMPIRE
• SMT-LIB
• z3
• Zeno
• CVC4
• AVATAR
• Imandra

This page was built for publication: Integer induction in saturation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2055871)