Related papers: Finite two-dimensional proof systems for non-finit…
We study the general problem of strengthening the logic of a given (partial) (non-deterministic) matrix with a set of axioms, using the idea of rexpansion. We obtain two characterization methods: a very general but not very effective one,…
Models of complex systems are widely used in the physical and social sciences, and the concept of layering, typically building upon graph-theoretic structure, is a common feature. We describe an intuitionistic substructural logic called…
In this paper, we focus on the variety DHMSH of dually hemimorphic semi-Heyting algebras from a logical point of view. Firstly, we present a Hilbert-style axiomatization of a new logic called Dually hemimorphic semi-Heyting logic (DHMSH,…
Over the past two decades several fragments of first-order logic have been identified and shown to have good computational and algorithmic properties, to a great extent as a result of appropriately describing the image of the standard…
We prove that the problem of determining whether a finite logical matrix determines an algebraizable logic is complete for EXPTIME. The same result holds for the classes of order algebraizable, weakly algebraizable, equivalential and…
We provide a complete axiomatization of modal inclusion logic - team-based modal logic extended with inclusion atoms. We review and refine an expressive completeness and normal form theorem for the logic, define a natural deduction proof…
We consider the extension of two variable logic with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of…
We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a…
The usual reading of logical implication "A implies B" as "if A then B" fails in intuitionistic logic: there are formulas A and B such that "A implies B" is not provable, even though B is provable whenever A is provable. Intuitionistic…
We bring forward a logical system of transition algebras that enhances many-sorted first-order logic using features from dynamic logics. The sentences we consider include compositions, unions, and transitive closures of transition…
We generalize intuitionistic tense logics to the multi-modal case by placing grammar logics on an intuitionistic footing. We provide axiomatizations for a class of base intuitionistic grammar logics as well as provide axiomatizations for…
We present a logic named L_{LF} whose intended use is to formalize properties of specifications developed in the dependently typed lambda calculus LF. The logic is parameterized by the LF signature that constitutes the specification. Atomic…
We study the finite satisfiability problem for the two-variable fragment of first-order logic extended with counting quantifiers (C2) and interpreted over linearly ordered structures. We show that the problem is undecidable in the case of…
We analyze the periodicity of optimal long products of matrices. A set of matrices is said to have the finiteness property if the maximal rate of growth of long products of matrices taken from the set can be obtained by a periodic product.…
Matching logic is a formalism for specifying, and reasoning about, mathematical structures, using patterns and pattern matching. Growing in popularity, it has been used to define many logical systems such as separation logic with recursive…
The set of finite binary matrices of a given size is known to carry a finite type A bicrystal structure. We first review this classical construction, explain how it yields a short proof of the equality between Kostka polynomials and…
We show that a proof in multiplicative linear logic can be represented as a decorated surface, such that two proofs are logically equivalent just when their surfaces are geometrically equivalent. This is an extended abstract for…
Non-iterative normal modal logics are defined by axioms of modal degree 1. In this paper we use calculations with normal forms to determine the set of all possible non-iterative normal modal logics, unimodal propositional extensions of K.…
The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with…
In the first part of this paper we analyzed finite non-deterministic matrix semantics for propositional non-normal modal logics as an alternative to the standard Kripke's possible world semantics. This kind of modal systems characterized by…