A comprehensive combination framework

fragment enjoys suitable noetherianity conditions and admits an abstract version of a `KeislerShelah like' isomorphism theorem. We show that this general decidability transfer result covers recent work on combination in first-order theories as well as in various intensional logics such as description, modal, and temporal logics. Categories and Subject Descriptors: F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--Mechanical theorem proving; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving--Inference engines; I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods--Modal logic; Predicate logic General Terms: Logic, Algorithms, Decidability Additional Key Words and Phrases: Combination, Decision Procedures, Higher-Order Logic, Modal and Description Logics, Satisfiability Modulo Theory

• Type: Journal
• Year: 2008
• Where: TOCL
• Authors: Silvio Ghilardi, Enrica Nicolini, Daniele Zucchelli
• Keywords: Artificial Intelligence, Logics, Mathematical Logic, TOCL 2008