| Popis: |
We present a non-deterministic model of computation related to Robinson’s first-order resolution. This model formalises and extends ideas sketched by Girard in his Transcendental Syntax programme. After establishing formal defini- tions and basic properties, we show its Turing-completeness by exhibiting how it naturally models logic programs as well as non-deterministic tiling constructions such as those defining the abstract tile assembly model, recently used in DNA computing. In a second part, we explain how this model of computation yields, using realisability techniques, a dynamic semantics of proofs in the multiplicative fragment of linear logic (MLL), for which we obtain full-completeness results for both MLL and MLL extended with the so-called MIX rule. |
