John F Sowa wrote:
> Michael,
>
> The word 'decidable' has been bandied about in contexts that are
> far removed from its original definition. Many of those extensions
> are convenient and useful. But the word should always be used with
> all the proper qualifications.
> (01)
Fully agree. (02)
> <snip>
> Fundamental definition: A procedure P, as stated in some formal
> language L, is said to be *undecidable* for some data D iff it is
> impossible to prove whether P will come to a halt in processing D
> or whether it will continue forever (AKA "get hung up in a loop").
>
> If it can be proved that P will come to a halt on D, then P is
> said to be *decidable* for input data D. Note that a procedure
> can be decidable for some data, but undecidable for other data.
> (03)
Right. So a desirable procedure should be decidable on all the data it
will be asked to process. No one cares whether one can write
undecidable programs in the language. The requirement is only that a
given procedure will halt, having accomplished its purpose, with all
"possible" data input. (The point here is that the possible inputs can
be constrained by prior actions of the overall process in which the
procedure is used.) (04)
> <snip>
>
> The distinction of decidable/undecidable, which is properly defined
> for procedures, can be extended to many other things, and each
> extension must be carefully evaluated:
> <snip>
>
> 3. Logic languages: Properly speaking, no version of logic can state
> a procedure. Therefore, the notion of decidability has no direct
> extension to logics. However, a combination of a logic with some
> computational procedure can be used for some kinds of tasks. But
> what is decidable is always the *combination* of a logic with a
> particular kind of procedure for a particular kind of task:
> (05)
The computational procedure -- the "reasoning algorithm" -- is a
procedure, with the above characterization. If the input to that
procedure is an arbitrary collection of statements in a well-defined
"logic language", then that defines the concept "all permitted input
data". One question is then whether the chosen reasoning algorithm will
halt for all possible collections of statements in the language. The
other important question is whether the reasoning algorithm produces
useful results for collections of statements that constitute 'theories'
that have some practical consequences. (06)
> (a) Proving theorems: A logic plus a proof procedure can be used
> to test whether a particular statement is can be derived from
> other statements (which may be called axioms).
> (07)
So, the computational procedure is "decidable" if it can determine
whether S0 is derivable from (S1, ..., Sn) for arbitrary S0 and Si
written in the input data language. It does not suffice that it halts,
if it can halt without being able to make the determination. (08)
> (b) Answering questions: A logic plus a proof procedure plus some
> given data can be used to derive answers from the data. This
> kind of problem is similar to the task of proving theorems,
> if the axioms are equated with the data. However, the data
> may be in a specialized form, such as a relational database
> or a triple store. For such data, the task of answering
> questions may be decidable when task (a) is undecidable.
> (09)
That is, if the permissible input data is restricted to something
significantly less than all possible statements in the language. In
this case, what John is talking about is a fixed input theory -- a
particular set of statements (S1, ..., Sn) -- and a set of additional
statements Sj, all of which are simple relations. (010)
> (c) Constraint testing: A logic can be used to state constraints
> on permissible data. The task is of verifying whether the
> constraints are true of some data is closer to (b) than to (a).
> (011)
Yes, if the data are expressible as simple relations. (012)
> (d) Induction or data mining: Deduction is only one way of using
> logic, and it requires a prior set of axioms before it can be
> used. The task of induction or data mining is to analyze the
> given data to form generalizations, which may later be used
> for other tasks, which may include (a), (b), or (c).
>
> (e) Abduction: Another important way of using logic is to form
> hypotheses about a given set of data. These hypotheses are
> often much more complex (or "insightful") than induction.
> The methods of abduction are related to what would be called
> "creative" in humans, and no formal specification is possible.
> However, the hypotheses generated by abduction can and should
> be tested against the data by other methods, such as (a) or (b).
>
> Given this range of uses for logic, the term 'decidable' can only be
> applied to a logic when a specific kind of task for a specific kind
> of data is being considered.
> (013)
Yes. Excluding the gratis excursiion into induction and abduction,
which are expected to be iffy and are often accomplished by mathematical
methods other than logic, e.g. statistics and mathematical programming,
what we see above is that there are two target uses of logic in
industry: (a) and (b)/(c). (014)
Industry has been using logics for the (b)/(c) cases for at least 25
years, and we now know a lot about the relationships between reasoning
algorithms, base theories, and decidability and computational bounding.
Almost all of the logics used for (b)/(c) are constrained FOLs or "not
FOL", and almost all of the algorithms used with these logics are
computationally bounded. That is why they are commonly used in industry. (015)
> <snip>
>
> Yes. The above discussion shows that the term 'decidable' can only be
> applied to a logic language in a very indirect way. It is so indirect
> that it's more misleading than useful to say that a certain logic
> language is decidable or undecidable. That decision *always* depends
> on what you plan to do with the logic.
> (016)
That decision depends on what sets of input statements -- the
"permissible input data" -- are allowed, and whether the chosen
reasoning algorithm halts with useful results for all possible input sets. (017)
We may say that a language is "decidable" if there is any known
reasoning algorithm that will always terminate given an arbitrary S0
hypothesis and an arbitrary theory S1,...,Sn, where all the Si are
statements in the language. There are many logic languages for which
there are such known reasoning algorithms. (018)
The issue that started this thread is whether emerging technologies for
(a) and (b) -- languages and reasoning engines that accept arbitrary
sets of sentences in those languages -- will be acceptable in industry
if they are not decidable. The whole idea of the DL world is that each
DL language comes with a known reasoning algorithm that will always halt
given a valid input data set = a set of sentences in the language. So
DLs, and OWL/DL in particular, are "decidable" in the sense above, and
in fact, they are computationally bounded. Following the 25+-year
history of industrial adoption of other logics, that is expected to be a
requirement for most industry applications. (019)
Everyone agrees that FOL is more expressive and potentially more useful,
but all of the reasoning procedures that are widely used in academia
either restrict the allowable FOL inputs in some way that greatly
reduces its expressiveness or are programmed to throw up their hands at
some point -- they "halt" by saying "not determinable" (in some
language). The problem of not knowing the relationship between input
data -- the sets of valid sentences -- and the "not determinable" result
is what causes industry to shy away from FOL reasoners. (020)
-Ed (021)
>
>
> I discuss these and related issues in the following paper:
>
> http://www.jfsowa.com/pubs/fflogic.pdf
> Fads and fallacies about logic
>
> John
>
> _________________________________________________________________
> Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
> Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
> Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
> Shared Files: http://ontolog.cim3.net/file/
> Community Wiki: http://ontolog.cim3.net/wiki/
> To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
>
> (022)
--
Edward J. Barkmeyer Email: edbark@xxxxxxxx
National Institute of Standards & Technology
Systems Integration Division, Engineering Laboratory
100 Bureau Drive, Stop 8263 Tel: +1 301-975-3528
Gaithersburg, MD 20899-8263 Cel: +1 240-672-5800 (023)
"The opinions expressed above do not reflect consensus of NIST,
and have not been reviewed by any Government authority." (024)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join: http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J (025)
|