Questions tagged [first-order-logic]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
-1 votes
0 answers
32 views

corresponding resoving and arbitary resolving

Notations: $$C_x \otimes C_{\bar{x}} = V_1 \lor \ldots \lor V_a \lor W_1 \lor \ldots \lor W_b$$ $$ \text{ where } C_x = x \lor V_1 \lor \ldots \lor V_a \text{ and } C_{\bar{x}} = \bar{x} \lor W_1 \lor ...
Jxb's user avatar
  • 315
-3 votes
1 answer
98 views

Can one do descriptive complexity theory using abstract state machines?

I learned about ASM recently and was interested how it could used for descriptive complexity theory. Such link seems natural to me: you can give construction of algebraic model for formula as an ASM. ...
uhbif19's user avatar
  • 295
1 vote
0 answers
47 views

Elimination of monadic second-order quantifiers

I'm trying to understand what is currently known to be possible regarding the elimination of monadic second-order quantifiers. Many sources cite that monadic second-order logic supports elimination of ...
Nicola Gigante's user avatar
2 votes
1 answer
73 views

Second-order reachability in second-order logic

By second-order reachability I mean a second-order lifting of the reachability problem on first-order structures. So let $R(X,Y)$ be a second-order binary predicate (i.e. it links a set of elements $X$...
Nicola Gigante's user avatar
0 votes
2 answers
66 views

Inexpressibility results for first-order logic that fail extending the language

Think of the classical inexpressivity results that one studies in early courses about first-order logic, e.g. that on a signature with a binary predicate $R$ one cannot express that $R$ is connected. ...
Nicola Gigante's user avatar
4 votes
1 answer
52 views

References on second-order quantifier elimination and related topics

I was wondering whether something like elimination of second-order quantifiers exist, and indeed it seems it does. I've found there's a workshop on this topic, and the webpage describes exactly what I ...
Nicola Gigante's user avatar
0 votes
0 answers
64 views

Number of quantifier alternations in prenex form of a formula

I'm currently studying hyperlogics and in particular HyperLTL/CTL*. In model checking algorithms for such logics the number of quantifier alternations appearing in a formula can play an important role ...
timtombobjohn's user avatar
1 vote
0 answers
73 views

Do soundness and completeness need to be exact converses of eachother?

This question concerns the derivational soundness and completeness of the first-order proof system LK (without equality) as presented in Logical Foundations of Proof Complexity by Cook and Nguyen. In ...
Johnny's user avatar
  • 201
1 vote
1 answer
75 views

Why isn't the proof obtained using Buss's proof of the derivational completeness of LK anchored?

The version of Buss's proof I'm referring to is the proof of Lemma II.2.24 in Logical Foundations of Proof Complexity by Cook and Nguyen. In the interest of keeping this question self-contained I've ...
Johnny's user avatar
  • 201
0 votes
1 answer
91 views

Number of equivalent formulas in a function-free first order logic language?

In this paper by Martin Grohe, in the first paragraph of section 4.1, it says: "because upto logical equivalence there only exist finitely many $FO[\rho]$ formulas of quantifier rank at most $q$ ...
SagarM's user avatar
  • 706
0 votes
1 answer
66 views

Resources for first-order and second-order monadic logics with a model-checking objective

What are some good books and surveys for learning about first-order logic and monadic second-order logic? I'm a graduate student in computer science with a focus on algorithms. For model-checking on ...
fva's user avatar
  • 45
0 votes
1 answer
86 views

reducing this problem to a decision problem

Before I can define my problem, let's make a simple definition. An expression $e$ is a conjunction of inequalities of the form $x~ op~ v$ where: $x$ is a variable, $op\in[<,>,\leq,\geq,=]$, and $...
mahou_2019's user avatar
1 vote
0 answers
149 views

What is the model of computation that corresponds (in the manner of Curry-Howard) to the deduction rule of resolution?

The Curry-Howard Correspondence is well-documented for the isomorphism which associates the intuitionistic natural deduction proof calculus (logic side) with the type system for the simply typed ...
jpt4's user avatar
  • 81
4 votes
0 answers
82 views

Are there classes for that FO-model checking is FPT on hypergraphs?

For graphs, there are many classes that admit FPT-algorithms for model checking of first order logic, e.g. the class of nowhere dense graphs by Grohe et. al. Are there similar results for ($k$-uniform)...
embie27's user avatar
  • 41
3 votes
3 answers
502 views

Evaluating asymptotic probabilities of First Order Logic Formulas?

0-1 Laws in first order logic state that the probability of a FOL sentence $\Phi$, defined as follows: $$P(\Phi) = \frac{|\{\omega \in \Omega^{n}:\omega \models \Phi\}|}{|\Omega^{n}|} $$ where $\Omega^...
SagarM's user avatar
  • 706
9 votes
1 answer
150 views

Validity problem of intuitionistic two-variable logic

The two-variable fragment $\mathrm{FO}^2$ consist of those sentences of first-order logic $\mathrm{FO}$ in which precisely two variables occur (e.g. $\exists x \exists y \exists z R(x,y,z)$ is not a ...
Reijo Jaakkola's user avatar
3 votes
2 answers
151 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
Hao S's user avatar
  • 186
2 votes
2 answers
150 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 ...
Nicola Gigante's user avatar
2 votes
1 answer
217 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 ...
SagarM's user avatar
  • 706
0 votes
0 answers
52 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 ...
SagarM's user avatar
  • 706
2 votes
2 answers
218 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 ...
Evan Aad's user avatar
  • 354
1 vote
0 answers
104 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 ...
SagarM's user avatar
  • 706
2 votes
0 answers
171 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.
Bartosz Bednarczyk's user avatar
2 votes
1 answer
182 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 ...
SagarM's user avatar
  • 706
3 votes
1 answer
180 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 ...
SagarM's user avatar
  • 706
9 votes
1 answer
332 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 ...
SagarM's user avatar
  • 706
1 vote
2 answers
190 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 ...
SagarM's user avatar
  • 706
1 vote
0 answers
104 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 ...
SagarM's user avatar
  • 706
6 votes
3 answers
597 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, ...
SagarM's user avatar
  • 706
7 votes
1 answer
370 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 ...
Faustus's user avatar
  • 193
4 votes
1 answer
219 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 ...
Evan Aad's user avatar
  • 354
4 votes
1 answer
143 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(...
Evan Aad's user avatar
  • 354
6 votes
0 answers
390 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 ...
Joey Eremondi's user avatar
11 votes
0 answers
219 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 ...
user3483902's user avatar
  • 1,181
3 votes
0 answers
47 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 ...
StefanH's user avatar
  • 2,037
1 vote
0 answers
142 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 ...
Geckabor's user avatar
12 votes
2 answers
456 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. ...
Joey Eremondi's user avatar
12 votes
1 answer
277 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}] (...
Samuel Schlesinger's user avatar