Published:
May 2000
Proceedings:
Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2000)
Volume
Issue:
Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2000)
Track:
All Papers
Downloads:
Abstract:
Automated theorem proving with connection tableau calculi imposes search problems in tremendous search spaces. In this paper, we present a new approach to search space reduction in connection tableau calculi. In our approach structurally similar parts of the search space are compressed by means of disjunctive constraints. We describe the necessary changes of the calculus, and we develop elaborate techniques for an efficient constraint processing. Moreover, we present an experimental evaluation of our approach.
FLAIRS
Proceedings of the Thirteenth International Florida Artificial Intelligence Research Society Conference (FLAIRS 2000)
ISBN 978-1-57735-113-9
Published by The AAAI Press, Menlo Park, California.