Global caching, inverse roles and fixpoint logics
Date
2009
Authors
Gore, Rajeev
Journal Title
Journal ISSN
Volume Title
Publisher
CEUR-WS.ORG
Abstract
I will begin by explaining an optimal tableau-based algorithm for checking ALC-satisfiability which uses "global caching" and which appears to work well in practice. The algorithm settles a conjecture that "global caching can lead to optimality". I will then explain how "global caching" can be extended to "global state caching" for inverse roles, thereby extending the result to ALCI-satisfiability, and converse roles in general. Finally, I will explain how "global caching" can be used to give optimal "on the fly" tableau decision procedures for some fix- point logics. Finally, some open questions. The talk is intended to be expository so it will be at a fairly high level.
Description
Keywords
Keywords: Decision procedure; Fixpoints; Global state; On the flies; Optimality; Algorithms; Formal languages; Formal logic; Optimization; Data description
Citation
Collections
Source
Proceedings of the 22nd International workshop on Description logics (DL 2009)
Type
Conference paper
Book Title
Entity type
Access Statement
License Rights
DOI
Restricted until
2037-12-31
Downloads
File
Description