Best Buy Coupon
| – | Planning to put the reasoning script onto object-oriented rails. It will take some time to accomplish, but will give some benefits... E.g. to be able to easily add new results, to be able to automatically show all results that follow from the given ones, to be able to add new complexity "measures" (such as complexity of query answering, complexity of finite model reasoning, etc), and even to create other Complexity Navigators (say, for sub-boolean logics like EL, or for modal logics, etc). So far, any of these tasks requires a lot of manual work and re-programming many things. | |
| – | For all papers in the bibliography, BiBTeX entries are created, with the "doi" and "ee" fields whenever possible. Note that the "ee" fields ("electronic edition") are clickable! Some missing abstracts are also added. | |
| – | For all journal articles, BiBTeX entries are added. | |
| – | Corrections are made to the text on elimination of TBoxes and ABoxes. | |
| – | Abstracts added. You can open/close a particular abstract by clicking a link next to PDF or PS link. You can also open/close all abstracts by a single pressing a special button at the beginning of the list of papers (this may be useful for searching papers by keywords in their abstracts). | |
| – |
In the (PSpace-complete) Description Logics SIN and SIQ ,
it is assumed that transitive roles are not
used in number restrictions (although it is only said on p.24 of
[HorrocksSattlerTobies1998, Definition 19]
and not mentioned in the abstract,
so I didn't mention it in the Navigator before; now it's fixed).
• On the contrary, for the unrestricted SIN and SIQ , concept satisfiability w.r.t. general TBoxes is undecidable; see [KazSatZol2007] (note that no role hierarchy was needed to obtain undecidability). • In fact, the unrestricted SIQ is the fusion of several copies of the graded inverse modal logics: GrIK (which is PSpace-complete) and GrIK4 (which is (globally) undecidable). • At the same time, the restricted SIQ is the fusion of several copies of the inverse modal logics: GrIK (which is PSpace-complete) and IK4 (which is PSpace-complete); that is why it is PSpace-complete. • Is concept satifiability (without TBoxes) for the unrestricted SIQ undecidable too? I.e. is the the unrestricted SIQ locally undecidable? Yes! (the result will be published soon) | |
| – |
In a recent paper I read:
The description logic S extends ALC with transitive roles,
and so can be thought of as the union of Km and K4m.
Nope, this is not fair...
As everyone knows, K ⊂ K4, so their union is just K4.
• In fact, S corresponds to the fusion of several copies of the (PSpace-complete) modal logics K and K4. • Similarly, unrestricted SQ (i.e., where transitive roles are allowed in number restrictions) corresponds to the fusion of several copies of the graded modal logics: GrK (which is PSpace-complete) and GrK4 (which is NExpTime-complete); so concept satisfiability in the unrestricted SQ is decidable (in fact, NExpTime-complete). • Furthermore, restricted SQ (i.e., where transitive roles are not allowed in number restrictions) corresponds to the fusion of several copies of the PSpace-complete graded modal logic GrK and another PSpace-complete modal logic K4; therefore, concept satisfiability in this logic is PSpace-complete. • Complexity of GrK and GrK4 can be found in [Kazakov, Pratt-Hartmann, 2009]; for the results on fusions of modal / description logics, see [Frank Wolter, Fusion of Description Logics, JAIR, 2002]. | |
| – | Long conference names (and their dates and places) are now hidden, only short names are left to be shown (e.g., IJCAI'91). However, you can press a special button at the beginning of the list of papers and all long names will be shown again. This is done with a use of a semantic HTML markup. | |
| – | Added some new results: First-order two-variable logic with counting is NExpTime-complete even with binary encoding of numbers (Ian Pratt-Hartmann, 2005); PDL with intersection and converse is not only decidable, but 2ExpTime-complete (S.Goeller, M.Lohrey, C.Lutz, 2007). | |
| – | After years, many of the external links to PDF and PS documents are broken (as people move their homepages, and sites change their link structures). Henceforth, for your (and my) convenience, documents are now stored locally, with meaningful file names. | |
| – | Added a link to the 2nd edition of The Description Logic Handbook. Reformatted the bibliography, with a sort of semantic html markup. Corrected several references (years, pages, even paper titles). Updated links to people's homepages. | |
| – | A trivial, but missing, bunch of results is added: All role constructors in the logic ALC(∪,o,id) are eliminable. Therefore, for all its sublogics the complexity of all problems (concept satisfiablilty and ABox consistency, with or without TBox) is the same as for ALC. Similarly for ALC extended with inverse roles and/or nominals. | |
| – | Some improvements in design: constructors are highlighted in blue; rows with constructors are highlighted when the mouse is over; now you can click anywhere in the row (not only on the checkbox) in order to select the constructor; role-value maps and feature agreement constructors (both not realized so far) are hidden to save space (there are not much results known for them anyway). | |
| – | In SHIQ family of Description Logics, there is a notorious restriction on the syntax: transitive roles and their sub-roles cannot be used in number restrictions (otherwise, the logic becomes undecidable). Our recent results [KazSatZol2007] shows that, in many cases, one can use transitive roles in number restrictions – and still have a decidable logic! So the notion of a simple role could be substantially extended. | |
| – | ABox consistency in the logic ALCI with empty or acyclic TBoxes is PSpace-complete, a result obtained in [Ding et al., 2007] by reduction of logics with inverses to logics without inverses. | |
| – | Improved interface: whether role complement is atomic or full, and whether complex roles are allowed or forbidden in number restrictions is now displayed explicitly in the field "You have selected a DL..." (only if these options are relevant, of course). Otherwise people often forget about these options and come to wrong conclusions. | |
| – | Finite model property and tree model property depend on what kind of TBoxes are allowed. Some minor corrections to the Navigator are applied, with almost no effect on currently displayed results (just because there are very few positive results on FMP or TMP for logics, in which TBoxes are not internalized, and for which adding TBoxes breaks FMP or TMP). | |
| – | All sublogics of SHOQ have the finite model property. The result is not new (see a paper by C.Lutz, C.Areces, I.Horrocks, and U.Sattler, 2002), but was missing in the Complexity Navigator. | |
| – | The result is added: the concept satisfiability problem in the logic SI with acyclic TBoxes is PSpace-complete. | |
| – | Now the picture concerning μ-logics is (relatively) complete: all logics between μALC and μALCQIO are ExpTime-complete (even with numbers coded in binary), except for logics above μALCFIO (which are undecidable). The remaining open problem about μALCQO has been solved in [P.Bonatti, C.Lutz, A.Murano, and M.Y.Vardi, 2006]. | |
| – | All logics between ALCFIO and ALCQIO(∩,∪,¬) with or without TBoxes are NExpTime-complete (with unary number encoding only) for both concept satisfiability and ABox consistency problems. If we consider only "safe" boolean combinations of roles, then such an extension of any logic between ALC and ALCQI is PSpace-complete without TBoxes, and ExpTime-complete with general TBoxes (the case of acyclic TBoxes remains open). These results were picked up again by Birte Glimm from the inexhaustible source – Stephan Tobies' PhD Thesis. | |
| – | Concept satisfiability for the logic SIN is shown to be PSpace-complete by I.Horrocks, U.Sattler, and S.Tobies in 1998. Moreover, the Finite Model Property for this logic (and all its sublogics) follows from their results as well. (Thanks to Birte Glimm for pointing this out to me.) | |
| – | The Complexity Navigator is even more handy now: all references to the literature are hyperlinks. One click – and you see the reference you need! | |
| – | The results about logics RIQ, sRIQ, and sROIQ are added. Dependencies concerning R are implemented: if R is ticked, then S and H are ticked (and hence, TBox is internalized). Another checkbox s appeared, for some additional features in the logics sRIQ and sROIQ (a lower-case letter s is used for them, in order to avoid collision with the upper-case S, which traditionally stands for transitivity). | |
| – | Knowledge base consistency for any logic between ALC and SHIQ w.r.t. general TBoxes has the same complexity as concept satisfiability, as S.Tobies has shown in his PhD Thesis. (Thanks to Birte Glimm for pointing this out to me.) | |
| – |
The checkbox for R (complex role inclusions) is added,
so far inactive. Its dependency with other features,
its impact on logic name, and complexity results will be added later.
The button | |
| – | In the logic ALCQI, finite model reasoning (both concept satisfiability and ABox consistency) w.r.t. general TBoxes is ExpTime-complete. This improves the ExpExpTime upper bound established in 1996. | |
| – | The logic μALCQIO is undecidable. Among its sublogics, only the decidability of μALCQO remains unknown. | |
| – | Buttons "OWL-Lite" and "OWL-DL" are added. | |
| – | This list of updates was created. Thus the list below this point only partially covers the history of updates. | |
| – | A short article by Bijan Parsia, where, in particular, the Navigator is mentioned. | |
| – |
The μ-operator is added, with its dependencies:
TBox is internalized in presence of | |
| – | Many results on DLs with number restrictions (N) and role operations are added. There is a subtlety in the naming of these logics: one can allow/disallow role operators independently in number (≥n R) and in value (∃R, ∀R) restrictions. To resolve the issue, the selector was introduced to the Navigator. Dependency: This selector is active iff one of F, N, or Q and any role operation (other than role inverse) are selected. | |
| – | The link to the Navigator appeared on the Description Logic web site. | |
| – | Numerous results on DLs with role negation are added. For this, the selector " role negation" was introduced to the Navigator. Dependencies: 1) If ¬ and one of {∩,∪} is selected, then the other one is also selected (by the script). 2) The full/atomic selector is active iff the negation and any other role operation (except role inverse) is selected. Exception: this selector is not active, if only {¬,∩,∪} and no other operations are selected. 3) The atomic negation is turned into full (by the script) iff {¬,∩,∪} and no other operations are selected. | |
| – | WOW! A link to the DL Complexity Navigator pas appeared in the English (Description Logic), German (Beschreibungslogik), Spanish (Lógicas de Descripción) and other articles in Wikipedia. | |
| – | The announcement about the Navigator was sent in the DL mailing list. | |
| – | TBox is internalizable in extensions of the logics: ALCIO, SH, ALC(∪,*). | |
| – | The dependency is realized: If a TBox is internalizable in a logic, then the script must "collect" the results from the cases of empty, acyclic, and general TBoxes. | |
| – | The dependency is realized: If a logic contains nominals, then the complexity result for ABox consistency must be automatically read off from that for concept satisfiability. | |
| – | The first version was designed, but contained almost no complexity results. |