Integer induction in saturation

DOI10.1007/978-3-030-79876-5_21MaRDI QIDQ2055871OpenAlexFDO

Authors Petra Hozzová, Laura Kovács, Andrei Voronkov

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)

Recommendations

• Getting saturated with induction
• Induction in saturation-based proof search
• Combining induction and saturation-based theorem proving
• Induction for SMT solvers

Cites work

• AVATAR: The Architecture for First-Order Theorem Provers
• Automating Inductive Proofs Using Theory Exploration
• Coming to terms with quantified reasoning
• Induction for SMT solvers
• Induction in saturation-based proof search
• Making theory reasoning simpler
• Superposition with structural induction
• TIP: tons of inductive problems
• The Imandra Automated Reasoning System (System Description)
• Theorem Proving in Higher Order Logics
• Zeno: an automated prover for properties of recursive data structures

Cited in

(6)

• scientific article; zbMATH DE number 3895067 (Why is no real title available?)
• Getting saturated with induction
• Lemmaless induction in trace logic
• Induction in saturation-based proof search
• Induced saturation number
• Inductive benchmarks for automated reasoning

Describes a project that uses

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)