Integer induction in saturation

DOI10.1007/978-3-030-79876-5_21MaRDI QIDQ2055871zbMATH OpenOpenAlexFDO

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

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

Cited in

(11)

• Inductive benchmarks for automated reasoning
• Induction in saturation-based proof search
• Induced saturation number
• scientific article; zbMATH DE number 3895067 (Why is no real title available?)
• Getting saturated with induction
• Lemmaless induction in trace logic
• Learning conjecturing from scratch
• Rewriting and inductive reasoning
• A mathematical benchmark for inductive theorem provers
• Synthesis of recursive programs in saturation
• Induction in saturation

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)