MSPASS: Modal reasoning by translation and first-order resolution

Ullrich Hustadt, R.A. Schmidt

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

Abstract

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
Pages67-71
Number of pages5
ISBN (Electronic)9783540450085
ISBN (Print)9783540676973
DOIs
Publication statusPublished - 21 Jun 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1847

Keywords

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

Fingerprint

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

Cite this