A combined superposition and model evolution calculus
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- Automated Deduction – CADE-20
- Automated Deduction – CADE-20
- Combining instance generation and resolution
- Comparing instance generation methods for automated reasoning
- Computer Science Logic
- Ordered semantic hyper-linking
- Refutational theorem proving for hierarchic first-order theories
- System Description: Spass Version 3.0
- Term Rewriting and All That
- The model evolution calculus.
- Theorem proving with ordering and equality constrained clauses
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Cited in
(14)- A complete superposition calculus for primal grammars
- Lemma Learning in the Model Evolution Calculus
- Labelled splitting
- The model evolution calculus as a first-order DPLL method
- Integrating Linear Arithmetic into Superposition Calculus
- Automated Deduction – CADE-20
- Model evolution with equality -- revised and implemented
- scientific article; zbMATH DE number 1950258 (Why is no real title available?)
- scientific article; zbMATH DE number 5999715 (Why is no real title available?)
- Combining superposition, sorts and splitting
- Superposition and Model Evolution Combined
- A superposition calculus for abductive reasoning
- Model Evolution with Equality Modulo Built-in Theories
- Labelled Splitting
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)
