Thumbnail
Access Restriction
Open

Author Brand, Sebastian ♦ Gennari, Rosella ♦ Rijke, Maarten De
Source CiteSeerX
Content type Text
Publisher Springer
File Format PDF
Language English
Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science
Subject Keyword Decision Procedure ♦ Sat-based Model ♦ Constraint Satisfaction Problem ♦ Constraint-based Method ♦ First-order Logic ♦ Constraint Method ♦ Modal-like Formalism ♦ Finite Constraint Satisfaction Problem ♦ Transition System ♦ Guarded Form ♦ Modal Satisfiability ♦ Appropriate Set ♦ Constraint Solver ♦ Description Logic ♦ Propositional Logic ♦ Modal Search Tree ♦ Specialised Constraint ♦ Modal Satisfiability Problem ♦ Basic Modal Formula
Description Modal and modal-like formalisms such as temporal or description logics go beyond propositional logic by introducing operators that allow for a guarded form of quantification over states or paths of transition systems. Thus, they are more expressive than propositional logic, yet computationally better behaved than first-order logic. We propose constraint-based methods to model and solve modal satisfiability problems. We model the satisfiability of basic modal formulas via appropriate sets of finite constraint satisfaction problems, and then resolve these via constraint solvers. The domains of the constraint satisfaction problems contain other values than just the Boolean 0 or 1; for these values, we create specialised constraints that help us steer the decision procedure and so keep the modal search tree as small as possible. We show experimentally that this constraint modelling gives us a better control over the decision procedure than existing SAT-based models.
Educational Role Student ♦ Teacher
Age Range above 22 year
Educational Use Research
Education Level UG and PG ♦ Career/Technical Study
Learning Resource Type Article
Publisher Date 2004-01-01
Publisher Institution Recent Advances in Constraints, 2003, volume 3010 of LNAI