Normalisation Control in Deep Inference via Atomic Flows
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 an...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2008-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1081/pdf |
| _version_ | 1827322994970591232 |
|---|---|
| author | Alessio Guglielmi Tom Gundersen |
| author_facet | Alessio Guglielmi Tom Gundersen |
| author_sort | Alessio Guglielmi |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:37:44Z |
| format | Article |
| id | doaj.art-702e584ed2fd472caebe15f5ab16f622 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:44Z |
| publishDate | 2008-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-702e584ed2fd472caebe15f5ab16f6222024-03-08T08:52:03ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742008-03-01Volume 4, Issue 110.2168/LMCS-4(1:9)20081081Normalisation Control in Deep Inference via Atomic FlowsAlessio Guglielmihttps://orcid.org/0000-0002-7234-2347Tom GundersenWe 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.https://lmcs.episciences.org/1081/pdfmathematics - logiccomputer science - logic in computer sciencef.4.1 |
| spellingShingle | Alessio Guglielmi Tom Gundersen Normalisation Control in Deep Inference via Atomic Flows Logical Methods in Computer Science mathematics - logic computer science - logic in computer science f.4.1 |
| title | Normalisation Control in Deep Inference via Atomic Flows |
| title_full | Normalisation Control in Deep Inference via Atomic Flows |
| title_fullStr | Normalisation Control in Deep Inference via Atomic Flows |
| title_full_unstemmed | Normalisation Control in Deep Inference via Atomic Flows |
| title_short | Normalisation Control in Deep Inference via Atomic Flows |
| title_sort | normalisation control in deep inference via atomic flows |
| topic | mathematics - logic computer science - logic in computer science f.4.1 |
| url | https://lmcs.episciences.org/1081/pdf |
| work_keys_str_mv | AT alessioguglielmi normalisationcontrolindeepinferenceviaatomicflows AT tomgundersen normalisationcontrolindeepinferenceviaatomicflows |