Superposition for Fixed Domains

DOI10.1007/978-3-540-87531-4_22MaRDI QIDQ3540186zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

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

Cited in

(15)

• Superposition for fixed domains
• scientific article; zbMATH DE number 1848313 (Why is no real title available?)
• 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
• scientific article; zbMATH DE number 5857449 (Why is no real title available?)
• System description: SPASS-FD
• Deciding the Inductive Validity of ∀ ∃ * Queries
• Model completeness, covers and superposition
• Decidability Results for Saturation-Based Model Building
• Superposition as a decision procedure for timed automata
• Superposition decides the first-order logic fragment over ground theories

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)