Hans Jürgen Ohlbach  @ NUS Home/Search
Context Related
| dcs.kcl.ac.uk/staf...olution_cade.ps.gz Cached: PS.gz PS PDF Image Update Help From: dcs.kcl.ac.uk/staff/o...abstracts (more) (Enter author homepages) |
Rate this article:      (best)Comment on this article |
Abstract: A syntax transformation is presented that eliminates the modal logic operators from modal logic formulae by shifting the modal context information to the term level. The formulae in the transformed syntax can be brought into conjunctive normal form such that a clause based resolution calculus without any additional inference rule, but with special modal unification algorithms, can be defined. The method works for first-order modal logics with the two operators # and à and with constant-domain... (Update)
Context of citations to this paper: More
.... validity, which underly these systems, have been extended to intuitionistic logic and the modal logics K,K4,D,D4,T,S4, and S5 [17, 28, 29, 27]. On this basis the existing proof methods have been extended accordingly [18, 19] in order to develop a coherent theorem prover...
.... logic since this allows us to use the wealth of knowledge in first order theorem proving to mechanize modal deduction (see e.g. [17, 20, 12, 5]) Let FO n be the fragment of classical first order logic using at most n individual variables and no function symbols. Any modal...
Cited by: More
Building Logic Toolboxes - Heguiabehere (2003) (Correct)
Multimodal Logic Programming - Nguyen (2003) (Correct)
Multimodal Logic Programming and Its Applications to Modal.. - Nguyen (2003) (Correct)
Active bibliography (related documents): More All
0.0: Relations Between Propositional Normal Modal Logics: An Overview - Goré, al. (1995) (Correct)
0.0: Labelled Proofs for Quantified Modal Logic - Artosi, Benassi, Governatori.. (1996) (Correct)
0.0: Ground and Free-Variable Tableaux for Variants of Quantified.. - Mayer, Cerrito (2001) (Correct)
Similar documents based on text: More All
0.1: A Set-Theoretic Approach to Automated Deduction in Graded.. - Montanari, Policriti (1997) (Correct)
0.1: Killer Transformations - Hans Jürgen Ohlbach, Dov Gabbay.. (1994) (Correct)
0.1: Automated Support for the Development of Non-Classical Logics - Ullrich Hustadt (Correct)
Related documents from co-citation: More All
25: Proof Methods for Modal and Intuitionistic Logics (context) - Fitting - 1983
21: Automated Deduction in Non-Classical Logics (context) - Wallen - 1990
20: A machine-oriented logic based on the resolution principle (context) - Robinson - 1965
BibTeX entry: (Update)
H. J. Ohlbach. A resolution calculus for modal logics. Ph.D. Thesis, Universitat Kaiserslautern, 1988. http://citeseer.comp.nus.edu.sg/121270.html More
@misc{ ohlbach88resolution,
author = "H. Ohlbach",
title = "A resolution calculus for modal logics",
text = "H. J. Ohlbach. A resolution calculus for modal logics. Ph.D. Thesis, Universitat
Kaiserslautern, 1988.",
year = "1988",
url = "citeseer.comp.nus.edu.sg/121270.html" }
Citations (may not include all citations):242 Proof methods for modal and intuitionistic logics (context) - Fitting - 1983
203 An Introduction to Modal Logics (context) - Hughes, Cresswell - 1968
11 Modal Theorem Proving (context) - Abadi, Manna - 1986
1 Paramodulation and theorem provcing in first order theories .. (context) - Robinson, Wos - 1969
The graph only includes citing articles where the year of publication is known.
Documents on the same site (http://www.dcs.kcl.ac.uk/staff/ohlbach/homepage/publications/conferences/abstracts.html): More
Compilation of Recursive Two-Literal Clauses into Unification.. - Ohlbach (1990) (Correct)
SCAN - Elimination of Predicate Quantifiers - Ohlbach (Correct)
Role Hierarchies and Number Restrictions - Ohlbach, Koehler (1997) (Correct)
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.