On two-variable guarded fragment logic with expressive local Presburger constraints [PDF]
Logical Methods in Computer Science, 2022 We 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 ...
Chia-Hsuan Lu, Tony Tan
doaj +4 more sources
On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics [PDF]
Logical Methods in Computer Science, 2021 We present syntactic characterisations for the union closed fragments of existential second-order logic and of logics with team semantics. Since union closure is a semantical and undecidable property, the normal form we introduce enables the handling and
Matthias Hoelzel, Richard Wilke
doaj +5 more sources
The succinctness of first-order logic on linear orders [PDF]
Logical Methods in Computer Science, 2005 Succinctness is a natural measure for comparing the strength of different logics. Intuitively, a logic L_1 is more succinct than another logic L_2 if all properties that can be expressed in L_2 can be expressed in L_1 by formulas of (approximately) the ...
Martin Grohe, Nicole Schweikardt
doaj +6 more sources
A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic
International Conference on Computer Aided Verification, 2017 We consider the satisfiability problem for a fragment of separation logic including inductive predicates with shape and arithmetic properties. We show that the fragment is decidable if the arithmetic properties can be represented as semilinear sets.
Quang Loc Le +3 more
openalex +3 more sources
A Fragment of Dependence Logic Capturing Polynomial Time [PDF]
Logical Methods in Computer Science, 2014 In this paper we study the expressive power of Horn-formulae in dependence logic and show that they can express NP-complete problems. Therefore we define an even smaller fragment D-Horn* and show that over finite successor structures it captures the ...
Johannes Ebbing +3 more
doaj +2 more sources
Propositional Logics Complexity and the Sub-Formula Property [PDF]
Electronic Proceedings in Theoretical Computer Science, 2015 In 1979 Richard Statman proved, using proof-theory, that the purely implicational fragment of Intuitionistic Logic (M-imply) is PSPACE-complete.
Edward Hermann Haeusler
doaj +5 more sources
On decidability of a fragment of intuitionistic predicate logic
Lietuvos Matematikos Rinkinys, 1999 There is not abstract.
Jolanta Kaušilaitė +1 more
doaj +4 more sources
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 Kieronski
doaj +3 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 +3 more sources
Decision procedure for a fragment of quantified branching temporal logic
Lietuvos Matematikos Rinkinys, 2002 There is not abstract.
Aida Pliuškevičienė
doaj +4 more sources