@inbook{0acaa9680e7e49758d6ae8e7cf91fa74,
title = "Computational space efficiency and minimal model generation for guarded formulae",
abstract = "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.",
keywords = "Modal Logic, Decision Procedure, Description Logic, Predicate Symbol, Model Constraint",
author = "L. Georgieva and Ullrich Hustadt and R.A. Schmidt",
year = "2001",
month = nov,
day = "21",
language = "English",
isbn = "9783540429579",
series = "Lecture Notes in Computer Science",
publisher = "Springer Berlin",
pages = "85--99",
editor = "Robert Nieuwenhuis and Voronkov, {Andrei }",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning",
address = "Germany",
}