Hyperresolution for Guarded Formulae

Georgieva, L. and Hustadt, U. and Schmidt, R. A. (2000)

In Baumgartner, P. and Zhang, H. (eds), Proceedings of the Third International Workshop on First-Order Theorem Proving (FTP 2000). Fachberichte Informatik 5/2000, Institut für Informatik, Universität Koblenz-Landau, 101-112. BiBTeX, PostScript.

This paper investigates the use of hyperresolution as a decision procedure and model builder for guarded formulae. In general hyperresolution is not a decision procedure for the entire guarded fragment. However we show that there are natural fragments which can be decided by hyperresolution. In particular, we prove decidability of hyperresolution with or without splitting for the fragment GF1- and point out several ways of extending this fragment without loosing decidability. As hyperresolution is closely related to various tableaux methods the present work is also relevant for tableaux methods. We compare our approach to hypertableaux, and mention the relationship to other clausal classes which are decidable by hyperresolution.

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

Last modified: 27 Apr 2001
Copyright © 2000 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk