The Limits of Decidability: Counting, Transitivity, Equivalence
Lead Research Organisation:
University of Manchester
Department Name: Computer Science
Abstract
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.
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.
Planned Impact
The research proposed here is aimed principally at providing a resource to the Knowledge Engineering community in the form of algorithms for reasoning with a new range of expressive formal languages. The most efficient way to achieve impact for this work is through presentation of results in specialist conferences and publication in specialist journals in the area of Knowledge Representation and Reasoning. Accordingly, funds have been requested for this purpose (see Case for Support, Section D).
The mathematical techniques we expect to call on in the proposed research will be drawn from the fields of integer programming, combinatorics and graph theory. (See the Case for Support, Section C.) We believe that the applications of these techniques investigated here will be of interest to the wider mathematics/logic community. In particular, we hope to stimulate the interchange of ideas between practitioners in the area of Knowledge Engineering and the academic communities centred around the mathematical techniques underlying our research. To this end, we have requested funds for participation in academic conferences with a more general mathematical audience (see Case for Support, Section D).
The mathematical techniques we expect to call on in the proposed research will be drawn from the fields of integer programming, combinatorics and graph theory. (See the Case for Support, Section C.) We believe that the applications of these techniques investigated here will be of interest to the wider mathematics/logic community. In particular, we hope to stimulate the interchange of ideas between practitioners in the area of Knowledge Engineering and the academic communities centred around the mathematical techniques underlying our research. To this end, we have requested funds for participation in academic conferences with a more general mathematical audience (see Case for Support, Section D).
People |
ORCID iD |
| I Pratt-Hartmann (Principal Investigator) |
Publications
Pratt-Hartmann I
(2016)
Quine's Fluted Fragment is Non-Elementary
Pratt-Hartmann I
(2014)
Logics with counting and equivalence
Pratt-Hartmann I
(2018)
Finite satisfiability for two-variable, first-order logic with one transitive relation is decidable
in Mathematical Logic Quarterly
PRATT-HARTMANN I
(2019)
THE FLUTED FRAGMENT REVISITED
in The Journal of Symbolic Logic
Pratt-Hartmann I
(2015)
The two-variable fragment with counting and equivalence
in Mathematical Logic Quarterly
Kourtis G
(2017)
ADDING PATH-FUNCTIONAL DEPENDENCIES TO THE GUARDED TWO-VARIABLE FRAGMENT WITH COUNTING
in Logical Methods in Computer Science
Kieronski E
(2015)
Equivalence closure in the two-variable guarded fragment
in Journal of Logic and Computation
Kieronski E
(2017)
Equivalence closure in the two-variable guarded fragment
in Journal of Logic and Computation
| Description | The aims of the project were to enhance our understanding of the theoretical limits of automated reasoning, and to extend the repertoire of techniques available to knowledge engineers for reasoning about structured data. The detailed objectives involved the investigation of the computational complexity of reasoning with two sorts of logics: (i) logics featuring counting quantifiers and equivalence relations; (ii) logics extending the 'Fluted Fragment';---a restricted form of logic introduced by W. V. Quine in 1969. (For a technical audience: roughly speaking, in the Fluted Fragment, variables are quantified in the same order in which they appear as arguments to predicates.) The stated objectives regarding logics featuring counting quantifiers were fully met. The principal results obtained are: (1) two-variable first-order logic with counting quantifiers can be extended with a single equivalence relation without increasing the complexity of reasoning; (2) adding a second equivalence relation results in undecidability. In an extension to the original project objectives, I and my project collaborators in Wroclaw and Opole determined the complexity of reasoning in two-variable guarded logic with any number of equivalence relations. These results close the last open problems concerning two-variable logics with equivalence relations, so that an essentially complete picture results. The obtained results were published in one conference paper (in the conference LICS 2014) and two journal papers (in Mathematical Logic Quarterly and the Journal of Logic and Computation). In addition to charting the limits of decidability in logics with equivalence relations, the techniques employed in result (1) represent a novel extension of techniques from linear algebra to the complexity-theoretic analysis of decidable fragments of logic. The stated objectives regarding extensions of the Fluted Fragment were not met in the way envisaged, because of a surprising finding. The original plan (as set out in the case for support) was to extend a result concerning the computational complexity of the Fluted Fragment published by W.C. Purdy in the journal Studia Logia in 2002. The analysis of this logic turned out to be much harder than expected. The solution was found close to the end of the project, when, together with my project collaborators in Opole, I found that Purdy's result was in fact false: the complexity of the Fluted Fragment is much harder than previously claimed. (For experts: Purdy claimed that the satisfiability problem is in NExpTime; in fact, it is non-elementary.) This result was presented at the conference Logic in Computer Science, 2016 and the Journal of Symbolic Logic, vol 84(3), 2019, pp. 1020--1048. In fact, we showed more: we found a hierarchy of logics contained within the Fluted Fragment, of ever greater complexity. The time required to correct this mistake in the published literature meant that progress on extensions of this fragment could not be made. However, since these extensions must be at least as complex as the Fluted Fragment, our work shows that they are probably of little practical interest. Arising out of the above work, further results have been obtained on the complexity of other decidable fragments, including the guarded two-variable fragment with equivalence relations and the guarded two-variable fragment with counting and key-constraints. In particular, in 2018, the principal investigator resolved a long outstanding open question in this area by showing the finite satisfiability problem for two-variable first-order logic with a single transitive relation is decidable. |
| Exploitation Route | The research undertaken here has potential applications in Knowledge Representation, Artificial Intelligence and automatic program verification. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| URL | http://www.cs.man.ac.uk/~ipratt/ |