R. Schmidt. Optimised Modal Translation and Resolution. PhD thesis, Universit at des Saarlandes, Saarbrucken, Germany, 1997.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

.... 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 can translate many systems into the same background language and hence explore di erent, and also combined, systems without the need to modify the prover. But empirical tests show that ....

R. Schmidt. Optimised Modal Translation and Resolution. PhD thesis, Universit at des Saarlandes, Saarbrucken, Germany, 1997.

.... 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 ....

R. Schmidt. Optimised Modal Translation and Resolution. PhD thesis, Fakultat der Universitat des Saarlandes, 1997.

.... 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 can translate many systems into the same background language and hence explore di erent, and also combined, systems without the need to modify the prover. But empirical tests show that ....

R. Schmidt. Optimised Modal Translation and Resolution. PhD thesis, Universit at des Saarlandes, Saarbrucken, Germany, 1997.

.... pre computed term depth bounds, whereby termination can be guaranteed (Schmidt 1998a, 1998b) However, in practice this solution is very poor (Hustadt et al. 1998) For non transitive modal logics, good performance results have been obtained with the resolution theorem prover SPASS (Hustadt and Schmidt 1997, 1999a, Hustadt et al. 1998, Schmidt 1998b) Transitive relations play also an important role in automated deduction for first order logic. A general resolution calculus designed for binary relations satisfying the general scheme R i ffi R j R k (including equality) is by Bachmair and ....

....OE a new name Q . Such transformations were used by Tseitin (1970) in studying the relative complexity of proof systems of propositional logic. They form a standard technique not only in the connection with resolution decision procedures (de Nivelle 1998, Hustadt and Schmidt 1998, 1999b, Schmidt 1997), but allow also linear transformation of first order formulae into clausal form (Baaz et al. 1994, Boy de la Tour 1992, Nonnengart et al. 1998) Let be a subset of Pos(OE) for a first order formula OE in negation normal form. We associate with each position of a new predicate symbol Q Seriality ....

Schmidt, R. A. 1997. Optimised Modal Translation and Resolution. Doctoral dissertation, Universitat des Saarlandes, Saarbrucken, Germany.

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.