Making theory reasoning simpler
From MaRDI portal
Publication:2233504
DOI10.1007/978-3-030-72013-1_9zbMATH Open1474.68060OpenAlexW3131612531MaRDI QIDQ2233504FDOQ2233504
Authors: Giles Reger, Johannes Schoisswohl, Andrei Voronkov 
Publication date: 18 October 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-72013-1_9
Recommendations
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cites Work
- Title not available (Why is that?)
- Rewriting
- On deciding satisfiability by theorem proving with speculative inferences
- Theory Instantiation
- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic
- Computing small clause normal forms
- Superposition modulo linear arithmetic SUP(LA)
- Refutational theorem proving for hierarchic first-order theories
- Integrating Linear Arithmetic into Superposition Calculus
- Layered clause selection for theory reasoning (short paper)
- Hierarchic superposition with weak abstraction
- Selecting the selection
- Unification with abstraction and theory instantiation in saturation-based reasoning
Cited In (6)
- Coming to terms with quantified reasoning
- Lemmaless induction in trace logic
- Fully reusing clause deduction algorithm based on standard contradiction separation rule
- Unification with abstraction and theory instantiation in saturation-based reasoning
- Integer induction in saturation
- The 11th IJCAR automated theorem proving system competition – CASC-J11
Uses Software
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)
