Re: decidable fragments of first order logic?



Frederick Williams wrote:
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.

A short paper by Gurevich gives an overview of the situation at

http://research.microsoft.com/~gurevich/Opera/91.pdf

but this file won't open for me in Adobe or Ghostscript. The
author was kind enough to send me a Postscript file which works
fine. I'll email it to anyone who wants it; just let me know
by post or email.

--
hz
.

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?
    ... 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)
  • 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?
    ... Marshall schrieb: ... decision procedure if all predicates have arity 1, ... Are there other fragments of FOL that are decidable? ...
    (sci.logic)