%0 Conference Paper %1 KutzMossakowski2011 %A Kutz, Oliver %A Mossakowski, Till %B Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence and the Twenty-Third Innovative Applications of Artificial Intelligence Conference %D 2011 %E Burgard, Wolfram %E Roth, Dan %I AAAI Press; Menlo Park, CA %K architectural consistency modular ontology specification %P 227-234 %T A Modular Consistency Proof for Dolce %U http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3754 %X 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.

@inproceedings{KutzMossakowski2011, abstract = {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.}, added-at = {2016-08-05T15:59:03.000+0200}, author = {Kutz, Oliver and Mossakowski, Till}, biburl = {https://www.bibsonomy.org/bibtex/240ff919c3d1d3ba16bc074e9870c2f5a/tillmo}, booktitle = {Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence and the Twenty-Third Innovative Applications of Artificial Intelligence Conference}, editor = {Burgard, Wolfram and Roth, Dan}, interhash = {63d5715550feaef819643ec998620dc2}, intrahash = {40ff919c3d1d3ba16bc074e9870c2f5a}, keywords = {architectural consistency modular ontology specification}, pages = {227-234}, pdfurl = {http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/download/3754/3863}, publisher = {AAAI Press; Menlo Park, CA}, status = {Reviewed}, timestamp = {2016-08-05T15:59:03.000+0200}, title = {A Modular Consistency Proof for Dolce}, url = {http://www.aaai.org/ocs/index.php/AAAI/AAAI11/paper/view/3754}, year = 2011 }