Model evolution with equality -- revised and implemented

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 Deduction – CADE-20
• A combined superposition and model evolution calculus
• Superposition and Model Evolution Combined
• Lemma Learning in the Model Evolution Calculus
• Model Evolution with Equality Modulo Built-in Theories

zbMATH Keywords

automated theorem provingequational reasoninginstance-based methodsmodel evolution calculus with equalitysuperposition inference ruletheorem prover \texttt{E-Darvin}

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

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

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

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)