Optimised ExpTime Tableaux for𝒮ℋℐ𝒩over Finite Residuated Lattices | Zendy

Jian Huang | Zendy; Xinye Zhao | Zendy; Jianxing Gong | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Optimised ExpTime Tableaux for𝒮ℋℐ𝒩over Finite Residuated Lattices

Author(s) -

Jian Huang,

Xinye Zhao,

Jianxing Gong

Publication year - 2014

Publication title -

journal of applied mathematics

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.307

H-Index - 43

eISSN - 1687-0042

pISSN - 1110-757X

DOI - 10.1155/2014/702326

Subject(s) - satisfiability , description logic , computer science , residuated lattice , algorithm , semantics (computer science) , consistency (knowledge bases) , fuzzy logic , exptime , theoretical computer science , mathematics , discrete mathematics , artificial intelligence , computational complexity theory , programming language , pspace

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research