2022 Developer Survey is open! Take survey.

# Tag Info

Accepted

### Existing implementation of Scott's reduction?

You might check the FO2 solver by Tomer Kotek et. al (ICDT 2017): https://forsyte.at/alumni/kotek/fo2-solver/ as well as an FO2 solver by Tony Tan and his students (LICS 2021): https://arxiv.org/abs/...
• 1,110
Accepted

• 1,112

### Tableau method for two-variable first-order logic

You might check the FO2 solver by Tomer Kotek: https://forsyte.at/alumni/kotek/fo2-solver/ This is the only existing FO2 solver (Tony Tan with his student have a paper under submission, in which they ...
• 1,110

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

There is a rather technically-detailed description to be found in any of the following: D.F. Holt, D.B.A. Epstein, and S. Rees. The use of knuth-bendix methods to solve the word problem in automatic ...

### State of the Art for the Monadic Class?

In a 1993 LICS paper, Bachmair, Ganzinger and Waldmann showed that set constraints are equivalent to monadic FOL, in Set Constraints are the Monadic Class. If memory serves, set constraints are ...
• 31.6k

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

Reading the discussion below the other answer made me realize that it’s not immediately obvious what is the complexity of translation of FO sentences in this language to equivalent FO1 sentences. ...
• 14.7k
1 vote
Accepted

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

Answering your second question, the logic you mean is known as Monadic FO or Monadic Predicate Calculus. It is known the logic is equivalent to FO1 (as Emil Jeřábek suggested) by some very old works ...
• 1,110
1 vote

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

I take that by "symmetry" we are talking about reasoning over the generalities in a first-order formula instead of grounding all the possible assignments. I may be misinterpreting the ...

Only top scored, non community-wiki answers of a minimum length are eligible