Computational Space Efficiency and Minimal Model Generation for Guarded Formulae

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

In R. Nieuwenhuis and A. Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning (Proc. LPAR'2001). Lecture Notes in Artificial Intelligence 2250, Springer, 85-99. BiBTeX, DOI Link (Copyright © Springer).

This paper describes a number of hyperresolution-based decision procedures for a subfragment of the guarded fragment. We first present a polynomial space decision procedure of optimal worst-case space and time complexity for the fragment under consideration. We then consider minimal model generation procedures which construct all and only minimal Herbrand models for guarded formulae. These procedures are based on hyperresolution, (complement) splitting and either model constraint propagation or local minimality tests. All the procedures have concrete application domains and are relevant for multi-modal and description logics that can be embedded into the considered fragment.


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

Last modified: 19 May 09
Copyright © 2001,2 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk