(Hyper)sequent Calculi for the ALC(S4) Description Logics
Fuente:
Redalyc
Salvato in:
| Autore principale: | |
|---|---|
| Natura: | Artículo científico |
| Lingua: | en |
| Pubblicazione: |
Instituto Politécnico Nacional
2016
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1876463058568609792 |
|---|---|
| author | Juan Pablo Muñoz |
| author_facet | Juan Pablo Muñoz |
| contents | (Hyper)sequent Calculi for the ALC(S4) Description Logics Juan Pablo Muñoz Everardo Bárcenas Iván Martínez José Ramón Enrique Arrazola Computación proof theory (Hyper)sequents Description logics automated reasoning Description logics (DL) form a well-known family of knowledge representation languages. One of its main applications is on the Semantic Web as a reasoning framework in the form of the Ontology Web Language (OWL). In this paper, we propose a cut-free tree hypersequent calculus for terminological reasoning in the Description Logic ALC. We show the calculus is sound and complete. Also, an implementation is provided together with a complexity analysis. In addition, we also describe a cut-free sequent calculus for the description logic ALC with reflexive and transitive roles. Soundness and completeness are proven, and a complexity analysis and an implementation are also provided. 2016 artículo científico 1405-5546 https://www.redalyc.org/articulo.oa?id=61544821007 en http://www.redalyc.org/revista.oa?id=615 Computación y Sistemas application/pdf Instituto Politécnico Nacional Computación y Sistemas (México) Num.1 Vol.20 |
| format | Artículo científico |
| id | redalyc_61544821007 |
| institution | Redalyc |
| language | en |
| publishDate | 2016 |
| publisher | Instituto Politécnico Nacional |
| spellingShingle | (Hyper)sequent Calculi for the ALC(S4) Description Logics Juan Pablo Muñoz Computación proof theory (Hyper)sequents Description logics automated reasoning (Hyper)sequent Calculi for the ALC(S4) Description Logics Juan Pablo Muñoz Everardo Bárcenas Iván Martínez José Ramón Enrique Arrazola Computación proof theory (Hyper)sequents Description logics automated reasoning Description logics (DL) form a well-known family of knowledge representation languages. One of its main applications is on the Semantic Web as a reasoning framework in the form of the Ontology Web Language (OWL). In this paper, we propose a cut-free tree hypersequent calculus for terminological reasoning in the Description Logic ALC. We show the calculus is sound and complete. Also, an implementation is provided together with a complexity analysis. In addition, we also describe a cut-free sequent calculus for the description logic ALC with reflexive and transitive roles. Soundness and completeness are proven, and a complexity analysis and an implementation are also provided. 2016 artículo científico 1405-5546 https://www.redalyc.org/articulo.oa?id=61544821007 en http://www.redalyc.org/revista.oa?id=615 Computación y Sistemas application/pdf Instituto Politécnico Nacional Computación y Sistemas (México) Num.1 Vol.20 |
| title | (Hyper)sequent Calculi for the ALC(S4) Description Logics |
| topic | Computación proof theory (Hyper)sequents Description logics automated reasoning |
| url | https://www.redalyc.org/articulo.oa?id=61544821007 |