Related papers: Models for the Displacement Calculus
In this paper we introduce Commutative/Non-Commutative Logic (CNC logic) and two categorical models for CNC logic. This work abstracts Benton's Linear/Non-Linear Logic by removing the existence of the exchange structural rule. One should…
The aim of this expository article is to present recent developments in the centuries old discussion on the interrelations between continuous and differentiable real valued functions of one real variable. The truly new results include,…
We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof system based on inference rules, a combinatorial proof is a…
We develope a difference calculus analogous to the differential geometry by translating the forms and exterior derivatives to similar expressions with difference operators, and apply the results to fields theory on the lattice [Ref. 1]. Our…
We prove that in every compact space of Delone sets in $\mathbb{R}^d$ which is minimal with respect to the action by translations, either all Delone sets are uniformly spread, or continuously many distinct bounded displacement equivalence…
We introduce infinitary action logic with exponentiation -- that is, the multiplicative-additive Lambek calculus extended with Kleene star and with a family of subexponential modalities, which allows some of the structural rules…
Let ${\mathcal C}= \bigcup_{i=1}^n C_i \subseteq \mathbb{P}^2$ be a collection of smooth rational plane curves. We prove that the addition-deletion operation used in the study of hyperplane arrangements has an extension which works for a…
The primary goal of this paper is to present a unified way to transform the syntax of a logic system into certain initial algebraic structure so that it can be studied algebraically. The algebraic structures which one may choose for this…
We introduce a proper display calculus for (non-distributive) Lattice Logic which is sound, complete, conservative, and enjoys cut-elimination and sub-formula property. Properness (i.e. closure under uniform substitution of all parametric…
Autonomous morphology, such as inflection class systems and paradigmatic distribution patterns, is widespread and diachronically resilient in natural language. Why this should be so has remained unclear given that autonomous morphology…
Logical relations are one of the most powerful techniques in the theory of programming languages, and have been used extensively for proving properties of a variety of higher-order calculi. However, there are properties that cannot be…
Filinski constructed a symmetric lambda-calculus consisting of expressions and continuations which are symmetric, and functions which have duality. In his calculus, functions can be encoded to expressions and continuations using primitive…
Proving proof-size lower bounds for $\mathbf{LK}$, the sequent calculus for classical propositional logic, remains a major open problem in proof complexity. We shed new light on this challenge by isolating the power of structural rules,…
We extend the {\lambda}-calculus with constructs suitable for relational and functional-logic programming: non-deterministic choice, fresh variable introduction, and unification of expressions. In order to be able to unify…
The compactness theorem for a logic states, roughly, that the satisfiability of a set of well-formed formulas can be determined from the satisfiability of its finite subsets, and vice versa. Usually, proofs of this theorem depend on the…
There is a deformation of the ordinary differential calculus which leads from the continuum to a lattice (and induces a corresponding deformation of physical theories). We recall some of its features and relate it to a general framework of…
In the modeling of dislocations one is lead naturally to energies concentrated on lines, where the integrand depends on the orientation and on the Burgers vector of the dislocation, which belongs to a discrete lattice. The dislocations may…
Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametricity, and enforcing security protocols. In most…
An extension of the H-theorem for dissipative particle dynamics (DPD) to the case of a multi-component fluid is made. Detailed balance and an additional H-theorem are proved for an energy-conserving version of the DPD algorithm. The…
Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where each proposition has an intrinsic mode of truth. It has…