Proof Theory of Resource Logics


Research areas


Classical propositional logic (CPL) captures many aspects of human reasoning using logical expressions like "A & B", "A or B", "not A" and "if A then B". Suppose that we want to use logic to reason about resources like money or computer memory. Then we can let "A" stand for the fact that we have one dollar say. Classical propositional logic has some unwanted properties such as "(A & A) equals A" which conflate two copies of A (two dollars) with one copy of A (one dollar). Thus classical propositional logic is not a resource-sensitive logic. To avoid such strange properties of CPL, computer scientists often use logics called substructural logics, which allow us to make more fine-grained distinctions between the number and order of the formulae. Thus, none of the following principles of CPL hold in these logics: "(A & A) equals A"; "(A & B) equals (B & A)"; "A implies (A or B)".


The project is to study such logics with the aim of developing proof-calculi for these logics, in particular, some new logics with resource interpretations.


The project will involve reading technical papers in this area so you will need a strong background in discrete mathematics. It will also involve proving theorems about the proof-calculi that you design.


Successful completion is likely to lead to a publication.


proof theory, sequent calculi, cut-elimination, proof search

Updated:  15 May 2018/Responsible Officer:  Head of School/Page Contact:  CECS Marketing