Re: decidable fragments of first order logic?

herbzet wrote:

Marshall wrote:

As I understand it, first order logic in general is not decidable.
However various fragments of FOL are decidable. There's a
decision procedure if all predicates have arity 1, for example.

Are there other fragments of FOL that are decidable?
Are the limits of decidable fragments known? Which
raises the question for me of whether it might be possible
to characterize the "size" of a decidable fragment, and
then ask what the "largest" such fragment might be.

Answers, discussion, and/or pointers to further reading welcome.

Marshall

"Solvable Cases of the Decision Problem" by W. Ackermann
North-Holland Publishing Company [1954]

is an older work on the subject.

And "The Classical Decision Problem" by B Borger, B Gradel and Y
Gurevich, Springer-Verlag is a newer one.

--
How unlike the home life of our own dear Queen.
Remove "antispam" and ".invalid" for e-mail address.
.

Relevant Pages

  • Re: decidable fragments of first order logic?
    ... decision procedure if all predicates have arity 1, ... Are there other fragments of FOL that are decidable? ... Any sufficiently weak first-order theory is decidable. ...
    (sci.logic)
  • Re: decidable fragments of first order logic?
    ... Marshall wrote: ... decision procedure if all predicates have arity 1, ... Are there other fragments of FOL that are decidable? ...
    (sci.logic)
  • Re: decidable fragments of first order logic?
    ... decision procedure if all predicates have arity 1, ... Are there other fragments of FOL that are decidable? ...
    (sci.logic)
  • Re: decidable fragments of first order logic?
    ... decision procedure if all predicates have arity 1, ... Are there other fragments of FOL that are decidable? ... On the elemential level, the atomic life along its scale becomes ...
    (sci.logic)
  • Re: decidable fragments of first order logic?
    ... Are there other fragments of FOL that are decidable? ... Examples of theories that have been shown *decidable* using quantifier elimination are Presburger arithmetic, real closed fields, atomless Boolean algebras, term algebras, dense linear orders, random graphs, Feature trees, as well as many of their combinations such as Boolean Algebra with Presburger arithmetic, and Term Algebras with Queues. ... Quantifier elimination can also be used to show that "combining" decidable theories leads to new decidable theories. ...
    (sci.logic)