Decidability Results for Saturation-Based Model Building

DOI10.1007/978-3-642-02959-2_30zbMath1250.03014OpenAlexW1597601988MaRDI QIDQ5191116

Matthias Horbach, Christoph Weidenbach

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_30

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items (3)

Decidability Results for Saturation-Based Model Building ⋮ Predicate Completion for non-Horn Clause Sets ⋮ System Description: SPASS-FD

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Explicit representation of terms defined by counter examples
• Equational problems and disunification
• Induction = I-axiomatization + first-order consistency.
• Automated model building
• Superposition for Fixed Domains
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Hyperresolution and automated model building
• Decidability Results for Saturation-Based Model Building
• Model Representation over Finite and Infinite Signatures
• Automated Deduction – CADE-19

This page was built for publication: Decidability Results for Saturation-Based Model Building