U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In P. Lambrix, A. Borgida, M. Lenzerini, R. Moller, and P. Patel-Schneider, editors, Proceedings of the International Workshop on Description Logics, Linkoping, Sweden, 1999. CEUR.  @ NUS  Home/Search   Document Details and Download   Summary   Related Articles   Check

....distinguishing feature of HyLoRes is that it is not based on tableau algorithms but on (direct) resolution. HyLoRes implements a version of the given clause algorithm, which has become the skeleton underlying most first order provers. In contrast to translation based provers like MSPASS [17], HyLoRes performs resolution directly on the modal (or hybrid) input, with no translation into background logics. It is often said that hybrid logics combine interesting features from both modal and first order logics. In the same spirit, HyLoRes fuses ideas from state of the art first order ....

.... being the orientation of equalities so that we always replace nominals by nominals which are lower in a certain ordering. 4 Comparison and Testing The prototype is not yet meant to be competitive when compared with state of the art theorem provers for modal and description logics like MSPASS [17], DLP [20] FaCT [16] RACER [14] or SAT [11] On the one hand, the system is still in a preliminary stage of development (only very simple optimizations for hybrid logics have been implemented) and on the other hand hybrid and description languages are related but different. H ( #) is ....

[Article contains additional citation context not shown here]

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In Lambrix et al. [18], pages 136--137.

....The implementation of efficient decision procedures for modal logics is a major research problem in automated deduction. Several systems have been developed, like Kris [1,2] Ksat [3,4] LWB [5] FaCT [6] and more recently sat [7,8] KK [9] dlp [10] HAM ALC [11] KtSeqC [12] and MSPASS [13]. In the last few years, a competition is run in conjunction with the Tableaux conferences, aiming at stimulating the development of effective systems. The last four of the above cited systems participated at the last competition, and as the organizer Fabio Massacci writes 1 The winner ....

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In P. Lambrix, A. Borgida, M. Lenzerini, R. Moller, and P. Patel-Schneider, editors, Collected Papers from the International Description Logics Workshop (DL'99), pages 136--137. CEUR, July 1999.

....speaking, L is ALC extended with full Boolean operators on roles, the inverse operator on roles, and an identity role relating each individual to itself. We argue that all operators present in L are standard description logic operators: see, e.g. 8, 5, 18] for Boolean operators on roles, [16] for Boolean operators on roles and inverse roles, and [6] for (some) Boolean operators on roles, inverse, and the identity role. Moreover, the modal logic equivalent of L is also a standard modal logic; see, e.g. 11, 15, 19] for Boolean operators on modal parameters, 4, 12, 26] for ....

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In Proc. of DL'99, pages 136--137. Linkoping University, 1999.

....speaking, L is ALC extended with full Boolean operators on roles, the inverse operator on roles, and an identity role relating each individual to itself. We argue that all operators present in L are standard description logic operators: see, e.g. 8, 5, 18] for Boolean operators on roles, [16] for Boolean operators on roles and inverse roles, and [6] for (some) Boolean operators on roles, inverse, and the identity role. Moreover, the modal logic equivalent of L is also a standard modal logic; see, e.g. 11, 15, 19] for Boolean operators on modal parameters, 4, 12, 26] for ....

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In Proc. of DL'99, pages 136-137. Linkoping University, 1999.

....The implementation of ecient decision procedures for modal logics is a major research problem in automated deduction. Several systems have been developed, like Kris [1, 2] Ksat [3, 4] LWB [5] FaCT [6] and more recently sat [7, 8] KK [9] dlp [10] HAM ALC [11] KtSeqC [12] and MSPASS [13]. A competition is run in conjunction with the Tableaux conferences, aiming at stimulating the development of e ective systems. At the last competition, the last four of the above cited systems participated, and as the organizer Fabio Massacci of the competition writes [14] The winner is ....

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In P. Lambrix, A. Borgida, M. Lenzerini, R. Moller, and P. PatelSchneider, editors, Collected Papers from the International Description Logics Workshop (DL'99), pages 136-137. CEUR, July 1999.

No context found.

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In P. Lambrix, A. Borgida, M. Lenzerini, R. Moller, and P. Patel-Schneider, editors, Proceedings of the International Workshop on Description Logics, Linkoping, Sweden, 1999. CEUR.

No context found.

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In Proc. of DL'99, pages 136--137. Linkoping University, 1999.

No context found.

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In Lambrix et al. [9], pages 136-137.

No context found.

U. Hustadt, R. A. Schmidt, and C. Weidenbach. MSPASS: Subsumption testing with SPASS. In Lambrix et al. [15], pages 136-137.

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.