Article

Cut-free exptime tableaux for checking satisfiability of a knowledge base in the description logic ALCI

Author:

ISMIS'11: Proceedings of the 19th international conference on Foundations of intelligent systems

Pages 465 - 475

Published: 28 June 2011 Publication History

Abstract

We give the first direct cut-free ExpTime (optimal) tableau decision procedure, which is not based on transformation or on the precompletion technique, for checking satisfiability of a knowledge base in the description logic ALCI.

References

[1]

Ding, Y., Haarslev, V.,Wu, J.: A new mapping from ALCI to ALC. In: Proceedings of Description Logics (2007).

Google Scholar

[2]

De Giacomo, G., Lenzerini, M.: TBox and ABox reasoning in expressive description logics. In: Aiello, L.C., Doyle, J., Shapiro, S.C. (eds.) Proceedings of KR 1996, pp. 316-327. Morgan Kaufmann, San Francisco (1996).

Google Scholar

[3]

Goré, R.P., Nguyen, L.A.: EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies. In: Olivetti, N. (ed.) TABLEAUX 2007. LNCS (LNAI), vol. 4548, pp. 133-148. Springer, Heidelberg (2007).

Digital Library

Google Scholar

[4]

Goré, R., Widmann, F.: Sound global state caching for ALC with inverse roles. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 205-219. Springer, Heidelberg (2009).

Digital Library

Google Scholar

[5]

Goré, R., Widmann, F.: Optimal and cut-free tableaux for propositional dynamic logic with converse. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 225-239. Springer, Heidelberg (2010).

Digital Library

Google Scholar

[6]

Horrocks, I., Sattler, U.: Description logics - basics, applications, and more. In: Tutorial Given at ECAI-2002, http://www.cs.man.ac.uk/~horrocks/Slides/ecai-handout.pdf

Google Scholar

[7]

Nguyen, L.A.: An efficient tableau prover using global caching for the description logic ALC. Fundamenta Informaticae 93(1-3), 273-288 (2009).

Digital Library

Google Scholar

[8]

Nguyen, L.A.: The long version of the current paper (2011), http://www.mimuw.edu.pl/~nguyen/alci-long.pdf

Google Scholar

[9]

Nguyen, L.A., Szałas, A.: expTime tableaux for checking satisfiability of a knowledge base in the description logic ALC. In: Nguyen, N.T., Kowalczyk, R., Chen, S.-M. (eds.) ICCCI 2009. LNCS(LNAI), vol. 5796, pp. 437-448. Springer, Heidelberg (2009).

Digital Library

Google Scholar

[10]

Nguyen, L.A., Szałas, A.: An optimal tableau decision procedure for Converse-PDL. In: Nguyen, N.-T., Bui, T.-D., Szczerbicki, E., Nguyen, N.-B. (eds.) Proceedings of KSE 2009, pp. 207-214. IEEE Computer Society, Los Alamitos (2009).

Digital Library

Google Scholar

[11]

Nguyen, L.A., Szałas, A.: A tableau calculus for regular grammar logics with converse. In: Schmidt, R.A. (ed.) CADE-22. LNCS(LNAI), vol. 5663, pp. 421-436. Springer, Heidelberg (2009).

Digital Library

Google Scholar

[12]

Nguyen, L.A., Szałas, A.: Checking consistency of an A Box w.r.t. global assumptions in PDL. Fundamenta Informaticae 102(1), 97-113 (2010).

Digital Library

Google Scholar

[13]

Nguyen, L.A., Szałas, A.: Tableaux with global caching for checking satisfiability of a knowledge base in the description logic SH. T. Computational Collective Intelligence 1, 21-38 (2010).

Digital Library

Google Scholar

Cited By

View all

Ha QHoang TNguyen LNguyen HSzałas ATran TTrong GHluchy LQuyet TCastelli EDuc KChi MTran V(2012)A bisimulation-based method of concept learning for knowledge bases in description logicsProceedings of the 3rd Symposium on Information and Communication Technology10.1145/2350716.2350753(241-249)Online publication date: 23-Aug-2012
https://dl.acm.org/doi/10.1145/2350716.2350753
Nguyen L(2011)A cut-free exptime tableau decision procedure for the description logic SHIProceedings of the Third international conference on Computational collective intelligence: technologies and applications - Volume Part I10.5555/2041845.2041908(572-581)Online publication date: 21-Sep-2011
https://dl.acm.org/doi/10.5555/2041845.2041908

Index Terms

Cut-free exptime tableaux for checking satisfiability of a knowledge base in the description logic ALCI
1. Theory of computation
  1. Logic

Index terms have been assigned to the content through auto-classification.

Recommendations

ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic $\mathcal{ALC}$
ICCCI '09: Proceedings of the 1st International Conference on Computational Collective Intelligence. Semantic Web, Social Networks and Multiagent Systems

We give the first <Emphasis Type="SmallCaps">ExpTime</Emphasis> (optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic $\mathcal{ALC}$, not based on transformation that encodes ABoxes by nominals or ...
A cut-free calculus for second-order Gödel logic

We prove that the extension of the known hypersequent calculus for standard first-order Gödel logic with usual rules for second-order quantifiers is sound and (cut-free) complete for Henkin-style semantics for second-order Gödel logic. The proof is ...
Cut-free Sequent Calculus and Natural Deduction for the Tetravalent Modal Logic
Abstract
The tetravalent modal logic ( $TML$ ) is one of the two logics defined by Font and Rius (J Symb Log 65(2):481–518, 2000) (the other is the normal tetravalent modal logic ${TML}^{N}$ ) in connection with Monteiro’s tetravalent modal algebras. These logics are ... $^{}$

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ISMIS'11: Proceedings of the 19th international conference on Foundations of intelligent systems

June 2011

745 pages

ISBN:9783642219153

Editors:
Marzena Kryszkiewicz
Warsaw University of Technology, Warsaw, Poland
,
Henryk Rybinski
Warsaw University of Technology, Warsaw, Poland
,
Andrzej Skowron
The University of Warsaw, Warsaw, Poland
,
Zbigniew W. Raś
University of North Carolina, Charlotte, NC and Warsaw University of Technology, Warsaw, Poland

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 28 June 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 24 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Ha QHoang TNguyen LNguyen HSzałas ATran TTrong GHluchy LQuyet TCastelli EDuc KChi MTran V(2012)A bisimulation-based method of concept learning for knowledge bases in description logicsProceedings of the 3rd Symposium on Information and Communication Technology10.1145/2350716.2350753(241-249)Online publication date: 23-Aug-2012
https://dl.acm.org/doi/10.1145/2350716.2350753
Nguyen L(2011)A cut-free exptime tableau decision procedure for the description logic SHIProceedings of the Third international conference on Computational collective intelligence: technologies and applications - Volume Part I10.5555/2041845.2041908(572-581)Online publication date: 21-Sep-2011
https://dl.acm.org/doi/10.5555/2041845.2041908

Abstract

References

Cited By

Index Terms

Recommendations

ExpTime Tableaux for Checking Satisfiability of a Knowledge Base in the Description Logic $\mathcal{ALC}$

A cut-free calculus for second-order Gödel logic

Cut-free Sequent Calculus and Natural Deduction for the Tetravalent Modal Logic

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations