G. Mints. Resolution calculi for modal logics. amst, 143:1--14, 1989.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....it is natural to wonder why direct resolution methods for modal languages don t gure in the picture. Designing resolution methods that can directly (without translation into large background languages) be applied to modal logics, received some attention in the late 1980s and early 1990s [20, 30, 16]. Also, the rst (non clausal) resolution methods for temporal languages go back to that period with the work of Abadi and Manna [1] Recently, new results on clausal temporal resolution have been presented (see [18] But even though we might sometimes think of modal languages as a simple ....

....by (A1) we can infer by ( that (p; p 2r q) p; p 2r q; 2r q) this already involves some simpli cations) An application of (31) allows us to perform this inference under 3. As we have just seen, the direct resolution method for modal logics presented in [20] and, similarly, those in [21, 30, 16]) performs resolution inside modalities, leading to a proliferation of deductive rules. In the next sections we develop a direct resolution method for modal, description and hybrid logic that retains as much of the lean onerule character of traditional resolution methods as possible. The key ....

G. Mints. Resolution calculi for modal logics. amst, 143:1-14, 1989.

....it is natural to wonder why direct resolution methods for modal languages don t gure in the picture. Designing resolution methods that can directly (without translation into large background languages) be applied to modal logics, received some attention in the late 1980s and early 1990s [20, 30, 16]. Also, the rst (non clausal) resolution methods for temporal languages go back to that period with the work of Abadi and Manna [1] Recently, new results on clausal temporal resolution have been presented (see [18] But even though we might sometimes think of modal languages as a simple ....

....by (A1) we can infer by ( that (p; p 2r q) p; p 2r q; 2r q) this already involves some simpli cations) An application of (31) allows us to perform this inference under 2. As we have just seen, the direct resolution method for modal logics presented in [20] and, similarly, those in [21, 30, 16]) performs resolution inside modalities, leading to a proliferation of deductive rules. In the next sections we develop a direct resolution method for modal, description and hybrid logic that retains as much of the lean onerule character of traditional resolution methods as possible. The key ....

G. Mints. Resolution calculi for modal logics. amst, 143:1-14, 1989.

....is required. 5. Structural transformation Structural transformation, also known as renaming or transformation to de nitional form, is a standard technique for transforming formulae into a more suitable normal form, and is used in many areas, including automated deduction [4, 38, 41] modal logic [33, 34] and description logics [3] In this paper its primary purpose is to keep a tight link between the structure of modal formulae and their translated clausal form. Let Pos( be the set of positions of a rst order formula . If is a position in , then j denotes the subformula of at ....

Mints, G.: 1989, `Resolution Calculi for Modal Logics'. American Mathematical Society Translations 143, 1-14.

....logics have been proposed. 21] presents a system in which explicit notation is introduced to denote possible worlds. This is related to the tableau systems of [7] and some of those in [9] see also [24] Most competing systems do not use this device though. See [1] 2] 14] 6] 5] 3] [17], 19] and [20] The idea of context is explicit or implicit in various systems proposed for modal logics. In a Kripke model a modal operator corresponds to a shift from one possible world to another. Di#erent parts of a formula can be within the scopes of di#erent modal operators, and so may not ....

G. E. Mints, Resolution calculi for modal logics, Eesti NSV Tead. Akad. Toimetised Fuus-Mat. vol 35, pp 279--290 (1986).

....standard textbooks on modal logic render decision procedures that are not practical. More practical are semantic tableaux methods, but they suffer from the non determinism due to the implicit or explicit presence of accessibility relations and in many cases deduction can become quite unmanageable. Mints 1989 proposes a resolution calculus adapted and extended for modal propositional formulae. This method is a direct inference method, it manipulates modal formulae. We use a resolution calculus too. But in contrast to Mints, we use To appear in Advances in Modal Logic 96 M. Kracht, M. de Rijke, H. ....

Mints, G. 1989. Resolution Calculi for Modal Logics. Amer. Math. Soc. Transl.

....systems for first order logic, modal tableaux systems are special purpose systems with the characteristic properties of accessibility built in. Fine (1975) uses a reduction to normal form from which finite models can be constructed. Other practical methods use resolution calculi. For example, Mints (1986, 1989, 1990) proposes a resolution calculus adapted and extended for modal propositional formulae. We use a resolution calculus too. But in contrast to Mints, we use the classical resolution calculus for predicate logic without changing it. Our method is indirect in that we manipulate first order ....

Mints, G. (1989), Resolution calculi for modal logics, Amer. Math. Soc. Transl.

No context found.

G. Mints. Resolution calculi for modal logics. amst, 143:1--14, 1989.

Online articles have much greater impact   More about CiteSeer.IST at NUS   Add search form to your site   Submit documents   Feedback  

CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.