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

• 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

(11)

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

Describes a project that uses

Uses Software

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

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)