Model evolution with equality -- revised and implemented
From MaRDI portal
(Redirected from Publication:429586)
Recommendations
Cites work
- scientific article; zbMATH DE number 1614697 (Why is no real title available?)
- scientific article; zbMATH DE number 1809860 (Why is no real title available?)
- scientific article; zbMATH DE number 1809861 (Why is no real title available?)
- scientific article; zbMATH DE number 1809862 (Why is no real title available?)
- scientific article; zbMATH DE number 1950261 (Why is no real title available?)
- scientific article; zbMATH DE number 1552532 (Why is no real title available?)
- A machine program for theorem-proving
- Automated Deduction – CADE-20
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- Computer Science Logic
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Handbook of automated reasoning. In 2 vols
- Ordered semantic hyper-linking
- Paramodulation-based theorem proving
- Refutational theorem proving for hierarchic first-order theories
- Superposition and Model Evolution Combined
- System Description: E- KRHyper
- System Description: Spass Version 3.0
- The TPTP problem library. CNF release v1. 2. 1
- The disconnection method
- The model evolution calculus as a first-order DPLL method
- The model evolution calculus.
- The state of CASC
- Theorem proving with ordering and equality constrained clauses
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Cited in
(17)- Lemma Learning in the Model Evolution Calculus
- Finite reasons for safety. Parameterized verification by finite model finding
- Automated Deduction – CADE-20
- Model evolution and refinement
- A combined superposition and model evolution calculus
- Semantically-guided goal-sensitive reasoning: model representation
- On First-Order Model-Based Reasoning
- The equivalence between the TE, TM model and the Darwin models
- Detection and exploitation of functional dependencies for model generation
- E-Darvin
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Set of support, demodulation, paramodulation: a historical perspective
- SCL(EQ): SCL for first-order logic with equality
- (LIA) - Model Evolution with Linear Integer Arithmetic Constraints
- SCL(EQ): SCL for first-order logic with equality
- Superposition and Model Evolution Combined
- Model Evolution with Equality Modulo Built-in Theories
Describes a project that uses
Uses Software
This page was built for publication: Model evolution with equality -- revised and implemented
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q429586)