In a multigranular framework, the two most important binary predicates are those for subsumption and disjointness. In the first part of this work, a sound and complete inference system for assertions using these predicates is developed. It is customized for the granular framework; particularly, it models both bottom and top granules correctly, and it requires all granules other then the bottom to be nonempty. Furthermore, it is single use, in the sense that no assertion is used more than once as an antecedent in a proof. In the second part of this work, a method is developed for extending a sound and complete inference system on a framework which admits Armstrong models to one which provides sound and complete inference on all assertions, both positive and negative. This method is then applied to the binary granule predicates, to obtain a sound and complete inference system for subsumption and disjointness, as well as their negations.
翻译:在多粒度框架中,两个最重要的二元谓词是子集与不交。在本工作的第一部分中,我们为使用这些谓词的断言开发了一个完备的推理系统。它针对粒度框架进行了定制,特别是正确地模拟了底部和顶部粒度,同时要求除底部粒度之外的所有粒度都是非空的。此外,它是单次使用的,即在证明中没有一个断言被用作前提超过一次。在本工作的第二部分中,我们开发了一种方法,用于在允许阿姆斯特朗模型的框架上扩展完备性推理系统,以提供对所有断言的完备推理(包括正面和负面断言)。然后,我们将此方法应用于二元粒度谓词,以获得子集和不交以及它们的否定的完备推理系统。