Superposition for Fixed Domains

DOI10.1007/978-3-540-87531-4_22zbMATH Open1156.03313OpenAlexW1531043891MaRDI QIDQ3540186FDOQ3540186

Authors: 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

Recommendations

• Superposition for fixed domains
• Superposition for bounded domains
• Superposition with equivalence reasoning and delayed clause normal form transformation.
• Superposition modulo a Shostak theory.
• A superposition calculus for abductive reasoning

Mathematics Subject Classification ID

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

Cites Work

• Combining superposition, sorts and splitting
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Paramodulation-based theorem proving
• Equational problems and disunification
• Title not available (Why is that?)
• Automating inductionless induction using test sets
• Automated theorem proving by test set induction
• Model building with ordered resolution: Extracting models from saturated clause sets
• Induction = I-axiomatization + first-order consistency.
• Title not available (Why is that?)
• A method for simultaneous search for refutations and models by equational constraint solving
• Title not available (Why is that?)
• Tree Automata with Equality Constraints Modulo Equational Theories
• Inductive theorem proving by consistency for first-order clauses

Cited In (15)

• Title not available (Why is that?)
• Semantics for first-order superposition logic
• A superposition calculus for abductive reasoning
• Superposition for bounded domains
• A complete superposition calculus for primal grammars
• Superposition modulo a Shostak theory.
• A rule-based framework for building superposition-based decision procedures
• Title not available (Why is that?)
• System description: SPASS-FD
• Deciding the Inductive Validity of ∀ ∃ * Queries
• Decidability Results for Saturation-Based Model Building
• Model completeness, covers and superposition
• Superposition as a decision procedure for timed automata
• Superposition decides the first-order logic fragment over ground theories
• Superposition for fixed domains

This page was built for publication: Superposition for Fixed Domains

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3540186)