TITLE: How to Make Reasoning Faster: Subsumption Detection in Tableau-Based Automated Theorem Proving
TIME: Monday, June 4, 2001 1:00 p.m. - 3:00 p.m; ASB 9896
ABSTRACT:
As is well-known, theorem proving in any logic that is at least as expressive as propositional logic is NP-hard at best. However, implementations of theorem proving algorithms have become fast enough to handle fairly large-sized knowledge bases occurring in real-life applications. This progress is due to a number of techniques that have been devised to improve efficiency, such as backjumping, caching of intermediate results, heuristics, and normalization.
These efficiency techniques can be further improved by implementing a subsumption detection algorithm. A formula A subsumes a formula B iff, whenever B is satisfied, A is also satisfied. While the subsumption detection problem is just as hard as deciding unsatisfiability, subclasses of subsumption can be detected in polynomial time. Whenever a subsumption relation is discovered, one of the formulas involved is redundant and can be eliminated, which leads to smaller knowledge bases, more efficient caching, and earlier detection of unsatisfiability.
The benefits of subsumption detection are currently being quantitatively evaluated with a newly developed theorem prover, which will also be introduced in this talk. Some of the experimental results demonstrating the strength of this approach will be presented.
For further information please contact Jens Happe at jhappe@cs.sfu.ca