ANYTIME CLAUSAL REASONING

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 (M odus Ponens). Such a family of reasoners constitutes an anytime reason er, since each propositional theory has a complete reasoner in the fam ily. We provide an alternative characterization, based on a fixed-poin t construction, of the reasoners in our anytime families. This fixed-p oint characterization is then used to define a transformation of propo sitional theories into logically equivalent theories for which the bas e reasoner is complete; such theories are called ''vivid''. Developing appropriate notions of vividness and techniques for compiling theorie s into vivid theories has already generated considerable interest in t he KR community. We illustrate our approach by developing an anytime f amily based on Boolean constraint propagation.