Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic

Abstract

There has been a great deal of work on characterizing the complexity of the satisfiability and validity problem for modal logics. In particular, Ladner showed that the satisfiability problem for all logics between K and S4 is PSPACE-hard, while for S5 it is NP-complete. We show that it is negative introspection, the axiom Kp ) KKp, that causes the gap: if we add this axiom to any modal logic between K and S4, then the satisfiability problem becomes NP-complete. Indeed, the satisfiability problem is NP-complete for any modal logic that includes the negative introspection axiom.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Feb 01, 2007
Accession Number
AD1020505

Entities

People

  • Joseph Halpern
  • Leandro C. Rego

Organizations

  • Cornell University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Algorithms
  • Artificial Intelligence
  • Computer Science
  • Computers
  • Consistency
  • Construction
  • Electronic Mail
  • Hardness
  • Literature
  • Notation
  • Observation
  • Semantics
  • Standards
  • Theoretical Computer Science
  • Universities

Readers

  • Computer Engineering
  • Microwave Engineering.
  • Military History of the United States in the 20th Century.