Details of Grant 

EPSRC Reference:	EP/K018868/1
Title:	Efficient and Natural Proof Systems
Principal Investigator:	Guglielmi, Dr A
Other Investigators:	McCusker, Professor G
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	University of Bath
Scheme:	Standard Research
Starts:	01 February 2013	Ends:	12 May 2016	Value (£):	556,849
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 21 Nov 2012 EPSRC ICT Responsive Mode - Nov 2012 Announced
Summary on Grant Application Form
We are all familiar with the language of classical logic, which is normally used for both mathematical and informal arguments, but there are other important and useful logics. Some nonclassical logics, for example, can be associated with programming languages to help control the behaviour of their programs, for instance via type systems. In order to define the proofs of a logic we need a proof system consisting of a formal language and some inference rules. We normally design proof systems following the prescriptions of some known formalism that ensures that we obtain desirable mathematical properties. In any case, we must make sure that proofs can be checked for validity with a computational effort that does not exceed certain limits. In other words, we want checking correctness to be relatively easy, also because this property facilitates the design of algorithms for the automatic discovery of proofs. However, there is a tension between the ease by which proofs can be checked and their size. If a proof is too small, checking it is difficult. Conversely, formalisms that make it very easy to check and to search for proofs create big bureaucratic unnatural proofs. All traditional proof systems suffer to various extents from this problem, because of the rigidity of all traditional formalisms, which impose an excess of structure on proof systems. We intend to design a formalism, provisionally called Formalism B, in which arbitrary logics can be defined and their proofs described in a way that is at the same time efficient and natural. Formalism B will ideally lie at the boundary between the class of proof systems and that of systems containing proto-proofs that are small and natural, but are too difficult to check. In other words, we want to maximise naturality by retaining as much efficiency as possible in proof representation. A driving force in this effort will be the use of existing algebraic theories that seem to capture some of the structure needed by the new formalism. There are two main reasons for doing this. One is theoretical: the problem is compelling, and tackling it fits well into a research effort in the theory of computation that tries to define proofs as more abstract mathematical objects than just intricate pieces of syntax. Suffice to say that we are at present unable to decide by an algorithm when two seemingly different proofs of the same statement use the same ideas and so are equivalent, or not. This is a problem that dates back to Hilbert and that requires more abstract ways to describe proofs than traditional syntax provides. The second reason is practical: we need formal proofs to verify the correctness of complex computer systems. The more powerful computer systems become, the more we need to ensure that they do what they are supposed to do. Formal verification is increasingly adopted as a viable instrument for this, but still much needs to be done in order to make it an everyday tool. We need to invent proof systems that simplify the interaction with proof assistants, and that could represent in some canonical way proofs that are essentially the same, so that no duplication occurs in the search for and storing of proofs in proof libraries. This project intends to contribute by exploiting proof-theoretic advances of the past ten years. We have developed a new design method for proof systems that reduces the size of inference steps to their minimal terms, in a theory called `deep inference'. The finer scale of rules allows us to associate proofs with certain purely geometric objects that faithfully abstract away proof structure, and that are natural guides for the design of proof systems whose proofs would not suffer from several forms of bureaucracy. In short, after a decade in which we broke proofs into their smallest pieces, by retaining their properties, we are now reshaping them in such a way that they still retain all the features we need but do not keep the undesirable ones.
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.bath.ac.uk