# Questions tagged [first-order-logic]

The tag has no usage guidance.

19 questions
Filter by
Sorted by
Tagged with
46 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 ...
139 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 ...
83 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 ...
142 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.
123 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 ...
122 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 ...
177 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 ...
127 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 ...
69 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 ...
317 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, ...
239 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 ...