Re: [CL] Re: Decidability
Norbert,
Brandon's note requires a more complex answer,
and I'll comment on it later. But your question
is easier to answer:
> Are Horn clauses really decidable in first-order logic?
That depends. If you have Horn clauses with predicates
whose definitions are complex, then it is undecidable.
However, there is a subset called Datalog, which is
essentially what is used in SQL, and that is decidable.
What makes it decidable is that all predicates are
defined, directly or indirectly, by tables (i.e.,
collections of ground-level assertions).
There is another very important subset in which
the predicates are defined by primitive recursion
(in which the maximum number of steps in any
computation can be predicted by a simple function).
However, there are very complex functions, such
as Ackermann's function and the Busy Beaver function,
which take a finite number of steps, but that finite
number requires much more than exponential time to
compute. There are also functions and predicates
whose termination is undeciable. If those predicates
are used in Horn-clause logic, then all bets are off.
However, very, very few people use predicates that
require more than primitive-recursive power to compute,
and those few people are undoubtedly smart enough to
know what they're doing. I see absolutely no reason
to prevent smart people from doing something that
they make a conscious decision to do. Anybody who
wants to define Ackermann's function or the Busy
Beaver function is either a sophisticated researcher
or a student who has been assigned a homework exercise.
Bottom line: I would recommend Horn-clause logic with
well-founded semantics and arbitrary definitional power
as the basic rule language.
John Sowa