Model evolution with equality -- revised and implemented

DOI10.1016/j.jsc.2011.12.031zbMath1258.03020OpenAlexW2163681902MaRDI QIDQ429586

Cesare Tinelli, Björn Pelzer, Peter Baumgartner

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

zbMATH Keywords

equational reasoningautomated theorem provinginstance-based methodsmodel evolution calculus with equalitysuperposition inference ruletheorem prover \texttt{E-Darvin}

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Semantically-guided goal-sensitive reasoning: model representation, On First-Order Model-Based Reasoning, Semantically-guided goal-sensitive reasoning: inference system and completeness, Detection and exploitation of functional dependencies for model generation, SCL(EQ): SCL for first-order logic with equality, E-Darvin, Set of support, demodulation, paramodulation: a historical perspective, SCL(EQ): SCL for first-order logic with equality, Finite reasons for safety

Uses Software

• OTTER
• VAMPIRE
• SPASS
• TPTP
• Darwin
• Metis_
• iProver
• E Theorem Prover
• Bliksem
• E-KRHyper

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Experiments with discrimination-tree indexing and path indexing for term retrieval
• The TPTP problem library. CNF release v1. 2. 1
• Refutational theorem proving for hierarchic first-order theories
• Ordered semantic hyper-linking
• Theorem proving with ordering and equality constrained clauses
• 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
• iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
• System Description: E- KRHyper
• System Description: Spass Version 3.0
• Geometric Resolution: A Proof Procedure Based on Finite Model Search
• The disconnection method
• Superposition and Model Evolution Combined
• Computer Science Logic
• Automated Deduction – CADE-20
• A machine program for theorem-proving
• Automated Deduction – CADE-19