Renate A. Schmidt  @ NUS Home/Search
Context Related
| cs.man.ac.uk/~schmidt/publi...PhD.ps.gz Cached: PS.gz PS PDF Image Update Help From: cs.man.ac.uk/~schmidt/publicat... (more) Homepages: R.Schmidt HPSearch (Update Links) |
Rate this article:      (best)Comment on this article |
Abstract: This thesis studies the optimised functional translation of propositional modal logics to first-order logic, and first-order resolution as a means for realising modal reasoning. The optimised functional translation maps modal logics to a lattice of clausal logics, called path logics. The general apparatus of inference for path logics is theory resolution. We show that satisfiability in basic path logic and certain extensions can be decided by resolution and condensing without requiring... (Update)
Context of citations to this paper: More
.... For non transitive modal logics, good performance results have been obtained with the resolution theorem prover SPASS (Hustadt and Schmidt 1997, 1999a, Hustadt et al. 1998, Schmidt 1998b) Transitive relations play also an important role in automated deduction for first...
.... [12] or spass [38] handle modal formulas in this way, in some cases using extremely optimized translations like those investigated in [32, 37]. This approach has both advantages and disadvantages with respect to the tableau approach. On the one hand we can translate many...
Cited by: More
Resolution in Modal, Description and Hybrid Logic - Areces, de Nivelle, de Rijke (2002) (Correct)
The Complexity of Regularity in Grammar Logics - Demri (2001) (Correct)
A Resolution-Based Decision Procedure for Extensions of K4 - Ganzinger, Hustadt.. (1998) (Correct)
Similar documents based on text: More All
0.7: Optimised Modal Translation and Resolution - Schmidt (1997) (Correct)
0.6: Control Flow Graphs for Real-Time System Analysis.. - Theiling (2002) (Correct)
0.5: Programming Constraint Services - Schulte (2002) (Correct)
Related documents from co-citation: More All
3: Resolution-Based Decision Procedures for Subclasses of First-Order Logic (context) - Hustadt - 1999
2: Resolution calculi for modal logics (context) - Mints - 1989
2: URL httpspas (context) - URL, mpi et al. - 2001
BibTeX entry: (Update)
Schmidt, R. A. 1997. Optimised Modal Translation and Resolution. Doctoral dissertation, Universitat des Saarlandes, Saarbrucken, Germany. http://citeseer.comp.nus.edu.sg/707136.html More
@phdthesis{ schmidt97optimised,
author = "R. Schmidt",
title = "Optimised Modal Translation and Resolution",
school = "Universit{\"a}t des Saarlandes, Saarbr{\"u}cken, Germany",
year = "1997",
url = "citeseer.comp.nus.edu.sg/707136.html" }
Citations not processed or no citations identified.
Documents on the same site (http://www.cs.man.ac.uk/~schmidt/publications/): More
Hyperresolution for Guarded Formulae - Georgieva, Hustadt, Schmidt (2000) (Correct)
A Resolution-Based Decision Procedure for Extensions of K4 - Ganzinger, Hustadt.. (1998) (Correct)
Maslov's Class K Revisited - Hustadt, Schmidt (1999) (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.