This thesis describes a decision and minimization procedure for modal logic. The decision procedure answers the question of whether there exists a satisfying pointed model for a formula which obeys user-specified first-order conditions on the underlying frame. Then the minimization procedure produces a minimal model with respect to the number of worlds that satisfies the desired formula while obeying the requisite conditions on the underlying frame. A proof of correctness for the decision and minimization procedures is supplied, as well as a description of an implementation built upon the Enfragmo model expansion solver. / Graduate / 0984 / 0318 / wbkboyer@gmail.com
| Identifer | oai:union.ndltd.org:uvic.ca/oai:dspace.library.uvic.ca:1828/7462 |
| Date | 18 August 2016 |
| Creators | Boyer, Wanda B. K. |
| Contributors | Yap, Audrey, Kapron, Bruce M. (Bruce Michael) |
| Source Sets | University of Victoria |
| Language | English, English |
| Detected Language | English |
| Type | Thesis |
| Rights | Available to the World Wide Web, http://creativecommons.org/licenses/by-nc-sa/2.5/ca/ |
Page generated in 0.0024 seconds