Return to search

Integrating Reasoning Services for Description Logics with Cardinality Constraints with Numerical Optimization Techniques

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

Identiferoai:union.ndltd.org:DRESDEN/oai:qucosa:de:qucosa:85337
Date08 May 2023
CreatorsDe Bortoli, Filippo
ContributorsBaader, Franz, Peñaloza Nyssen, Rafael, Technische Universität Dresden
Source SetsHochschulschriftenserver (HSSS) der SLUB Dresden
LanguageEnglish
Detected LanguageEnglish
Typeinfo:eu-repo/semantics/publishedVersion, doc-type:masterThesis, info:eu-repo/semantics/masterThesis, doc-type:Text
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.002 seconds