Superposition for Fixed Domains

DOI10.1007/978-3-540-87531-4_22zbMath1156.03313OpenAlexW1531043891MaRDI QIDQ3540186

Matthias Horbach, Christoph Weidenbach

Publication date: 20 November 2008

Published in: Computer Science Logic (Search for Journal in Brave)

Full work available at URL: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.311.4342

Mathematics Subject Classification ID

Classical first-order logic (03B10) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items

Superposition as a decision procedure for timed automata ⋮ Decidability Results for Saturation-Based Model Building ⋮ Deciding the Inductive Validity of ∀ ∃ * Queries

Cites Work

• Automating inductionless induction using test sets
• Equational problems and disunification
• A method for simultaneous search for refutations and models by equational constraint solving
• Automated theorem proving by test set induction
• Model building with ordered resolution: Extracting models from saturated clause sets
• Induction = I-axiomatization + first-order consistency.
• Tree Automata with Equality Constraints Modulo Equational Theories
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Inductive theorem proving by consistency for first-order clauses
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item