An SAT-based Decision Procedure for ALC

Fausto Giunchiglia and Roberto Sebastiani

The goal of this paper is to describe and thoroughly test a decision procedure, called KSAT, checking satisfiability in the terminological logic ACC. KSAT is said to be SATbased as it is defined in terms of a decision procedure for propositional satisfiability (SAT). The tests are performed comparing KSAT with, among other procedures, KRIS, a state-of-the-art tableau-based implementation of a decision procedure for ALe. KSAT outperforms KRIS of orders of magnitude. Furthermore, the empirical results highlight an intrinsic weakeness that tableau-based decision procedures have with respect to SATbased decision procedures.

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.