Solving the $100 modal logic challenge

Florian Rabe, Petr Pudlák, Geoff Sutcliffe, Weina Shen

Research output: Contribution to journalArticlepeer-review

4 Scopus citations

Abstract

We present the theoretical foundation, design, and implementation, of a system that automatically determines the subset relation between two given axiomatizations of propositional modal logics. This is an open problem for automated theorem proving. Our system solves all but six out of 121 instances formed from 11 common axiomatizations of seven modal logics. Thus, although the problem is undecidable in general, our approach is empirically successful in practically relevant situations.

Original languageEnglish (US)
Pages (from-to)113-130
Number of pages18
JournalJournal of Applied Logic
Volume7
Issue number1
DOIs
StatePublished - Mar 1 2009

Keywords

  • $100 challenge
  • Modal logic
  • Subset relationship

ASJC Scopus subject areas

  • Logic
  • Applied Mathematics

Fingerprint Dive into the research topics of 'Solving the $100 modal logic challenge'. Together they form a unique fingerprint.

Cite this