We have also been working for some time to semantically characterize a large class of inferences that can be done quickly. Our goal is to use this information to develop ``anytime'' approximate reasoning systems that are guaranteed to perform a broad class of inferences quickly, and which can then do more complicated reasoning as time allows. Our framework supports a kind of iterative refinement of the models: a system can start with a partial model and gradually make it more concrete as the reasoning process continues, and it will never preclude possibilities that actually remain open by doing so. The reasoning systems characterized by our semantics are tractable, and can be incrementally extended to more complete reasoners without sacrificing polytime behaviour.
Current work involves extending the framework to provide a tractable limited inference mechanism for full first-order logic, combining the ideas from the propositional case with our ideas on context-limited reasoning.