Details of Grant 

EPSRC Reference:	EP/K017438/1
Title:	The Limits of Decidability: Counting, Transitivity, Equivalence
Principal Investigator:	Pratt-Hartmann, Dr I
Other Investigators:
Researcher Co-Investigators:
Project Partners:	Opole University University of Wroclaw
Department:	Computer Science
Organisation:	University of Manchester, The
Scheme:	Standard Research
Starts:	14 March 2013	Ends:	17 September 2015	Value (£):	71,959
EPSRC Research Topic Classifications:	Fundamentals of Computing Information & Knowledge Mgmt
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 09 Oct 2012 EPSRC ICT Responsive Mode - Oct 2012 Announced
Summary on Grant Application Form
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.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.man.ac.uk