Combining decision procedures for positive theories sharing constructors

DOI10.1007/3-540-45610-4_25MaRDI QIDQ4808758zbMATH OpenFDO

Authors Franz Baader, Cesare Tinelli

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2378/23780352.htm

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)

Recommendations

• On Shostak's decision procedure for combinations of theories
• Logics in Artificial Intelligence
• Notions of knowledge in combinations of theories sharing constructors
• Combining decision procedures by (model-)equality propagation
• Combining Decision Procedures by (Model-)Equality Propagation
• Effective choice operations on constructive and positive models
• Combining Proof-Producing Decision Procedures
• Combining theories with shared set operations
• A generalization of Shostak's method for combining decision procedures
• Conjunctive rules in the theory of belief functions and their justification through decisions models

Cited in

(6)

• scientific article; zbMATH DE number 3898849 (Why is no real title available?)
• Combining equational theories sharing non-collapse-free constructors
• Quantifier Elimination and Provers Integration
• Deciding the word problem in the union of equational theories sharing constructors
• Model-theoretic methods in combined constraint satisfiability
• Non-disjoint combined unification and closure by equational paramodulation

This page was built for publication: Combining decision procedures for positive theories sharing constructors

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