No description available.

No description available.

No description available.

No description available.

No description available.

Specialized vocabulary, notations and inference rules tailored for the description, analysis and reasoning of a domain is very important for the domain. For domain-specific issues researchers focus mainly on the design and implementation of domain-specific languages (DSL) and pay little attention to the reasoning aspects. We believe that domain-specific reasoning is very important to help the proofs of some properties of the domains and should be more concise, more reusable and more believable. It deserves to be investigated in an engineering way. Type theory provides good support for generic reasoning and verification. Many type theorists want to extend uses of type theory to more domains, and believe that the methods, ideas, and technology of type theory can have a beneficial effect for computer assisted reasoning in many domains. Proof assistants based on type theory are well known as effective tools to support reasoning. But these proof assistants have focused primarily on generic notations for representation of problems and are oriented towards helping expert type theorists build proofs efficiently. They are successful in this goal, but they are less suitable for use by non-specialists. In other words, one of the big barriers to limit the use of type theory and proof assistant in domain-specific areas is that it requires significant expertise to use it effectively. We present LFTOP ― a new approach to domain-specific reasoning that is based on a type-theoretic logical framework (LP) but does not require the user to be an expert in type theory. In this approach, users work on a domain-specific interface that is familiar to them. The interface presents a reasoning system of the domain through a user-oriented syntax. A middle layer provides translation between the user syntax and LF， and allows additional support for reasoning (e.g. model checking). Thus, the complexity of the logical framework is hidden but we also retain the benefits of using type theory and its related tools, such as precision and machine-checkable proofs. The approach is being investigated through a number of case studies. In each case study, the relevant domain-specific specification languages and logic are formalized in Plastic. The relevant reasoning system is designed and customized for the users of the corresponding specific domain. The corresponding lemmas are proved in Plastic. We analyze the advantages and shortcomings of this approach, define some new concepts related to the approach, especially discuss issues arising from the translation between the different levels. A prototype implementation is developed. We illustrate the approach through many concrete examples in the prototype implementation. The study of this thesis shows that the approach is feasible and promising, the relevant methods and technologies are useful and effective.

No description available.

No description available.

Ontologies play a key role in many areas of Computing Science, such as Information Retrieval, Knowledge Management, and Knowledge Engineering. However, Ontology development and maintenance is a challenging task that is currently not very well supported by software tools. Most existing ontology editors cannot provide the kind of automated reasoning support that is required for the verification and for the validation of ontologies. More concretely, such an automated support should (i) check the ontology consistency and (ii) suggest possible enhancements to the ontology taxonomy. Description Logic engines compute the kind of inferences that are useful for an automated ontology verification and validation but are not suitable for all ontology representation languages. More concretely, the semantics of Description Logics is based on the Open World Assumption, whereas the semantics of some ontology representation languages is based on the Closed World Assumption. Furthermore, the knowledge model of Description Logics is derived from Frame-based knowledge representation. Therefore Description Logics lack some modelling primitives necessary to express knowledge that can be represented with conceptual modelling languages. On the other hand, conceptual modelling languages (i) do not have the same expressive power as Frame-based ontology languages and (ii) no reasoners are available for automated reasoning with these languages. Hence, this thesis introduces the Conceptual Knowledge Modelling Language (CKML) and proposes an approach for the verification and validation of CKML ontologies. Rather than developing a special-purpose reasoning algorithm for CKML, we investigate how Description Logic engines can be used for this task. This approach can also be applied to a language that describes database schemas specified with the Enhanced Entity-Relationship model.

No description available.