Research

On Structuring Proof Search for First Order Linear Logic


Reference:

Bruscoli, P. and Guglielmi, A., 2003. On Structuring Proof Search for First Order Linear Logic. In: Lecture Notes in Artificial Intelligence, 2003-01-01.

Related documents:

This repository does not currently have the full-text of this item.
You may be able to access a copy if URLs are provided below.

Abstract

We start from the Forum presentation of first order linear logic to design an equivalent system for which proof search is highly structured. We restrict formulae to a language of clauses and goals, without losing expressivity, in such a way that formulae have the same structure of Forum sequents. This means having a very big generalised connective that suffices for al l of linear logic. We can then design a system with only two big rules, a left one and a right one. The behaviour of such system in proof search is operational ly interesting and makes it suitable for further semantic investigations. We test the mutual harmony of the new rules by showing a cut elimination theorem.

Details

Item Type Conference or Workshop Items (Paper)
CreatorsBruscoli, P.and Guglielmi, A.
DepartmentsFaculty of Science > Computer Science
RefereedNo
StatusPublished
ID Code5553

Export

Actions (login required)

View Item