EXPTIME tableaux for ALC using sound global caching
Gore, Rajeev; Nguyen, Linh Anh
Description
We show that global caching can be used with propagation of both satisfiability and unsatisfiability in a sound manner to give an EXPTIME algorithm for checking satisfiability w.r.t. a TBox in the basic description logic ALC. Our algorithm is based on a simple traditional tableau calculus which builds an and-or graph where no two nodes of the graph contain the same formula set. When a duplicate node is about to be created, we use the pre-existing node as a proxy, even if the proxy is from a...[Show more]
dc.contributor.author | Gore, Rajeev | |
---|---|---|
dc.contributor.author | Nguyen, Linh Anh | |
dc.coverage.spatial | Brixen-Bressanone | |
dc.date.accessioned | 2015-12-10T22:20:47Z | |
dc.date.created | June 8-10 2007 | |
dc.identifier.isbn | 9788860460085 | |
dc.identifier.uri | http://hdl.handle.net/1885/52074 | |
dc.description.abstract | We show that global caching can be used with propagation of both satisfiability and unsatisfiability in a sound manner to give an EXPTIME algorithm for checking satisfiability w.r.t. a TBox in the basic description logic ALC. Our algorithm is based on a simple traditional tableau calculus which builds an and-or graph where no two nodes of the graph contain the same formula set. When a duplicate node is about to be created, we use the pre-existing node as a proxy, even if the proxy is from a different branch of the tableau, thereby building global caching into the algorithm from the start. Doing so is important since it allows us to reason explicitly about the correctness of global caching. We then show that propagating both satisfiability and unsatisfiability via the and-or structure of the graph remains sound. In the longer paper, by combining global caching, propagation and cutoffs, our framework reduces the search space more significantly than the framework of [1]. Also, the freedom to use arbitrary search heuristics significantly increases its application potential. A longer version with all optimisations is currently under review for a journal. An extension for SHI will appear in TABLEAUX 2007. | |
dc.publisher | Bozen-Bolzano University Press | |
dc.relation.ispartofseries | International Workshop on Description Logics (DL 2007) | |
dc.source | 2007 International Workshop on Description Logics Proceedings | |
dc.subject | Keywords: Decision procedure; Description logic; Optimal complexity; Optimisations; Satisfiability; Search heuristics; Search spaces; Formal languages; Formal logic; Heuristic algorithms; Optimization; Data description Decision procedures; Optimal complexity; Sound caching | |
dc.title | EXPTIME tableaux for ALC using sound global caching | |
dc.type | Conference paper | |
local.description.notes | Imported from ARIES | |
local.description.refereed | Yes | |
dc.date.issued | 2007 | |
local.identifier.absfor | 080203 - Computational Logic and Formal Languages | |
local.identifier.absfor | 010104 - Combinatorics and Discrete Mathematics (excl. Physical Combinatorics) | |
local.identifier.absfor | 080299 - Computation Theory and Mathematics not elsewhere classified | |
local.identifier.ariespublication | u4251866xPUB238 | |
local.type.status | Published Version | |
local.contributor.affiliation | Gore, Rajeev, College of Engineering and Computer Science, ANU | |
local.contributor.affiliation | Nguyen, Linh Anh, University of Warsaw | |
local.description.embargo | 2037-12-31 | |
local.bibliographicCitation.startpage | 8 | |
local.identifier.absseo | 890399 - Information Services not elsewhere classified | |
dc.date.updated | 2016-02-24T10:47:32Z | |
local.identifier.scopusID | 2-s2.0-84872941229 | |
Collections | ANU Research Publications |
Download
File | Description | Size | Format | Image |
---|---|---|---|---|
01_Gore_EXPTIME_tableaux_for_ALC_using_2007.pdf | 164.93 kB | Adobe PDF | Request a copy |
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.
Updated: 17 November 2022/ Responsible Officer: University Librarian/ Page Contact: Library Systems & Web Coordinator