Paper Info
Title
Full Completeness: Interactive And Geometric Characterizations Of The Space Of Proofs - Abstract
Abstract
We pursue the program of exposing the intrinsic mathematical structure of the "space of a proofs" of a logical system [AJ94b]. We study the case of Multiplicative-Additive Linear Logic (MALL). We use tools from Domain theory to develop a semantic notion of proof net for MALL, and prove a Sequentialization Theorem. We also give an interactive criterion for strategies, formalized in the same Domain-theoretic setting, to come from proofs, and show that a "semantic proof structure" satisfies the geometric correctness criterion for proof-nets if and only if it satisfies the interactive criterion for strategies. We also use the Domain-theoretic setting to give an elegant compositional account of Cut-Elimination. This work is a continuation of previous joint work with Radha Jagadeesan [AJ94b] and Paul-Andre Mellies [AM99].
Year
DOI
Venue
2007
10.1007/978-3-540-74915-8_1
COMPUTER SCIENCE LOGIC, PROCEEDINGS
Keywords
Field
DocType
domain theory,satisfiability
Discrete mathematics,Combinatorics,Mathematical structure,Computer science,Correctness,Domain theory,Proof theory,Mathematical proof,Linear logic,Completeness (statistics),Proof net
Conference
Volume
ISSN
Citations 
4646
0302-9743
0
PageRank 
References 
Authors
0.34
6
1
Name
Order
Citations
PageRank
Samson Abramsky13169348.51