Sequent reconstruction in LLM -- A sweepline proof (Q1892938): Difference between revisions
From MaRDI portal
Set profile property. |
Set OpenAlex properties. |
||
(One intermediate revision by one other user not shown) | |||
Property / cites work | |||
Property / cites work: Planar and braided proof-nets for multiplicative linear logic with mix / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: A sweepline algorithm for Voronoi diagrams / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Linear logic / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3219753 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q3694703 / rank | |||
Normal rank | |||
Property / cites work | |||
Property / cites work: Q4495851 / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1016/0168-0072(94)00033-y / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W2033995205 / rank | |||
Normal rank |
Latest revision as of 09:21, 30 July 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Sequent reconstruction in LLM -- A sweepline proof |
scientific article |
Statements
Sequent reconstruction in LLM -- A sweepline proof (English)
0 references
26 July 1995
0 references
Proof-nets for linear logic are defined as certain (inductively defined) graph structures satisfying a further (topological) correctness criterion. The criterion makes the construction of inductive arguments over proof-nets difficult. The fact that to any proof-net there corresponds a proof in the standard sequent presentation of the logic, is known as the sequentialization theorem, for which we know several proofs, all non-trivial. The paper gives a new proof of the theorem, applying a technique well-known in computational geometry (sweepline algorithms), which exploits the graphical nature of the nets. The sequent proof is reconstructed by processing the proof-net one slice at a time, starting with the top (at the axioms) and proceeding downwards. The crucial notion for this approach to work is that of standard layout of a proof-net (informally, each premise of a node lies above the node; the conclusion of a node lies below the node; for any par-node, all the other nodes which contribute to the construction of the formulas in the par lie above the par). Main (but not difficult) result of the paper is that any proof- net has a standard layout. At this point the sweepline algorithm is almost obvious. The paper starts with the pure multiplicative case. Then it covers the multiplicative constants and the exponentials. The unit for par and the weakening are treated by extending the proof-nets with a new kind of link (the probe), which ensures connectedness. With probes, the Danos-Regnier criterion holds also for constant and exponential proof- nets.
0 references
sweepline algorithms
0 references
linear logic
0 references
graph structures
0 references
proof-nets
0 references
sequent
0 references
sequentialization theorem
0 references
computational geometry
0 references
standard layout
0 references