Superposition and Model Evolution Combined

DOI10.1007/978-3-642-02959-2_2zbMath1237.03010OpenAlexW1635857625MaRDI QIDQ5191094

Peter Baumgartner, Uwe Waldmann

Publication date: 28 July 2009

Published in: Automated Deduction – CADE-22 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-02959-2_2

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (8)

Semantically-guided goal-sensitive reasoning: model representation ⋮ On First-Order Model-Based Reasoning ⋮ Model evolution with equality -- revised and implemented ⋮ Semantically-guided goal-sensitive reasoning: inference system and completeness ⋮ SCL(EQ): SCL for first-order logic with equality ⋮ Model Evolution with Equality Modulo Built-in Theories ⋮ Set of support, demodulation, paramodulation: a historical perspective ⋮ SCL(EQ): SCL for first-order logic with equality

Uses Software

• SPASS

Cites Work

• Unnamed Item
• Theorem proving with ordering and equality constrained clauses
• System Description: Spass Version 3.0
• Term Rewriting and All That
• Automated Deduction – CADE-20
• Automated Deduction – CADE-19

This page was built for publication: Superposition and Model Evolution Combined