Re: Decidability
John and Norbert,
I just checked up on Horn logic and it seems I was
mistaken about this. It is in general only semi-decidable
same as the full 1st-order logic. In fact Horn formulae
(ie conjunctions of Horn clauses) form a reduction class
for 1st-order logic --- meaning that their is a validity
preserving recursive function from the set of all 1st-order
formulae to the set of Horn formulae.
To get decidability you would need to restrict the quantifier
prefix structure, or equivalently the functional forms
in Skolemised form. But there are many useful Horn theories
that are decidable.
Probably you know the book "The Classical Decision Problem"
by B"orger, Gr"adel and Gurevich (Springer). This gives
a complete classification of decidable fragments of 1st-order
logic and is a useful, though very dense, reference.
I have added a couple of further comments below responding
to some of John's points.
John F. Sowa wrote:
> BB>... I would say that decidability is not something
> > that should be sought at all cost. In fact it seems
> > likely that any language sufficient to represent
> > anything like the richness of human thought must be
> > undecidable.
>
> I agree. But I would add that the words "decidable"
> and "undecidable" are inappropriate as modifiers of
> a language.
Yes, strictly that's right. But, applied to a language,
"decidable" normally means that the class of problems
of determining entailments in the language is undecidable
(or that the class of problems of testing theoremhood
is undecidable -- which is usually an equivalent problem).
> It is better to use them to characterize
> problems.
Well, if we want to be very strict, we should say that
undecidability only applies to classes of problems;
and in fact only to infinite classes of problems.
Any single problem or finite class of problems is
decidable, since there is an algorithm which can
give the answer in finite time (in fact a simple
lookup table will do it in constant time).
> As I said in my first note on this topic, all major
> programming languages (C, Ada, Java, C++, C#, Perl,
> Python, PHP, LISP, Prolog, etc.) allow programs to
> be expressed whose termination is undecidable. But
> nobody has ever said that property is a defect.
Yes termination of any general purpose programming language
is undecidable --- this can be seen as a consequence of
their generality. However, we do not write programs in
order that they be tested for termination. Programs are
written to solve other problems and we generally want them
to give an answer in finite time. Thus it is very useful
to know whether a class of target problems is decidable
or undecidable.
If undecidable we know we can never construct an algorithm
(in any programing language) which will terminate for
all problem instances in finite time).
Hence we must either switch attention to a simpler sub-class of
problems, which might still be quite useful to solve, or
we must put up with the possibility that our algorithm
won't necessarily terminate.
In the latter case we can either set a time limit and
just return "don't know" after that time, or we could
just leave it running indefinitely waiting to see if it
does eventually give a solution (fine for a research
problem, but probably doesn't make sense in any commercial
application).
> BB> However for processing and computation, decidability
> > is undoubtedly of utmost importance -- much more
> > important than the lower complexity boundaries,
> > I would say.
>
> Decidability of what? The language? A particular
> problem? I certainly agree that there is no point in
> letting a program run forever on a problem that will
> never terminate. But what if you have a problem whose
> termination is unknown? Perhaps you might want to let
> the program run over the weekend to see what happens.
I've already responded to these points above.
> BB> The main problem is of course that if I am really dealing
> > with a truly undecidable problem (such as computing
> > entailment) in some language), I cannot even write an
> > algorithm to do this. If I have a semi-decidable language,
> > the situation is very slightly better because at least
> > I have a test for positive cases -- but it's not much
> > better, because the complexity of this test is not
> > bounded by any function (so neither time nor memory
> > requirement are bounded).
>
> What are you saying? Do you mean that nobody should ever
> try to prove a theorem before proving that it's provable?
> Look at the _Principia Mathematica_. Whitehead and Russell
> proved a lot of theorems without knowing anything about the
> issues of undecidability, and it turns out that all their
> theorems can be proved in a few seconds with modern theorem
> provers. (Of course, there are probably many others that
> they couldn't prove, but they never put them in their book.)
Here you are talking about specific problem instances.
Clearly one can solve any particular problem. But there
are certainly (infinite) problem classes for which it
is impossible to construct a general solution algorithm.
> Look at the TPTP web site with thousands of problems for
> theorem provers. Many of those problems are expressed
> in full first-order logic, but they're provable. Why
> should people give up before they try them?
Well, 1st-order logic is semi-decidable, so any theorem
is provable in finite time.
Again, it's the class of problems, not the individual
problem that is undecidable.
> I completely agree with the following:
>
> BB> However, in many cases the complexity class does not
> > directly affect the practical scalability. This is because
> > complexity classes deal in worst cases. These typically
> > arise quite rarely compared to the average case. Thus it
> > may well be that a cubic algorithm works pretty well in
> > almost all cases (and hence could be perfectly acceptable
> > to web users who seem remarkably tolerant to systems that
> > don't always work).
>
> I would add that what's available on the web is so incomplete
> and so rife with errors that users have much more serious
> problems to worry about than the completeness or decidability
> of their proof procedures.
>
> BB> Thus the halting problem is solvable for "pure" Prolog
> > programs (but not if one uses the various messy stuff
> > that makes real programming possible).
>
> No. You can simulate a Turing machine in pure Prolog, for
> which the TM "tape" is expressed as a Prolog list. Then
> you can give it a tape that expresses an undecidable
> program. If you can't prove that the TM will halt, then
> you can't prove that the Prolog simulation of it will halt.
You are right. I was mistaken about that.
> BB> So the clever Prolog programmer does not tame the
> > undecidable but rather steers around the exponential.
>
> The Prolog programmer, like a programmer who uses any other
> language, steers around both exponential and undecidable
> problems. They've been doing that for over 50 years. Now
> web programmers have to steer around polynomial problems.
I pretty much agree with that.
However, most ordinary programs only tackle problem classes that
are at worst polynomial. Exponential problem classes are tackled
in domains such as scheduling. And undecidable classes are
generally not tackled, except in automated reasoning and
symbolic AI.
> And on the topic of Horn-clause logic, I would like to
> recommend the following note I sent to these lists four
> years ago. Note the discussion of how Bill Andersen and
> his colleagues dealt with 5532 axioms taken from Cyc, of
> which 84% of them could be expressed in hte Horn-clause
> subset. I highly recommend that approach.
It's certainly true that Horn Clauses are much better
computationally and have a pretty high expressive power.
I use them all the time since I am a heavy user of Prolog.
However, there are lots of things that can't be said in
Horn form (eg stuff like Px -> (Qx v Rx)).
So, although it may be a good idea to give Horn clause
modules special status and treatment within an ontology,
one will generally also have to include non-Horn information.
Best regards
Brandon
> John Sowa
> ____________________________________________________________
>
> Enrico,
>
> I think we agree about the nature of completeness and its importance
> for many kinds of reasoning. The differences in our points of view
> seem to result from different assumptions about the relationships
> between the ontology, the reasoning methods, and the kinds of problems
> to be solved.
>
> In your note, you seem to assume that there is one and only one
> kind of reasoning method that can be used with a given ontology:
>
> EF>Well, if you are a serious computer scientist, you should warn the
> >military agency that they can not use the same ontology to achieve
> >both tasks. You have to tell them that it is impossible to use your
> >(incomplete) logic-based system to solve a problem and its dual
> >at the same time.
>
> This is a very different assumption from the Cyc philosophy that Fritz
> Lehmann was discussing. Cyc has one very large ontology with many
> different reasoning methods that can be used with it to solve different
> kinds of problems. You seem to assume a different ontology for each
> kind of reasoning method.
>
> Since I'm not exactly sure what position either you or Fritz is
> advocating, let me explain the position that I would recommend
> for a large number of different kinds of problems:
>
> 1. Start with a large ontology stated in a very expressive version
> of logic, which includes at a minimum all of first-order logic.
> I would add metalevel and higher-order extensions for reasoning
> about the first-order axioms, selecting which ones to use for a
> given problem, and even revising the axioms in some cases.
>
> 2. At this point, I believe that Fritz and I would agree, but you are
> probably waving your hands to protest that the reasoning methods
> that would apply to such a logic would have to be intractable,
> incomplete, undecidable, etc. I think that both Fritz and I would
> agree with you. The difference is that Fritz says that he doesn't
> care, but I care more than he does. My position is somewhere
> between you and Fritz. I sympathize with your concerns, but I
> believe that there are ways of dealing with them in a way that is
> logically sound and with suitable guarantees to the users (the
> military authorities in your example).
>
> 3. The point I want to emphasize is that intractability is not a
> property of the logic, but a property of the problems you are
> trying to solve. An NP-complete problem will be NP-complete
> in any logic you use. Restricting the logic will not solve the
> problem -- it will just make it impossible to state the problem.
> Similarly, a polynomial-time problem is going to take polynomial
> time in any logic. If you can solve it in polynomial time with
> description logics or Horn-clause logics, a full FOL theorem
> prover, such as Otter, will also solve it in polynomial time
> (I will admit that a more restricted theorem prover may be able
> to solve some problems faster, but Otter has a variety of methods
> that it can choose for different problems. Even though it always
> uses full FOL to state the problem, it can automatically choose
> a more restricted method when it is suitable.)
>
> 4. There are many problems that require the full expressive power of
> FOL but can be solved in polynomial time. An example is answering
> an SQL query in terms of a relational database. The SQL query
> language has the expressive power of FOL, but any SQL query
> can be evaluated against a relational DB in polynomial time with
> an exponent that is less than or equal to the maximum number of
> quantifiers in the query. The world economy depends on such
> problems being solved billions of times a day.
>
> 5. One approach that I highly recommend started with the Cyc KB,
> which is probably the largest axiomatized KB ever developed.
> The developers (Petersen, Andersen, and Engel, see ref. below)
> used the full Cyc system to develop an application, but they
> wanted to run it as a standalone application without using the
> full power of Cyc. They developed tools that were able to extract
> the 5,532 axioms they needed from the half million axioms of the
> total Cyc system. Of those axioms, 4667 could be translated to
> Horn-clause form, which they used as part of a deductive database
> system. There were 875 axioms outside the Horn-clause subset;
> instead of throwing them away, they used those axioms as database
> constraints, which could be evaluated against their relational DB
> in polynomial time (a constraint is simply a query whose answer is
> required to be "yes"). See the full paper for more info.
>
> 6. Such examples illustrate my recommendation: use a large ontology
> with axioms stated in a highly expressive logic and develop
> automated tools that can extract different subsets of that ontology
> that can be used for different kinds of problems with different
> methods of reasoning. For those problems that can be solved with
> description logics or Horn-clause logics, the automated tools can
> extract the appropriate subset and translate it to the proper form.
> But the same tools may be used to extract other subsets for other
> purposes.
>
> Bottom line: I don't believe in a one-size-fits-all version of logic.
> Different problems may require different methods of reasoning with
> logics of different expressive powers. But many different versions
> of logic can be related to one another as subsets of a more expressive
> logic, from which they can be extracted with the aid of appropriate
> tools.
>
> I also take exception to the following point:
>
> EF>And for this, I don't mean two DIFFERENT tasks, but essentially
> >the same task viewed from the positive and the negative point of view.
>
> I don't regard the positive and negative views as "essentially the
> same task." One of them may be well defined and bounded while the
> other is open-ended and impossible to characterize. The set of all
> cows is finite, but the set of all non-cows is completely undefined.
>
> Following is the reference for point #5 above:
>
> Peterson, Brian J., William A. Andersen, & Joshua Engel (1998)
> "Knowledge bus: generating application-focused databases from large
> ontologies", in Proc. 5th KRDB Workshop, Seattle, WA. Available from
> http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-10/paper2.ps
>
>
> 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/
===============================================================