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, located at combined with the Twenty-Third Innovative Applications of Artificial Intelligence Conference, August 7-11, San Francisco, CA, USA, Pages 227-234, AAAI Press, Menlo Park, CA, 2011.
Zusammenfassung
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.