Institutional Repository

Modal satisifiability in a constraint logic environment

UnisaIR/Manakin Repository

Show simple item record

dc.contributor.advisor Britz, K. (Prof.) en
dc.contributor.advisor Hörne, T. (Mrs.) en
dc.contributor.author Stevenson, Lynette en
dc.date.accessioned 2009-08-25T10:59:12Z
dc.date.available 2009-08-25T10:59:12Z
dc.date.issued 2009-08-25T10:59:12Z
dc.date.submitted 2007-11-30 en
dc.identifier.uri http://hdl.handle.net/10500/2030
dc.description.abstract 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. en
dc.format.extent 1 online resource (vii, 179 leaves.)
dc.language.iso en en
dc.subject Modal satisfiability en
dc.subject Modal validity en
dc.subject Constraint satisfaction problem en
dc.subject Constraint solver en
dc.subject Tableau system en
dc.subject First-order translation en
dc.subject ECLiPSe en
dc.subject Modal logics K,KT,S4 en
dc.subject Constraint logic programming en
dc.subject.ddc 005.116
dc.subject.lcsh Computer algorithms
dc.subject.lcsh Business -- Data processing
dc.subject.lcsh Modality (Logic)
dc.subject.lcsh Constraint programming (Computer science)
dc.subject.lcsh Constraints (Artificial intelligence)
dc.subject.lcsh Programming (Computers)
dc.subject.lcsh Logic programming
dc.title Modal satisifiability in a constraint logic environment en
dc.type Thesis en
dc.description.department Computing en
dc.description.degree M.Sc. (Computer Science) en


Files in this item

This item appears in the following Collection(s)

  • Unisa ETD [4416]
    Electronic versions of theses and dissertations submitted to Unisa since 2003

Show simple item record

Search UnisaIR


Browse

My Account

Statistics