The modal satisfiability problem has to date been solved using either a specifically
designed algorithm, or by translating the modal logic formula into a different class
of problem, such as a first-order logic, a propositional satisfiability problem or a constraint
satisfaction problem. These approaches and the solvers developed to support
them are surveyed and a synthesis thereof is presented.
The translation of a modal K formula into a constraint satisfaction problem,
as developed by Brand et al. [18], is further enhanced. The modal formula, which
must be in conjunctive normal form, is translated into layered propositional formulae.
Each of these layers is translated into a constraint satisfaction problem and solved
using the constraint solver ECLiPSe. I extend this translation to deal with reflexive
and transitive accessibility relations, thereby providing for the modal logics KT and
S4. Two of the difficulties that arise when these accessibility relations are added
are that the resultant formula increases considerably in complexity, and that it is
no longer in conjunctive normal form (CNF). I eliminate the need for the conversion
of the formula to CNF and deal instead with formulae that are in negation normal
form (NNF). I apply a number of enhancements to the formula at each modal layer
before it is translated into a constraint satisfaction problem. These include extensive
simplification, the assignment of a single value to propositional variables that occur
only positively or only negatively, and caching the status of the formula at each node
of the search tree. All of these significantly prune the search space. The final results
I achieve compare favorably with those obtained by other solvers. / Computing / M.Sc. (Computer Science)
| Identifer | oai:union.ndltd.org:netd.ac.za/oai:union.ndltd.org:unisa/oai:uir.unisa.ac.za:10500/2030 |
| Date | 30 November 2007 |
| Creators | Stevenson, Lynette |
| Contributors | Britz, K. (Prof.), Hörne, T. (Mrs.) |
| Source Sets | South African National ETD Portal |
| Language | English |
| Detected Language | English |
| Type | Thesis |
| Format | 1 online resource (vii, 179 leaves.) |
Page generated in 0.0033 seconds