Track:
Contents
Downloads:
Abstract:
Research in hybrid logic systems and, later, description logics, has revealed a tradeoff between the expressivity of a logical formalism, and the complexity of reasoning within that formalism. This is why, for instance, tractable inference procedures are known for certain classes of description logics and for (some) formalisms underlying knowledge representation on the Semantic Web. Some traditions within artificial intelligence and knowledge representation have focused on more expressive knowledge representations. For some expressive representations, such as first-order logic, sound and complete proof calculi, such as the sequent calculus, have been developed. However, for the purposes of automated theorem proving, not all proof calculi are created equal. Engineering effective proof search strategies for some proof calculi is difficult, but other proof calculi, e.g., those based on resolution, do lend themselves to efficient proof search. Recognizing the diversity of knowledge representation systems currently in existence, the different properties of proof calculi which may be employed over these systems, and the growing need to combine inferences made under multiple logical systems, we propose the development of formalisms to govern these interactions, and call this the study of combined logics.