Preliminary Empirical Results on Anytime Propositional Reasoning (Abstract)

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.