Related papers: Feasible Proofs of Matrix Properties with Csanky's…

Let L be a linear difference operator with polynomial coefficients. We consider singularities of L that correspond to roots of the trailing (resp. leading) coefficient of L. We prove that one can effectively construct a left multiple with…

We present a polynomial-time algorithm that obtains a set of Asymptotic Linear Programs (ALPs) from a given linear system S, such that one of these ALPs admits a feasible solution if and only if S admits a feasible solution. We also show…

Logics with team semantics provide alternative means for logical characterization of complexity classes. Both dependence and independence logic are known to capture non-deterministic polynomial time, and the frontiers of tractability in…

We have recently presented a general method of proving the fundamental logical properties of Craig and Lyndon Interpolation (IPs) by induction on derivations in a wide class of internal sequent calculi, including sequents, hypersequents,…

Starting from the expression for the superdeterminant of (xI-M), where M is an arbitrary supermatrix, we propose a definition for the corresponding characteristic polynomial and we prove that each supermatrix satisfies its characteristic…

The Automatic Amortized Resource Analysis (AARA) derives program-execution cost bounds using types. To do so, AARA often makes use of cost-free types, which are critical for the composition of types and cost bounds. However, inferring…

Gottfried Leibniz embarked on a research program to prove all the Aristotelic categorical syllogisms by diagrammatic and algebraic methods. He succeeded in proving them by means of Euler diagrams, but didn't produce a manuscript with their…

In this paper, we introduce a foundation for computable model theory of rational Pavelka logic (an extension of {\L}ukasiewicz logic) and continuous logic, and prove effective versions of some theorems in model theory. We show how to reduce…

The Cayley--Hamilton--Newton theorem for half-quantum matrices is proven.

Dependence logics are a modern family of logics of independence and dependence which mimic notions of database theory. In this paper, we aim to initiate the study of enumeration complexity in the field of dependence logics and thereby get a…

We extend classical methods of computational complexity to the realm of distributed computing, where they sometimes prove more effective than in their original context. Our focus is on decision problems in the LOCAL model, a setting in…

Given an associative, not necessarily commutative, ring R with identity, a formal matrix calculus is introduced and developed for pairs of matrices over R. This calculus subsumes the theory of homogeneous systems of linear equations with…

The aim of this article is to employ the Lazy Set algorithm as an example for a mathematical framework for proving the linearizability of distributed systems. The proof in this approach is divided into two stages of lower and higher…

Variable independence and decomposability are algorithmic techniques for simplifying logical formulas by tearing apart connections between free variables. These techniques were originally proposed to speed up query evaluation in constraint…

Linearisability has become the standard correctness criterion for concurrent data structures, ensuring that every history of invocations and responses of concurrent operations has a matching sequential history. Existing proofs of…

A set of multivariate polynomials, over a field of zero or large characteristic, can be tested for algebraic independence by the well-known Jacobian criterion. For fields of other characteristic p>0, there is no analogous characterization…

A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used…

A LAnKe (also known as a Filippov algebra or a Lie algebra of the $n$-th kind) is a vector space equipped with a skew-symmetric $n$-linear form that satisfies the generalized Jacobi identity. Friedmann, Hanlon, Stanley and Wachs have shown…

Fair termination is the property of programs that may diverge "in principle" but that terminate "in practice", i.e. under suitable fairness assumptions concerning the resolution of non-deterministic choices. We study a conservative…

I develop in depth the machinery of $(\mathcal L, n)$-models originally introduced by Shelah and, independently in a slightly different form by Kripke. This machinery allows fairly routine constructions of true but unprovable sentences in…