Model evolution with equality -- revised and implemented

DOI10.1016/J.JSC.2011.12.031MaRDI QIDQ429586zbMATH OpenOpenAlexFDO

Authors Björn Pelzer, Cesare Tinelli, 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

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)

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

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

• 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)