U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. J. Automated Reasoning, 28(2):205--232, 2002. @ NUS Home/Search Document Details and Download
Summary Related Articles Check |
This paper is cited in the following contexts:
A Principle for Incorporating Axioms into the First-Order.. - Schmidt, Hustadt (2004) Self-citation (Hustadt Schmidt) (Correct)
No context found.
U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. J. Automated Reasoning, 28(2):205--232, 2002.
Mechanised Reasoning and Model Generation for Extended Modal.. - Schmidt, Hustadt (2003) Self-citation (Hustadt Schmidt) (Correct)
No context found.
U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. Journal of Automated Reasoning, 28(2):205--232, 2002.
Mechanised Reasoning and Model Generation for Extended Modal.. - Schmidt, Hustadt (2003) Self-citation (Hustadt Schmidt) (Correct)
....we have various options. Ordering refinements provide decision procedures for very expressive logics, while if we are interested in generating models for satisfiable formulae selection based refinements (or hyperresolution) are more natural (Fermuller et al. 18, 17] Leitsch [50] Hustadt et al. [30, 45, 44, 47]) We discuss an ordered resolution decision procedure for a class of clauses induced by K (m) #, #) in Section 6. In Section 7 we describe a refinement which relies solely on the selection of negative literals for certain extensions of K (m) #, #) This refinement has the property ....
....and inverse roles. Acyclic TBox statements, and both concept and role ABox statements are also in the scope of the last theorem. 8 Simulating tableaux Selection refinements of resolution (and hyperresolution) are closely related to standard modal tableau calculi and description logic systems [13, 17, 44, 45, 47]. In this section investigate simulation relationships between the selection based resolution procedure R and Massacci s single step prefixed tableau calculi [53] There are three notions of simulation [13] polynomial simulation of derivations, polynomial simulation of search, and step wise ....
[Article contains additional citation context not shown here]
U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. Journal of Automated Reasoning, 28(2):205--232, 2002. 27
A New Clausal Class Decidable by Hyperresolution - Georgieva, Hustadt, Schmidt (2002) Self-citation (Hustadt Schmidt) (Correct)
....based theorem prover with splitting can provide a polynomial space decision procedure for GF1 . We also describe several solutions to the problem of generating minimal Herbrand models for GF1 . In [13, 14] we have used structural transformation (or definitional form transformation, cf. e.g. [3, 19]) to transform GF1 formulae into clausal form. While it is straightforward to give a schematic characterisation of the resulting sets of clauses, it is much more di#cult to state the conditions which an arbitrary set of clauses needs to satisfy so that it shares most or all the properties of ....
.... basic multi modal logic K (m) and the corresponding description logic [25] For example, if we translate formulae of K (m) into first order logic and transform the resulting formulae into clausal form using structural transformation, then the clauses we obtain take one of the following forms [10, 18, 19]. Q 1 (a) # R(x, Q 2 (y) R(x, f(x) Q 2 (f(x) 6 Furthermore, we can always define an acyclic dependency relation on the predicate symbols in these clauses and associate groupings (0, 1) and (1, 1) with every unary and binary predicate symbol, respectively, such that ....
[Article contains additional citation context not shown here]
U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. In SAT 2000.
Reasoning about agents in the KARO framework - Hustadt, Dixon, Schmidt.. (2001) (1 citation) Self-citation (Hustadt Schmidt) (Correct)
No context found.
U. Hustadt and R. A. Schmidt, "Using resolution for testing modal satisfiability and building models," To appear in the SAT
Hyperresolution for Guarded Formulae - Georgieva, Hustadt, Schmidt (2000) (2 citations) Self-citation (Hustadt Schmidt) (Correct)
....fragment. In this paper we continue the line of investigation making use, however, of the close correspondence between tableauxbased decision procedure for modal logics and hyperresolution combined with splitting on an encoding of modal formulae in clausal logic, as previously demonstrated in [9, 20], and in [18, 19] for description logics. By using a structure preserving transformation of guarded formulae into clausal form we are able to recast the method of Lutz et al. in a first order setting using in particular hyperresolution with splitting. In this setting it is immediately clear that ....
....for reasoning about guarded formulae. Generally hyperresolution is not a decision procedure for the entire guarded fragment. A simple example is provided by the guarded formula p(y) # #x(p(x) # #z(p(z) # #) with clausal form p(a) p(x) # p(f(x) The method of proving termination used in [9, 20] in the case of modal logics does not generalise to GF1 . We investigate a di#erent argument adapted from Lutz et al. which takes into consideration the form of the derived clauses. The obtained results are more general than those previously known. Another aim is to study how the method relates ....
[Article contains additional citation context not shown here]
U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. To appear in the SAT 2000 Special Issue of J. Automated Reasoning, 2000.
Resolution-Based Methods for Modal Logics - de Nivelle, SCHMIDT, al. (2000) (1 citation) Self-citation (Hustadt Schmidt) (Correct)
....various options. Ordering refinements provide decision procedures for very expressive logics, while if we are interested in generating models for satisfiable formulae selection based refinements (or hyperresolution) are more natural (Fermuller et al. 12, 13] Leitsch [30] Hustadt and Schmidt [28, 29]) We will describe three resolution decision procedures: an ordered resolution decision procedure for a class of clauses induced by K (m) #, #, #) Section 5) an ordering refinement combined with a selection function for the guarded fragment (Section 6) and a refinement which relies ....
....of formulae. Section 3 defines the syntax and semantics of the logic K (m) #, #, #) and specifies the standard translation mapping into first order logic. A general framework of ordered resolution and selection is described in Section 4. This overview is based on the papers [14, 28, 29]. Some results have been improved and others are new. The definition of the class DL # in Section 5, generalises the class of DL clauses from [28] Section 7 includes a new complexity result. The results for extensions of K (m) #, #, #) with frame properties are slightly more general than in ....
[Article contains additional citation context not shown here]
U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. To appear in the SAT 2000 Special Issue of J. of Automated Reasoning, 2000. 292 Resolution-Based Methods for Modal Logics
Optimising minimal Herbrand model generation procedures - Georgieva (2003) (Correct)
No context found.
U. Hustadt and R. A. Schmidt. Using resolution for testing modal satisfiability and building models. Journal of Automated Reasoning, 28(2):205--232, 2002.
Online articles have much greater impact More about CiteSeer.IST at NUS Add search form to your site Submit documents Feedback
CiteSeer.IST at NUS - Copyright Penn State and NEC. Hosted by the School of Computing, National University of Singapore.