MSPASS: Modal reasoning by translation and first-order resolution

Ullrich Hustadt, R.A. Schmidt

Research output: Chapter in Book/Report/Conference proceedingChapterpeer-review


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.
Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods
Subtitle of host publicationInternational Conference, TABLEAUX 2000 St Andrews, Scotland, UK, July 3-7, 2000 Proceedings
EditorsRoy Dyckhoff
Place of PublicationHeidelberg
PublisherSpringer Berlin
Number of pages5
ISBN (Electronic)9783540450085
ISBN (Print)9783540676973
Publication statusPublished - 21 Jun 2000

Publication series

NameLecture Notes in Computer Science


  • Modal Logic
  • Decision Procedure
  • Description Logic
  • Modal Formula
  • Translation Method


Dive into the research topics of 'MSPASS: Modal reasoning by translation and first-order resolution'. Together they form a unique fingerprint.

Cite this