Re: [CL] Re: Decidability
John F. Sowa wrote:
> 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.
Yes that's right. I was thinking of a pure Horn language
built on 1st-order logic, where predicates are only defined
in terms of further Horn clauses including ground facts.
If predicates are given more complex meaning, such as being
interpreted as arithmetical relations, the language could
easily become undecidable. Thus, Prolog will be undecidable
if its usual in-built predicates and functions are used.
Datalog (I belive, though I don't know that much about it)
is close to pure Horn logic with only very restricted
built-in functionality, which maintains decidabilty.
Best regards
Brandon
>
> 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
>
--
===============================================================
Dr Brandon Bennett
Division of Artificial Intelligence Tel.: +44 (0)113 343 1070
School of Computing (room 9.16) (home) +44 (0)113 274 6920
University of Leeds Fax.: +44 (0)113 343 5468
Leeds LS2 9JT E-mail: brandon@comp.leeds.ac.uk
United Kingdom WWW: http://www.comp.leeds.ac.uk/brandon/
===============================================================