Normalisation control in deep inference via atomic flows

Alessio Guglielmi, T Gundersen

Research output: Contribution to journalArticle

  • 29 Citations

Abstract

We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.
LanguageEnglish
Article number9
Pages1-36
Number of pages36
JournalLogical Methods in Computer Science
Volume4
Issue number1
DOIs
StatusPublished - 31 Mar 2008

Fingerprint

Syntactics
Normalization
Atoms
Cut-elimination
Inference Rules
Propositional Logic
Tracing
Manipulation
Intuitive
Paradigm
Graph in graph theory
Theorem
Syntax

Cite this

Normalisation control in deep inference via atomic flows. / Guglielmi, Alessio; Gundersen, T.

In: Logical Methods in Computer Science, Vol. 4, No. 1, 9, 31.03.2008, p. 1-36.

Research output: Contribution to journalArticle

@article{fc1d34c40b1a44118158e17c676bb0b6,
title = "Normalisation control in deep inference via atomic flows",
abstract = "We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.",
author = "Alessio Guglielmi and T Gundersen",
year = "2008",
month = "3",
day = "31",
doi = "10.2168/LMCS-4(1:9)2008",
language = "English",
volume = "4",
pages = "1--36",
journal = "Logical Methods in Computer Science",
issn = "1860-5974",
publisher = "Technischen Universitat Braunschweig",
number = "1",

}

TY - JOUR

T1 - Normalisation control in deep inference via atomic flows

AU - Guglielmi,Alessio

AU - Gundersen,T

PY - 2008/3/31

Y1 - 2008/3/31

N2 - We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.

AB - We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.

UR - http://www.scopus.com/inward/record.url?scp=58049104083&partnerID=8YFLogxK

UR - http://dx.doi.org/10.2168/LMCS-4(1:9)2008

U2 - 10.2168/LMCS-4(1:9)2008

DO - 10.2168/LMCS-4(1:9)2008

M3 - Article

VL - 4

SP - 1

EP - 36

JO - Logical Methods in Computer Science

T2 - Logical Methods in Computer Science

JF - Logical Methods in Computer Science

SN - 1860-5974

IS - 1

M1 - 9

ER -