MSPASS: Modal Reasoning by Translation and First-Order Resolution

mspass is an extension of the first-order theorem prover spass, which can be used as a modal logic theorem prover, a theorem prover for description logics and a theorem prover for the relational calculus. 1 MSPASS mspass [17] is an enhancement of the first-order theorem prover spass with a translator of modal formulae, formulae of description logics, and formulae of the relational calculus. spass [19, 20] is one of the fastest and most sophisticated theorem provers for first-order logic with equality, and it's performance compares well with special purpose theorem provers for modal logics, description logics and first-order logic [7, 11, 18]. The input language of spass was extended to accept as input also modal, relational and description logic formulae. Modal formulae and description logic formulae are built from a vocabulary of propositional symbols of two disjoint types, namely, propositional (Boolean or concept) and relational (role). The repertoire of logical constructs incl...

• Type: Conference
• Year: 2000
• Where: TABLEAUX
• Authors: Ullrich Hustadt, Renate A. Schmidt
• Keywords: Artificial Intelligence, Description Logics, First-order Theorem Prover, TABLEAUX 2000, Theorem Provers