*Mukesh Dalal and Li Yang*

An anytime family of propositional reasoners is a sequence
I-_{o}, I-_{1},... of inference relations such that each I-_{k} is sound,
tractable, and makes more inferences than I-_{k-1}, and each
theory has a complete reasoner in the family. Anytime families
are useful for resource-bounded reasoning in knowledge
representation systems. We describe implementations of an
anytime family {I-_{k}} of clausal propositional reasoners using
three different strategies. We present empirical results
comparing the three strategies, the completeness of reasoning,
the time for making inferences, and the space used for
reasoning. Our results show that the reasoners with higher
values of *k* infer significantly more formulas than reasoners
with lower values of *k,* and the time for inferencing decreases
significantly as *k* is increased from 0 to 2.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.