Improvement of a tableau-based algorithm and the finite-step halting theorem

MaRDI QIDQ3641424zbMATH OpenFDO

Authors Guojun Wang, Bijing Li

Publication date 11 November 2009

zbMATH Keywords

description logicfinite-step halting theoremtableau-based algorithm

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Knowledge representation (68T30)

Recommendations

• EXPtime tableaux for ALC
• ExpTime tableaux for \(\mathcal {ALC}\) using sound global caching
• Simplification rules for constrained formula tableaux
• Inconsistency-tolerant description logic. II: A tableau algorithm for \(\mathcal{CALC}^{\mathsf C}\)
• A more efficient tableaux procedure for simultaneous search for refutations and finite models

This page was built for publication: Improvement of a tableau-based algorithm and the finite-step halting theorem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3641424)