U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbrucken, Germany, 1999.  @ NUS  Home/Search   Document Not in Database   Summary   Related Articles   Check

....when indirect methods are used. In translation based resolution calculi for modal logics, one translates modal languages into a large background language (typically rst order logic) and devises strategies that guarantee termination for the fragment corresponding to the original modal language [22, 29, 17, 5]. First order resolution provers like bliksem [12] or spass [38] handle modal formulas in this way, in some cases using extremely optimized translations like those investigated in [32, 37] This approach has both advantages and disadvantages with respect to the tableau approach. On the one hand we ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Universitat des Saarlandes, Saarbrucken, Germany, 1999.

.... fragment of xed point rst order logic in which can be naturally embedded the modal calculus (see e.g. Koz83] Once an interesting decidable fragment is identi ed, the design of decision procedures that meet the best worst case complexity upper bounds is often the next step (see e.g. [Sch97, Niv98, Hus99]) However, even if your favorite modal logic can be embedded in a known decidable fragment of second order logic, the characterization of the worst case complexity of your logic is not straightforward from the complexity of the second order fragment. For instance, the standard modal logic K can ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Fakultat der Universitat des Saarlandes, 1999.

....when indirect methods are used. In translation based resolution calculi for modal logics, one translates modal languages into a large background language (typically rst order logic) and devises strategies that guarantee termination for the fragment corresponding to the original modal language [22, 29, 17, 5]. First order resolution provers like bliksem [12] or spass [38] handle modal formulas in this way, in some cases using extremely optimized translations like those investigated in [32, 37] This approach has both advantages and disadvantages with respect to the tableau approach. On the one hand we ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Universitat des Saarlandes, Saarbrucken, Germany, 1999.

....model property, and ordered resolution for this fragment. We have proved completeness and termination of the procedure. Previous work on resolution based decision procedures for ( rst order fragments corresponding to) modal logic have either used far more complex and less intuitive orderings [Hus99] or have been based on changes to the underlying semantics [Sch99] While resolution based, our decision procedure incorporates many of the fundamental ideas underlying tableaux basd decision procedures for modal logic. For instance, in a typical tableau system, new successor states are created ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of FirstOrder Logic. PhD thesis, Universitat des Saarlandes, 1999.

....ordering on variables and arguments. To our knowledge, of the mentioned logics, uted logic has thus far not been studied in the context of resolution. For all other logics mentioned above resolution based decision procedures have been proposed, in some cases even several di erent re nements exist [1, 2, 5, 9]. Fluted logic is also of interest for its relationship to non classical logics. Fluted logic may be viewed as a generalisation of propositional modal logic, just as the guarded fragments can. The properties uted logic is known to share with modal logics are decidability and the nite model ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbrucken, Germany, 1999.

No context found.

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbrucken, Germany, 1999.

....one obtains generic decision procedures for modal logics and the corresponding description logics. Resolution decision procedures have been developed for the guarded fragment [12, 20] for Maslov s class K [43] for fluted logic [71] and various other classes related to modal logics, see e.g. [17, 29, 40]. In this paper we consider only the relationship to a fragment of clausal logic based on the two variable fragment. The fragment is called DL # [13] It is a variation of the class of DL clauses, that was introduced in [45] with the purpose of handling expressive description logics. In order to ....

....procedure we have to show that it is complete, and terminating. The completeness follows from Theorem 5.1. 10 Termination is a consequence of Theorem 6. 1, and the fact that the restriction derives only clauses that are within DL # , or splittable clauses with split components in DL # (cf. [40, 45]) #) Let # be a finite set of relational properties expressible in DL # . Let N be the clausal form of # Def # #(#) where # is any modal formula in L and # is defined as in Theorem 6.3. Then: i) Any derivation from N in R (up to redundancy) terminates in double exponential time. ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbrucken, Germany, 1999.

.... the extent to which they are able to map modal logics into rst order logic, the decidability of the fragments of rst order logic into which modal formulae are translated by rst order theorem proving techniques, and the computational behaviour of rst order theorem provers on these fragments [6, 13, 15, 21]. In the following we present a decision procedure for the satis ability problem in the core KARO logic consisting of three components: i) a normalisation function which reduces complex action formulae to atomic action subformulae, ii) a particular translation of normalised formulae into a ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Universitat des Saarlandes, Saarbrucken, Germany, 1999.

No context found.

U. Hustadt, Resolution-Based Decision Procedures for Subclasses of First-Order Logic, Ph.D. thesis, Universitt des Saarlandes, Saarbr cken, Germany, 1999.

.... parameters in existing theorem proving frameworks (Bachmair and Ganzinger, 1997) For the optimised functional translation this has been demonstrated in (Schmidt, 1997; Schmidt, 1999) while the relational and semi functional translation have been considered in (Ganzinger et al. 1999a; Hustadt, 1999; Hustadt and Schmidt, 1999b; Hustadt and Schmidt, 1998) Third, there are general guidelines for choosing these parameters in the right way to enforce termination and the hard part is to prove that termination is guaranteed. The most common approach uses ordering refinements of resolution to ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Universit at des Saarlandes, Saarbr ucken, Germany, 1999.

.... ; and ALB where the relations satisfy additional rst order restrictions including re exivity, irre exivity, seriality, symmetry, density, relational inclusion, etc [3, 9] For the optimised functional and semi functional translation of multi modal K (m) in which modalities may be serial [6, 16]. For the guarded fragment and other solvable fragments [4, 8] 3 3 Implementation mspass is implemented in ANSI C and di ers from spass only in the extended input language and the translation routines. The inference loop in mspass is controlled by two sets of clauses: The set of worked o ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbrucken, Germany, 1999.

....and bottom role, conjunction, disjunction, negation and converse. ffl For the optimised functional translation of ALC with or without serial, reflexive or transitive roles [ 15 ] ffl For the semi functional translation of ALC with or without serial, reflexive, symmetric or transitive roles [ 5 ] Implementation Both spass and mspass are implemented in ANSI C. The translation routines of mspass have alpha status (there are plans to change the input syntax slightly) Performance Extensive testing has been done with different versions of spass but as yet not with mspass. The tests ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbrucken, 1999. Submitted.

....and bottom role, conjunction, disjunction, negation and converse. ffl For the optimised functional translation of ALC with or without serial, reflexive or transitive roles [ 15 ] ffl For the semi functional translation of ALC with or without serial, reflexive, symmetric or transitive roles [ 5 ] Implementation Both spass and mspass are implemented in ANSI C. The translation routines of mspass have alpha status (there are plans to change the input syntax slightly) Performance Extensive testing has been done with different versions of spass but as yet not with mspass. The tests ....

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Univ. d. Saarlandes, Saarbrucken, 1999. Submitted.

No context found.

U. Hustadt. Resolution-Based Decision Procedures for Subclasses of First-Order Logic. PhD thesis, Universitat des Saarlandes, Saarbrucken, Germany, 1999.

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.