Axioms and models of linear logic
Copyright policy )Axioms and models of linear logic
Abstract Girard's recent system of linear logic is presented in a way that avoids the two-level structure of formulae and sequents, and that minimises the number of primitive function symbols. A deduction theorem is proved concerning the classical implication as embedded in linear logic. The Hilbert-style axiomatisation is proved to be equivalent to the sequent formalism. The axiomatisation leads to a complete class of algebraic models. Various models are exhibited. On the meta-level we use Dijkstra's method of explicit equational proofs.
- University of Groningen Netherlands
Deduction theorem, Logic in computer science, Equational proofs, Phase structures, Linear logic, Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.), Monoid, deduction theorem, Sequent calculus, Proof theory and constructive mathematics, linear logic, Hilbert-style formulation, topological Girard monoids, Model theory, Axiomatisation
Deduction theorem, Logic in computer science, Equational proofs, Phase structures, Linear logic, Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.), Monoid, deduction theorem, Sequent calculus, Proof theory and constructive mathematics, linear logic, Hilbert-style formulation, topological Girard monoids, Model theory, Axiomatisation
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).5 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!