Skip to main content
added 303 characters in body
Source Link

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 by Behmann and Loewenheim.

Regarding the first question, I do not know what is the complexity of model enumeration, but satisfiability checking is NExpTime-complete (check "The Classical Decision Problem" book), while the satisfiability problem for FO1 is NP-complete. Hence, even if the model enumeration is in P for 2-variable logic (a superset of FO1) it does not imply that the same bound holds for MFO, since the translation from MFO to FO1 might require an exponential blowup in the size of an input formula.

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 by Behmann and Loewenheim.

Regarding the first question, I do not know what is the complexity of model enumeration, but satisfiability checking is NExpTime-complete (check "The Classical Decision Problem" book).

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 by Behmann and Loewenheim.

Regarding the first question, I do not know what is the complexity of model enumeration, but satisfiability checking is NExpTime-complete (check "The Classical Decision Problem" book), while the satisfiability problem for FO1 is NP-complete. Hence, even if the model enumeration is in P for 2-variable logic (a superset of FO1) it does not imply that the same bound holds for MFO, since the translation from MFO to FO1 might require an exponential blowup in the size of an input formula.

Source Link

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 by Behmann and Loewenheim.

Regarding the first question, I do not know what is the complexity of model enumeration, but satisfiability checking is NExpTime-complete (check "The Classical Decision Problem" book).