Abstract
This thesis examines a novel induction-based framework
for logic programming. Limiting programs are logic programs distinguished
by two features, in general they contain an infinite data stream
over which induction will be performed, and in general it is not possible
for a system to know when a solution for any program is correct. These
facts are characteristic of some problems involving induction in artificial
intelligence, and several problems in knowledge representation and
logic programming have exactly these properties. This thesis presents
a specification language for problems with an inductive nature, limiting
programs, and a resolution based system, limiting resolution, for solving
these problems. This framework has properties which guarantee
that the system will converge upon a particular answer in the limit.
Solutions to problems which have such an inductive property by
nature can be implemented using the language, and solved with the
solver. For instance, many classification problems are inductive by
nature. Some generalized planning problems also have the inductive
property. For a class of generalized planning problems, we show that
identifying a collection of domains where a plan reaches a goal is equivalent
to producing a plan. This thesis gives examples of both.
Limiting resolution works by a generate-and-test strategy, creating
a potential solution and iteratively looking for a contradiction with the
growing stream of data provided. Limiting resolution can be implemented
by modifying conventional PROLOG technology. The generateand-
test strategy has some inherent inefficiencies. Two improvements
have arisen from this work; the first is a tabling strategy which records
previously failed attempts to produce a solution and thereby avoids redundant
test steps. The second is based on the heuristic observation
that for some problems the size of the test step is proportional to the
closeness of the generated potential-solution to the real solution, in a
suitable metric. The observation can be used to improve the performance
of limiting resolution.
Thus this thesis describes, from theoretical foundations to implementation,
a coherent methodology for incorporating induction into
existing general A.I. programming techniques, along with examples of
how to perform such tasks.