On Structuring Proof Search for First Order Linear Logic

P Bruscoli, A Guglielmi

Research output: Contribution to conferencePaper

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.
Original languageEnglish
Pages389-406
Number of pages18
Publication statusPublished - 2003
EventLecture Notes in Artificial Intelligence -
Duration: 1 Jan 2003 → …

Conference

ConferenceLecture Notes in Artificial Intelligence
Period1/01/03 → …

Fingerprint

Semantics

Cite this

Bruscoli, P., & Guglielmi, A. (2003). On Structuring Proof Search for First Order Linear Logic. 389-406. Paper presented at Lecture Notes in Artificial Intelligence, .

On Structuring Proof Search for First Order Linear Logic. / Bruscoli, P; Guglielmi, A.

2003. 389-406 Paper presented at Lecture Notes in Artificial Intelligence, .

Research output: Contribution to conferencePaper

Bruscoli, P & Guglielmi, A 2003, 'On Structuring Proof Search for First Order Linear Logic' Paper presented at Lecture Notes in Artificial Intelligence, 1/01/03, pp. 389-406.
Bruscoli P, Guglielmi A. On Structuring Proof Search for First Order Linear Logic. 2003. Paper presented at Lecture Notes in Artificial Intelligence, .
Bruscoli, P ; Guglielmi, A. / On Structuring Proof Search for First Order Linear Logic. Paper presented at Lecture Notes in Artificial Intelligence, .18 p.
@conference{98859d7853364f19b6e760077d54b1d9,
title = "On Structuring Proof Search for First Order Linear Logic",
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.",
author = "P Bruscoli and A Guglielmi",
year = "2003",
language = "English",
pages = "389--406",
note = "Lecture Notes in Artificial Intelligence ; Conference date: 01-01-2003",

}

TY - CONF

T1 - On Structuring Proof Search for First Order Linear Logic

AU - Bruscoli, P

AU - Guglielmi, A

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

M3 - Paper

SP - 389

EP - 406

ER -