Student research opportunities

Proof Theory of Resource Logics

Project Code: CECS_865

This project is available at the following levels:
Honours
Please note that this project is only for undergraduate students.

Keywords:

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

Supervisors:

Professor Rajeev Gore
Dr Alwen Tiu

Outline:

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)".

Goals of this project

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.

Requirements/Prerequisites

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.