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.
CITATION STYLE
Georgieva, L., Hustadt, U., & Schmidt, R. A. (2001). Computational space efficiency and minimal model generation for guarded formulae. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2250, pp. 85–99). Springer Verlag. https://doi.org/10.1007/3-540-45653-8_6
Mendeley helps you to discover research relevant for your work.