Search results for "NEXPTIME"

showing 3 items of 3 documents

Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants

2018

We consider extensions of the two-variable guarded fragment, GF2, where distinguished binary predicates that occur only in guards are required to be interpreted in a special way (as transitive relations, equivalence relations, pre-orders or partial orders). We prove that the only fragment that retains the finite (exponential) model property is GF2 with equivalence guards without equality. For remaining fragments we show that the size of a minimal finite model is at most doubly exponential. To obtain the result we invent a strategy of building finite models that are formed from a number of multidimensional grids placed over a cylindrical surface. The construction yields a 2NExpTime-upper bou…

FOS: Computer and information sciencesComputer Science - Logic in Computer ScienceTwo-variable logicGeneral Computer ScienceComputational complexity theoryLogicguarded fragmentBinary number0102 computer and information sciences01 natural sciencesUpper and lower boundsTheoretical Computer ScienceCombinatoricstransitive relationEquivalence relationfinite satisfiability problem0101 mathematicsEquivalence (formal languages)Integer programmingMathematicsDiscrete mathematicsTransitive relationNEXPTIMEcomputational complexity010102 general mathematicsLogic in Computer Science (cs.LO)Computational Mathematics010201 computation theory & mathematicsequivalence ralationACM Transactions on Computational Logic
researchProduct

On Horn spectra

1991

Abstract A Horn spectrum is a spectrum of a Horn sentence. We show that to solve Asser's problem, and consequently the EXPTIME = ? NEXPTIME question it suffices to consider the class of Horn spectra. We also pose the problem whether or not the generator of every Horn spectrum is a spectrum. We prove that from a negative solution of the generator problem, a negative answer for the EXPTIME = ? NEXPTIME question follows. Some other relations between the generator problem and Asser's problem are given. Finally, the relativized version of the generator problem is formulated and it is shown that it has an affirmative solution for some oracles, and a negative solution for some others.

Class (set theory)NEXPTIMEGeneral Computer ScienceFrench hornComputabilitySpectrum (functional analysis)EXPTIMEOracleTheoretical Computer ScienceCombinatoricsComputer Science::Logic in Computer ScienceComputer Science::Formal Languages and Automata TheoryComputer Science(all)Generator (mathematics)MathematicsTheoretical Computer Science
researchProduct

The fluted fragment revisited

2019

AbstractWe study the fluted fragment, a decidable fragment of first-order logic with an unbounded number of variables, motivated by the work of W. V. Quine. We show that the satisfiability problem for this fragment has nonelementary complexity, thus refuting an earlier published claim by W. C. Purdy that it is in NExpTime. More precisely, we consider ${\cal F}{{\cal L}^m}$, the intersection of the fluted fragment and the m-variable fragment of first-order logic, for all $m \ge 1$. We show that, for $m \ge 2$, this subfragment forces $\left\lfloor {m/2} \right\rfloor$-tuply exponentially large models, and that its satisfiability problem is $\left\lfloor {m/2} \right\rfloor$-NExpTime-hard. We…

Logic0102 computer and information sciencesQuine01 natural sciences68Q17Fragment (logic)0101 mathematicstransitivityMathematicsfirst-order logicDiscrete mathematicsTransitive relationNEXPTIME010102 general mathematicsdecidabilityfluted fragmentSatisfiabilityDecidabilityFirst-order logicPhilosophysatisfiability010201 computation theory & mathematicssatisfabilityBoolean satisfiability problemcomplexityJournal of Symbolic Logic
researchProduct