权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

The Limits of Decidability: Counting, Transitivity, Equivalence

可判定性的限制：计数、传递性、等价性

基本信息

批准号：
EP/K017438/1
负责人：
I Pratt-Hartmann
金额：
$ 9.17万
依托单位：
University of Manchester
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2013
资助国家：
英国
起止时间：
2013 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FK017438%2F1
关键词：
Limits Decidability Counting Transitivity Equivalence

项目摘要

First-order logic is a formal language for describing structured ensembles of objects and data. The use of first-order logic to specify, query and manipulate such structured data is now firmly embedded in the theory and practice of a wide range of academic disciplines. Automating the process of deductive reasoning in first-order logic is therefore a central challenge in Computer Science.However, reasoning with first-order logic is known to be undecidable: it is in principle impossible to write a computer program that can reliably determine all logical consequences expressible using this formalism. On the other hand, it has long been understood that, by restricting the language of first-order logic in various ways, we obtain 'fragments' of logic in which decidability is restored. Furthermore, we observe a trade-off between expressive power and computational manageability: the smaller a fragment is---i.e. the less expressive it is---the easier it is to reason in. The research proposed here will investigate several very expressive fragments of first-order logic---those near the upper limit of decidability---and determine their decidability/computational complexity.We take as our point of departure three fragments of first-order logic which are known to be decidable: the 'two-variable fragment', the 'guarded fragment' and the 'fluted fragment'. We investigate the effect of extending the expressive power of these logics in three ways (severally, or in combination). The first extension we consider involves numerical quantifiers, which allow us to place (upper or lower) bounds on how many objects satisfy some given property. The second extension we consider involves the use of transitive relations such as 'is taller than' or `earns more money then'. (Such relations have special logical properties that need to be taken into account in reasoning problems.) The third extension we consider involves the use of equivalence relations such as 'is the same height as' or 'has the same tax code as'. In this way, we obtain a collection of fragments of first-order logic for which it is currently open whether reasoning is decidable. We propose to resolve these open problems.For those fragments which we show to be decidable, we shall obtain (as a by-product of our proof) an algorithm for reasoning within the fragments in question; for those shown to be undecidable, we know that no such algorithm exists. Moreover, for the decidable fragments, we can quantify the difficulty of reasoning within them, and even identify the specific kinds of formulas that are responsible for the difficult cases. Thus, our research represents a contribution to the enterprise of using first-order logic to describe, query or manipulate structured data.

一阶逻辑是一种用于描述对象和数据的结构化集合的形式语言。使用一阶逻辑来指定，查询和操作这种结构化数据现在已经牢固地嵌入到广泛的学科理论和实践中。因此，自动化一阶逻辑的演绎推理过程是计算机科学的一个核心挑战。然而，一阶逻辑的推理是不可判定的：原则上不可能编写一个计算机程序来可靠地确定所有使用这种形式化的逻辑结果。另一方面，人们早就知道，通过以各种方式限制一阶逻辑的语言，我们得到了恢复可判定性的逻辑的“片段”。此外，我们观察到表达能力和计算能力之间的权衡：片段越小--也就是说，它的表达能力越低--越容易推理。这里提出的研究将调查几个非常有表现力的片段的一阶逻辑-那些接近上限的可判定性-并确定其可判定性/计算复杂度。我们采取作为我们的出发点的三个片段的一阶逻辑这是已知的可判定的：“两变量片段”，“保护片段”和“凹槽片段”。我们调查的影响，这些逻辑的表达能力，在三种方式（分别，或组合）。我们考虑的第一个扩展涉及数字量词，它允许我们对有多少对象满足某个给定属性设置（上或下）界限。我们考虑的第二个扩展涉及到传递关系的使用，例如“比”或“赚更多的钱”。(Such关系具有特殊的逻辑属性，需要在推理问题中加以考虑。我们考虑的第三个扩展涉及使用等价关系，例如“与……身高相同”或“与……税法相同”。通过这种方式，我们得到了一个一阶逻辑片段的集合，对于这些片段，推理是否是可判定的目前还没有定论。我们提出解决这些开放的问题。对于那些我们证明是可判定的片段，我们将获得（作为我们证明的副产品）在所讨论的片段内进行推理的算法;对于那些证明是不可判定的片段，我们知道不存在这样的算法。此外，对于可判定的片段，我们可以量化其中推理的难度，甚至可以识别出导致困难情况的特定类型的公式。因此，我们的研究代表了企业使用一阶逻辑来描述，查询或操作结构化数据的贡献。