Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Sound Global State Caching for ALC with Inverse Roles
| |
|
Sound Global State Caching for ALC with Inverse Roles
Rajeev Goré20  and Florian Widmann21
| (20) |
Logic and Computation Group, The Australian National University, Canberra, ACT 0200, Australia |
| (21) |
Logic and Computation Group and NICTA, The Australian National University, Canberra, ACT 0200, Australia |
Abstract
We give an optimal (exptime), sound and complete tableau-based 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.
Fulltext Preview (Small, Large)
 References secured to subscribers.
|
|
|
|
|
|