Implements the axiomatic translation principle introduced in Schmidt and Hustadt (2003) for a range of modal logics. In conjunction with the translator FLOTTER and dfg2tptp (both are part of the MSPASS distribution) it can be used with any first-order logic theorem prover recognising DFG or TPTP input. This combination of tools effectively renders the most powerful and flexible fully automated theorem prover for modal logic and first-order logic available to date.


A link to a web-interface will appear here soon.
Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 07 Oct 04
Copyright © 2003-2004 Renate A. Schmidt, School of Computer Science, Man Univ,