×

Anytime clausal reasoning. (English) Zbl 0905.68115

Summary: Given any incomplete clausal propositional reasoner satisfying certain properties, we extend it to a family of increasingly-complete, sound, and tractable reasoners. Our technique for generating these reasoners is based on restricting the length of the clauses used in chaining (Modus Ponens). Such a family of reasoners constitutes an anytime reasoner, since each propositional theory has a complete reasoner in the family. We provide an alternative characterization, based on a fixed point construction, of the reasoners in our anytime families. This fixed-point characterization is then used to define a transformation of propositional theories into logically equivalent theories for which the base reasoner is complete; such theories are called “vivid”. Developing appropriate notions of vividness and techniques for compiling theories into vivid theories has already generated considerable interest in the KR community. We illustrate our approach by developing an anytime family based on Boolean constraint propagation.

MSC:

68T05 Learning and adaptive systems in artificial intelligence
Full Text: DOI