Questions tagged [first-order-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
12
votes
1answer
254 views

For any two non-isomorphic graphs $G, H$, does there exist a polysize, polylog quantifier depth first order formula which witnesses this?

I want to be very specific. Does anyone know of a disproof or a proof of the following proposition: $\exists p \in \mathbb{Z}[x], n, k, C \in \mathbb{N},$ $\forall G, H \in STRUC[\Sigma_{graph}] (...
11
votes
2answers
440 views

State of the Art for the Monadic Class?

Monadic First Order Logic, also known as the Monadic Class of the Decision Problem, is where all predicates take one argument. It was shown to be decidable by Ackermann, and is NEXPTIME-complete. ...
10
votes
0answers
176 views

Descriptive Complexity characterzation of BPP

We know of descriptive complexity characterizations of classes such as P, and NP, which use First Order logic, and operators. Does BPP have a characterization under descriptive complexity, too(any ...
9
votes
1answer
269 views

Existing implementation of Scott's reduction?

As per this paper by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in $\mathrm{FO^2}$, In order to do this they use Scott's reduction. Which is the ...
7
votes
1answer
276 views

Kleene Algebra for star-free regular expressions

TLDR: Is there a notion of Kleene Algebra for star-free regular expressions? Kleene Algebras are algebraic structures that are equivalent to regular expressions. A Kleene Algebra is an idempotent ...
6
votes
3answers
436 views

Can modern SAT-Solvers utilise the symmetry of First Order Logic?

Apologies if the question is trivial or is wrongly stated, I am a Physicist! Assuming that we have a universally quantified first-order logic sentence, all variables are universally quantified, ...
6
votes
0answers
285 views

Reverse Skolemization?

I'm wondering if there are any references on "reverse skolemization", that is, converting a formula with functions into one purely consisting of quantifiers by eliminating function applications. I'm ...
4
votes
1answer
159 views

The theory of definitions in first order logic

I'm looking for a clear and thorough treatment of the theory of definitions in first order predicate logic from a syntactic/proof theoretic point of view (as opposed to semantic/model theoretic point ...
4
votes
1answer
125 views

A first order logic extended with binding terms like the familiar set descriptors $\{x:\varphi\}$

First order logic comes equipped with two kinds of terms: Variable: those terms of the form $x$ for some variable $x$, of which there are infinite. Function application: those terms of the form $f(...
3
votes
2answers
135 views

Looking for some lecture videos on logic, models of computation and computational complexity/tcs fundamentals [closed]

Looking for some lecture videos (introductory level) on logic, models of computation as well as computational complexity/ other theoretical computer science fundamentals
3
votes
1answer
140 views

Normal forms for counting quantifiers?

In the paper by [Erich Grädel and Martin Otto], the authors state that any formula in First Order Logic with two variables with counting quantifiers can be reduced to a formula of the form $$ \forall ...
3
votes
0answers
46 views

Extending the sequential calculus (logic over words) to allow a hierarchy of languages like the arithmetical hierarchy

Let $\Sigma$ be some finite alphabet. Then consider the logical language $\mathcal L = \{ R_a : a \in \Sigma \} \cup \{ <,= \}$ and first order formulas. For a given first order formula $\varphi$ a ...
2
votes
2answers
155 views

A clear and rigorous explanation of critical pairs and the Knuth-Bendix completion algorithm?

I'm looking for an explanation of critical pairs and the Knuth-Bendix completion algorithm that is at once rigorous and of high pedagogical value, i.e. clear, detailed, containing illustrative ...
2
votes
1answer
149 views

Is Scott's reduction sound for $\mathrm{FO}^2$ with equality?

As per this paper by Grädel, Kolaitis and Moshe Vardi, they discuss computational complexity of satisfiability problem in $\mathrm{FO^2}$, In order to do this they use Scott's reduction. Which is the ...
2
votes
2answers
100 views

Tableau method for two-variable first-order logic

$FO^2$, i.e. two-variable first-order logic, has a NEXPTIME-complete satisfiability problem (see Grädel, Kolaitis and Vardi '97). However, the decidability and complexity of this fragment is proved by ...
2
votes
1answer
97 views

Scott's normal form for $\exists y \forall x R(x,y) $

In this paper Scott's reduction is discussed, which reduces any FO2 formula to Scott's Normal form. As far as I understand the reduction process explained in the paper can get you to formulas with ...
2
votes
0answers
162 views

Order-invariant conjunctive queries are FO-definable without the order

I'm looking for a reference for Exercise 6.11 from Libkin's FMT book: Prove that an order-invariant conjunctive query is FO-definable without the order relation. All help is appreciated.
1
vote
2answers
140 views

Complexity of Model Enumeration in function free, equality free, First Order Logic with only Unary Predicates?

This question has inspired the following two questions. Given a first order logic language, with only unary predicates, finite number of variables, $\forall$ and $\exists$ i.e no equality and ...
1
vote
0answers
99 views

How does complexity of a counting problem influence wether it admits a closed form formula or not?

In https://arxiv.org/abs/1412.1505, the section "Results on Data Complexity" mentions the fact that since the authors are about to proove $\#P_1$ complexity for weighted model counting in ...
1
vote
0answers
73 views

Constructing FOL formula for which counting is easy?

Given a function free First Order Logic language $\mathcal{L}$ are there ways to write formulas for which counting the number of models for a given cardinality of the domain is easy (preferably exists ...
1
vote
0answers
119 views

Proof of SAT is complete for NP via first-order reductions

So I have been reading this: https://people.cs.umass.edu/~immerman/book/ch7.pdf I do not understand the proof of theorem 7.16, which says that SAT is complete for NP via first-order reductions. My ...
0
votes
0answers
49 views

How and How fast can we infer a logical formula that expresses a given graph in C$^2$( logic with 2 vars and counting quantifiers)?

In the following paper the author's claim that almost all graphs can be expressed in first order logic with counting quantifiers and two variables. I would like to know, is there any algorithm that ...
-3
votes
1answer
125 views

Logic of counting elements of the domain [closed]

I need to describe a logic of counting elements of the domain: in each model, the function outputs the number of elements in the domain of the model. What kind of function(s) shall be in the signature?...