Ordered E-Resolution and Path Logics

Schmidt, R. A. (Jan. 1998)

Manuscript. BiBTeX, with access restrictions: PostScript

Ordering refinements are particularly useful for avoiding unnecessary search and for obtaining resolution decision procedures. This paper presents a general framework for ordered E-resolution, allowing arbitrary selection of negative literals and providing a general notion of redundancy elimination. As different theories bring forth different and very special simplification rules, having an im-built general scheme for eliminating redundancy is especially useful. The strength of the framework is demonstrated for certain path logics arising by the optimised functional translation method from serial propositional modal logics.

Renate A. Schmidt
Home | Publications | FM Group | School | Man Univ

Last modified: 24 Jan 2000
Copyright © 1996,7,8 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk