In this article we firstly present a Kripke semantics for the description logic ALC which is directly inspired by the semantics for Intuitionistic logic. Moreover, we discuss why a direct translation of this kind of semantics is not adequate in the description logic context and propose a constructive semantics that differs from the previous one by the fact that we impose a condition on the partial order. We also present a tableau calculus which is sound and complete with respect to (...) our semantics. As an application of the calculus we prove that this semantics meets the disjunction property, a key criterion used in assessing whether a logic is constructive. (shrink)

This paper addresses questions of universality related to ontological engineering, namely aims at substantiating (negative) answers to the following three basic questions: (i) Is there a ‘universal ontology’?, (ii) Is there a ‘universal formal ontology language’?, and (iii) Is there a universally applicable ‘mode of reasoning’ for formal ontologies? To support our answers in a principled way, we present a general framework for the design of formal ontologies resting on two main principles: firstly, we endorse Rudolf Carnap’s principle of logical (...) tolerance by giving central stage to the concept of logical heterogeneity, i.e. the use of a plurality of logical languages within one ontology design. Secondly, to structure and combine heterogeneous ontologies in a semantically well-founded way, we base our work on abstract model theory in the form of institutional semantics, as forcefully put forward by Joseph Goguen and Rod Burstall. In particular, we employ the structuring mechanisms of the heterogeneous algebraic specification language HetCasl for defining a general concept of heterogeneous, distributed, highly modular and structured ontologies, called hyperontologies. Moreover, we distinguish, on a structural and semantic level, several different kinds of combining and aligning heterogeneous ontologies, namely integration, connection, and refinement. We show how the notion of heterogeneous refinement can be used to provide both a general notion of sub-ontology as well as a notion of heterogeneous equivalence of ontologies, and finally sketch how different modes of reasoning over ontologies are related to these different structuring aspects. (shrink)

In this paper, the positive fragment of the logic math formula of contraction-less relevant implication is extended with the addition of a paraconsistent negation connective similar to the strong negation connective in Nelson's paraconsistent four-valued logic math formula. This extended relevant logic is called math formula, and it has the property of constructible falsity which is known to be a characteristic property of math formula. A Gentzen-type sequent calculus math formula for math formula is introduced, and the cut-elimination and decidability (...) theorems for math formula are proved. Two extended Routley-Meyer semantics are introduced for math formula, and the completeness theorems with respect to these semantics are proved. (shrink)