Optimised ExpTime Tableaux for over Finite Residuated Lattices

Jian Huang, Xinye Zhao and Jianxing Gong

Journal of Applied Mathematics, 2014, vol. 2014, 1-15

Abstract:

This study proposes to adopt a novel tableau reasoning algorithm for the description logic with semantics based on a finite residuated De Morgan lattice. The syntax, semantics, and logical properties of this logic are given, and a sound, complete, and terminating tableaux algorithm for deciding fuzzy ABox consistency and concept satisfiability problem with respect to TBox is presented. Moreover, based on extended and/or completion-forest with a series of sound optimization technique for checking satisfiability with respect to a TBox in the logic, a new optimized ExpTime (complexity-optimal) tableau decision procedure is presented here. The experimental evaluation indicates that the optimization techniques we considered result in improved efficiency significantly.

Date: 2014
References: Add references at CitEc
Citations:

Downloads: (external link)
http://downloads.hindawi.com/journals/JAM/2014/702326.pdf (application/pdf)
http://downloads.hindawi.com/journals/JAM/2014/702326.xml (text/xml)

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:hin:jnljam:702326

DOI: 10.1155/2014/702326

Access Statistics for this article

More articles in Journal of Applied Mathematics from Hindawi
Bibliographic data for series maintained by Mohamed Abdelhakeem ().