Reformulating Non-Monotonic Theories for Inference and Updating (April 28 1992)
by Benjamin N. Grosof
Abstract:
We aim to help build programs that do large-scale, expressive
non-monotonic reasoning (NMR): especially, "learning agents" that
store, and revise, a body of conclusions while continually acquiring
new, possibly defeasible, premise beliefs. Currently available
procedures for forward inference and belief revision are exhaustive,
and thus impractical: they compute the entire non-monotonic theory,
then re-compute from scratch upon updating with new axioms. These
methods are thus badly intractable. In most theories of interest,
even backward reasoning is combinatoric (at least NP-hard). Here, we
give theoretical results for prioritized circumscription that show how
to reformulate default theories so as to make forward inference be
selective, as well as concurrent; and to restrict belief revision
to a part of the theory. We elaborate a detailed divide-and-conquer
strategy. We develop concepts of structure in NM theories, by
showing how to reformulate them in a particular fashion: to be
conjunctively decomposed into a collection of smaller "part"
theories. We identify two well-behaved special cases that are easily
recognized in terms of syntactic properties: disjoint appearances of
predicates, and disjoint appearances of individuals (terms). As part
of this, we also definitionally reformulate the global axioms, one
by one, in addition to applying decomposition. We identify a broad
class of prioritized default theories, generalizing default
inheritance, for which our results especially bear fruit. For this
asocially monadic class, decomposition permits reasoning to be
localized to individuals (ground terms), and reduced to
propositional. Our reformulation methods are implementable in
polynomial time, and apply to several other NM formalisms beyond
circumscription.
Last update: 1-8-98
Up to Benjamin Grosof's Papers page
Up to Benjamin Grosof home page
[ IBM Research home page ][
IBM home page |
Order |
Search |
Contact IBM |
Help |
(C) |
(TM)
]