Model evolution with equality -- revised and implemented
From MaRDI portal
Publication:429586
DOI10.1016/J.JSC.2011.12.031zbMATH Open1258.03020OpenAlexW2163681902MaRDI QIDQ429586FDOQ429586
Cesare Tinelli, Peter Baumgartner, Björn Pelzer
Publication date: 20 June 2012
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jsc.2011.12.031
Recommendations
automated theorem provingequational reasoninginstance-based methodsmodel evolution calculus with equalitysuperposition inference ruletheorem prover \texttt{E-Darvin}
Cites Work
- The TPTP problem library. CNF release v1. 2. 1
- Title not available (Why is that?)
- Title not available (Why is that?)
- System Description: E- KRHyper
- A machine program for theorem-proving
- Ordered semantic hyper-linking
- Automated deduction -- CADE-22. 22nd international conference on automated deduction, Montreal, Canada, August 2--7, 2009. Proceedings
- The model evolution calculus as a first-order DPLL method
- Title not available (Why is that?)
- Title not available (Why is that?)
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Title not available (Why is that?)
- The disconnection method
- Superposition and Model Evolution Combined
- Experiments with discrimination-tree indexing and path indexing for term retrieval
- Theorem proving with ordering and equality constrained clauses
- Paramodulation-based theorem proving
- Title not available (Why is that?)
- Handbook of automated reasoning. In 2 vols
- Refutational theorem proving for hierarchic first-order theories
- System Description: Spass Version 3.0
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Computer Science Logic
- Automated Deduction – CADE-20
- The state of CASC
- Automated Deduction – CADE-19
Cited In (14)
- Set of support, demodulation, paramodulation: a historical perspective
- SCL(EQ): SCL for first-order logic with equality
- SCL(EQ): SCL for first-order logic with equality
- The equivalence between the TE, TM model and the Darwin models
- Automated Deduction – CADE-20
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Semantically-guided goal-sensitive reasoning: model representation
- Lemma Learning in the Model Evolution Calculus
- Model evolution and refinement
- On First-Order Model-Based Reasoning
- E-Darvin
- Finite reasons for safety
- Model Evolution with Equality Modulo Built-in Theories
- Detection and exploitation of functional dependencies for model generation
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)