Recent research in the field of Description Logic (DL) investigated the complexity of the satisfiability problem for description logics that are obtained by enriching the well-known DL ALCQ with more complex set and cardinality constraints over role successors. The algorithms that have been proposed so far, despite providing worst-case optimal decision procedures for the concept satisfiability problem (both without and with a terminology) lack the efficiency needed to obtain usable implementations. In particular, the algorithm for the case without terminology is non-deterministic and the one for the case with a terminology is also best-case exponential. The goal of this thesis is to use well-established techniques from the field of numerical optimization, such as column generation, in order to obtain more practical algorithms. As a starting point, efficient approaches for dealing with counting quantifiers over unary predicates based on SAT-based column generation should be considered.:1. Introduction
2. Preliminaries
2.1. First-order logic
2.2. Linear Programming
2.3. The description logic ALCQ
2.4. Extending ALCQ with expressive role successor constraints
2.4.1. The logic QFBAPA
2.4.2 The description logic ALCSCC
3. The description logic ALCCQU
3.1. A normal form for ALCCQU
3.2. ALCQt as an equivalent formulation of ALCCQU
3.2.1. ALCQt is a sublogic of ALCCQU
3.2.2. ALCCQU is a sublogic of ALCQt
3.3. Model-theoretic characterization of ALCQt
3.3.1. ALCQt-bisimulation and invariance for ALCQt
3.3.2. Characterization of ALCQt concept descriptions
3.4. Expressive power
3.4.1. Relative expressivity of ALCQ and ALCCQU
3.4.2. Relative expressivity of ALCCQU and ALCSCC
3.5. ALCCQU as the first-order fragment of ALCSCC
4. Concept satisfiability in ALCCQU
4.1. The first-order fragment CQU
4.2. Column generation with SAT oracle
4.2.1. Column generation and CQU
4.2.2. From linear inequalities to propositional formulae
4.2.3. Column generation and ALCCQU
4.3. Branch-and-Price for ALCCQU concept satisfiability
4.4. Correctness of ALCCQU-BB
4.4.1. Complexity of ALCCQU-BB
5. Conclusion
- Bibliography
| Identifer | oai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:85337 |
| Date | 08 May 2023 |
| Creators | De Bortoli, Filippo |
| Contributors | Baader, Franz, Peñaloza Nyssen, Rafael, Technische Universität Dresden |
| Source Sets | Hochschulschriftenserver (HSSS) der SLUB Dresden |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, doc-type:masterThesis, info:eu-repo/semantics/masterThesis, doc-type:Text |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.002 seconds