Integer induction in saturation

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

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

Recommendations

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

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
• 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)