Publikation

A Modular Consistency Proof for Dolce

Oliver Kutz, Till Mossakowski

In: Wolfram Burgard , Dan Roth (Hrsg.). Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence and the Twenty-Third Innovative Applications of Artificial Intelligence Conference. AAAI Conference on Artificial Intelligence (AAAI-11) 5th befindet sich combined with the Twenty-Third Innovative Applications of Artificial Intelligence Conference August 7-11 San Francisco CA United States Seiten 227-234 AAAI Press Menlo Park, CA 2011.

Abstrakt

We propose a novel technique for proving the consistency of large, complex and heterogeneous theories for which ‘standard’ automated reasoning methods are considered insufficient. In particular, we exemplify the applicability of the method by establishing the consistency of the foundational ontology DOLCE, a large, first-order ontology. The approach we advocate constructs a global model for a theory, in our case DOLCE, built from smaller models of subtheories together with amalgamability properties between such models. The proof proceeds by (i) hand-crafting a so-called architectural specification of DOLCE which reflects the way models of the theory can be built, (ii) an automated verification of the amalgamability conditions, and (iii) a (partially automated) series of relative consistency proofs.

Weitere Links

condolce.pdf (pdf, 341 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence