(Hyper)sequent Calculi for the ALC(S4) Description Logics

Authors

  • Juan Pablo Muñoz Benemérita Universidad Autónoma de Puebla
  • Everardo Bárcenas CONCyT - Universidad Veracruzana
  • Iván Martínez Benemérita Universidad Autónoma de Puebla
  • José Ramón Enrique Arrazola Benemérita Universidad Autónoma de Puebla

DOI:

https://doi.org/10.13053/cys-20-1-2186

Keywords:

Description logics, (Hyper)sequents, proof theory, automated reasoning.

Abstract

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.

Author Biographies

Juan Pablo Muñoz, Benemérita Universidad Autónoma de Puebla

is a doctoral student in Mathematical Sciences at the Benemérita Universidad Autónoma de Puebla and also he is a grant holder by the Consejo Nacional de Ciencia y Tecnología (CONACYT). His main research areas are non-classical logic, proof theories, automated theorem proving, and knowledge representation.

Everardo Bárcenas, CONCyT - Universidad Veracruzana

is a researcher at the Consejo Nacional de Ciencia y Tecnología (CONACYT). He graduated from Université de Grenoble. His research interests include automated reasoning, modal logics, knowledge representation, and formal methods.

Iván Martínez, Benemérita Universidad Autónoma de Puebla

is a full-time professor of the Facultad de Ciencias Físico-Matemáticas at BUAP. He obtained his Ph.D. in Mathematical Sciences from the National Autonomus University of Mexico (UNAM) in 2010. His research interests are mathematical logic, set theory, logic programming, knowledge representation, and general topology.

José Ramón Enrique Arrazola, Benemérita Universidad Autónoma de Puebla

received his Bachelor’s, Master’s and Doctorate degrees from Benemérita Universidad Autónoma de Puebla in Puebla, Mexico, in 1986, 1989 and 1996, respectively. He has directed over 13 undergraduate theses, nine Master’s theses, and one doctoral thesis. Also, he has around 70 articles published. His research interests are mathematical logic, logic programming and knowledge representation, argumentation theory and topology. He is the current Director of the Physical-Mathematical Sciences Faculty at the Benemérita Universidad Autónoma de Puebla.

Downloads

Published

2016-03-31

Issue

Vol. 20 No. 1 (2016): Thematic Issue: Topic Trends in Computing Research (Guest Editor: Claudia P. Ayala)

Section

Articles

License 

Hereby I transfer exclusively to the Journal "Computación y 
Sistemas", published by the Computing Research Center (CIC-IPN),
the Copyright of the aforementioned paper. I also accept that these 
rights will not be transferred to any other publication, in any other 
format, language or other existing means of developing.
I certify that the paper has not been previously disclosed or simultaneo
usly submitted to any other publication, and that it does not contain 
material whose publication would violate the Copyright or other 
proprietary rights of any person, company or institution. I certify that 
I have the permission from the institution or company where I work or 
study to publish this work.
The representative author accepts the responsibility for the publication
of this paper on behalf of each and every one of the authors. 
This transfer is subject to the following conditions:
  • The authors retain all ownership rights (such as patent rights) of this work, except for the publishing rights transferred to the CIC, through this document.
  • Authors retain the right to publish the work in whole or in part in any book they are the authors or publishers. They can also make use of this work in conferences, courses, personal web pages, and so on.
  • Authors may include working as part of his thesis, for non-profit distribution only.