On Structuring Proof Search for First Order Linear Logic

P Bruscoli, A Guglielmi

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

Full first order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the `proof search as computation´ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.
Original languageEnglish
Pages (from-to)42-76
Number of pages35
JournalTheoretical Computer Science
Volume360
Issue number1-3
Publication statusPublished - 2006

Fingerprint

Proof Search
Linear Logic
Logic programming
Syntactics
First-order Logic
Computer programming languages
Semantics
Inference Rules
Testing
Cut-elimination
Operational Semantics
Appeal
Expressiveness
Logic Programming
Programming Languages
Paradigm
Restriction
Internal
Symmetry

Cite this

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

In: Theoretical Computer Science, Vol. 360, No. 1-3, 2006, p. 42-76.

Research output: Contribution to journalArticle

@article{003a0c0b67f148f4bc61e2e6874a974f,
title = "On Structuring Proof Search for First Order Linear Logic",
abstract = "Full first order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the `proof search as computation´ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.",
author = "P Bruscoli and A Guglielmi",
year = "2006",
language = "English",
volume = "360",
pages = "42--76",
journal = "Theoretical Computer Science",
issn = "0304-3975",
publisher = "Elsevier",
number = "1-3",

}

TY - JOUR

T1 - On Structuring Proof Search for First Order Linear Logic

AU - Bruscoli, P

AU - Guglielmi, A

PY - 2006

Y1 - 2006

N2 - Full first order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the `proof search as computation´ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.

AB - Full first order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the `proof search as computation´ paradigm. However, Forum still has to deal with syntactic details that would normally be ignored by a reasonable operational semantics. In this respect, Forum improves on Gentzen systems for linear logic by restricting the language and the form of inference rules. We further improve on Forum by restricting the class of formulae allowed, in a system we call G-Forum, which is still equivalent to full first order linear logic. The only formulae allowed in G-Forum have the same shape as Forum sequents: the restriction does not diminish expressiveness and makes G-Forum amenable to proof theoretic analysis. G-Forum consists of two (big) inference rules, for which we show a cut elimination procedure. This does not need to appeal to finer detail in formulae and sequents than is provided by G-Forum, thus successfully testing the internal symmetries of our system.

M3 - Article

VL - 360

SP - 42

EP - 76

JO - Theoretical Computer Science

JF - Theoretical Computer Science

SN - 0304-3975

IS - 1-3

ER -