Making theory reasoning simpler

DOI10.1007/978-3-030-72013-1_9zbMath1474.68060OpenAlexW3131612531MaRDI QIDQ2233504

Johannes Schoisswohl, Andrei Voronkov, Giles Reger

Publication date: 18 October 2021

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)

Related Items (3)

The 11th IJCAR automated theorem proving system competition – CASC-J11 ⋮ Lemmaless induction in trace logic ⋮ Integer induction in saturation

Uses Software

• VAMPIRE
• SMT-LIB
• z3

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• On deciding satisfiability by theorem proving with speculative inferences
• Refutational theorem proving for hierarchic first-order theories
• Layered clause selection for theory reasoning (short paper)
• Unification with abstraction and theory instantiation in saturation-based reasoning
• Selecting the Selection
• Integrating Linear Arithmetic into Superposition Calculus
• Superposition Modulo Linear Arithmetic SUP(LA)
• Hierarchic Superposition with Weak Abstraction
• Theory Instantiation
• A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic

This page was built for publication: Making theory reasoning simpler