On two-variable guarded fragment logic with expressive local Presburger constraints [PDF]
Logical Methods in Computer ScienceWe consider the extension of the two-variable guarded fragment logic with local Presburger quantifiers. These are quantifiers that can express properties such as "the number of incoming blue edges plus twice the number of outgoing red edges is at most ...
Chia-Hsuan Lu, Tony Tan
doaj +1 more source
Alternating Quantifiers in Uniform One-Dimensional Fragments with an Excursion into Three-Variable Logic [PDF]
Logical Methods in Computer ScienceThe uniform one-dimensional fragment of first-order logic was introduced a few years ago as a generalization of the two-variable fragment to contexts involving relations of arity greater than two.
Oskar Fiuk, Emanuel Kieroński
openalex +2 more sources
Loop-free verification of termination of derivation for a fragment of dynamic logic
Lietuvos Matematikos Rinkinys, 2008 A fragment of a deterministic propositional dynamic logic (DPDL, in short) is considered The language of considered fragment contains propositional symbols, action constants, action operator (repetition) and logical symbols.
Regimantas Pliuškevičius
doaj +1 more source
A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking [PDF]
Electronic Proceedings in Theoretical Computer Science, 2011 Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and continuous time, respectively.
Takashi Tomita +2 more
doaj +1 more source
Ordered fragments of first-order logic [PDF]
arXiv, 2021 Using a recently introduced algebraic framework for the classification of fragments of first-order logic, we study the complexity of the satisfiability problem for several ordered fragments of first-order logic, which are obtained from the ordered logic and the fluted logic by modifying some of their syntactical restrictions.
arxiv
From formulas to cirquents in computability logic [PDF]
Logical Methods in Computer Science, 2011 Computability logic (CoL) (see http://www.cis.upenn.edu/~giorgi/cl.html) is a recently introduced semantical platform and ambitious program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth that logic ...
Giorgi Japaridze
doaj +1 more source
One-Sided Sequent Systems for Nonassociative Bilinear Logic: Cut Elimination and Complexity
Bulletin of the Section of Logic, 2021 Bilinear Logic of Lambek amounts to Noncommutative MALL of Abrusci. Lambek proves the cut–elimination theorem for a one-sided (in fact, left-sided) sequent system for this logic.
Paweł Płaczek
doaj +1 more source
Complexity of the variable-free fragment of the weak Grzegorczyk logic [PDF]
arXiv, 2022 The paper proves PSPACE-hardness of variable-free fragments of all logics between K and wGrz.
arxiv
Lindstrom theorems for fragments of first-order logic [PDF]
Logical Methods in Computer Science, Volume 5, Issue 3 (August 3,
2009) lmcs:895, 2009 Lindstr\"om theorems characterize logics in terms of model-theoretic conditions such as Compactness and the L\"owenheim-Skolem property. Most existing characterizations of this kind concern extensions of first-order logic. But on the other hand, many logics relevant to computer science are fragments or extensions of fragments of first-order logic, e.g.,
arxiv +1 more source
Covering and separation for logical fragments with modular predicates [PDF]
Logical Methods in Computer Science, 2019 For every class $\mathscr{C}$ of word languages, one may associate a decision problem called $\mathscr{C}$-separation. Given two regular languages, it asks whether there exists a third language in $\mathscr{C}$ containing the first language, while being ...
Thomas Place +2 more
doaj +1 more source