A combined superposition and model evolution calculus
From MaRDI portal
Publication:438531
DOI10.1007/S10817-010-9214-XzbMATH Open1267.03033OpenAlexW1965168302MaRDI QIDQ438531FDOQ438531
Authors: Uwe Waldmann, Peter Baumgartner 
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9214-x
Recommendations
Cites Work
- Term Rewriting and All That
- Ordered semantic hyper-linking
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Comparing instance generation methods for automated reasoning
- Theorem proving with ordering and equality constrained clauses
- Title not available (Why is that?)
- Refutational theorem proving for hierarchic first-order theories
- System Description: Spass Version 3.0
- Computer Science Logic
- Automated Deduction – CADE-20
- The model evolution calculus.
- Combining instance generation and resolution
- Automated Deduction – CADE-20
Cited In (14)
- A superposition calculus for abductive reasoning
- Automated Deduction – CADE-20
- Superposition and Model Evolution Combined
- Title not available (Why is that?)
- Lemma Learning in the Model Evolution Calculus
- A complete superposition calculus for primal grammars
- Model evolution with equality -- revised and implemented
- The model evolution calculus as a first-order DPLL method
- Model Evolution with Equality Modulo Built-in Theories
- Title not available (Why is that?)
- Combining superposition, sorts and splitting
- Labelled splitting
- Labelled Splitting
- Integrating Linear Arithmetic into Superposition Calculus
Uses Software
This page was built for publication: A combined superposition and model evolution calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438531)
