Making theory reasoning simpler

DOI10.1007/978-3-030-72013-1_9MaRDI QIDQ2233504zbMATH OpenOpenAlexFDO

Authors Giles Reger, Johannes Schoisswohl, Andrei Voronkov

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-030-72013-1_9

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Unification with abstraction and theory instantiation in saturation-based reasoning
• Induction for SMT solvers
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Coming to terms with quantified reasoning
• Theory Instantiation

Cites work

• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
• Computing small clause normal forms
• Hierarchic superposition with weak abstraction
• Integrating Linear Arithmetic into Superposition Calculus
• Layered clause selection for theory reasoning (short paper)
• On deciding satisfiability by theorem proving with speculative inferences
• Refutational theorem proving for hierarchic first-order theories
• Rewriting
• Selecting the selection
• Superposition modulo linear arithmetic SUP(LA)
• Theory Instantiation
• Unification with abstraction and theory instantiation in saturation-based reasoning

Cited in

(6)

• Coming to terms with quantified reasoning
• Fully reusing clause deduction algorithm based on standard contradiction separation rule
• Lemmaless induction in trace logic
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Integer induction in saturation
• The 11th IJCAR automated theorem proving system competition – CASC-J11

Describes a project that uses

Uses Software

• VAMPIRE
• SMT-LIB
• z3

This page was built for publication: Making theory reasoning simpler

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