Sound Global State Caching for ALC with Inverse Roles

Abstract. We give an optimal (exptime), sound and complete tableaubased algorithm for deciding satisfiability with respect to a TBox in the logic ALCI using global state caching. Global state caching guarantees optimality and termination without dynamic blocking, but in the presence of inverse roles, the proofs of soundness and completeness become significantly harder. We have implemented the algorithm in OCaml, and our initial comparison with FaCT++ indicates that it is a promising method for checking satisfiability with respect to a TBox.

• Type: Conference
• Year: 2009
• Where: TABLEAUX
• Authors: Rajeev Goré, Florian Widmann
• Keywords: Artificial Intelligence, Complete Tableaubased Algorithm, Global State Caching, State Caching Guarantees, TABLEAUX 2009