## Abstract

We establish the complexity of decision problems associated with the nonmonotonic modal logic S4. We prove that the problem of existence of an S4-expansion for a given set A of premises is Σ_{2} ^{P}-complete. Similarly, we show that for a given formula ϕ and a set A of premises, it is Σ_{2} ^{P}-complete to decide whether ϕ belongs to at least one S4-expansion for A, and it is Π_{2} ^{P}-complete to decide whether ϕ belongs to all S4-expansions for A. An interesting aspect of these results is that reasoning (testing satisfiability and provability) in the monotonic modal logic S4 is PSPACE-complete. To the best of our knowledge, the nonmonotonic logic S4 is the first example of a nonmonotoific formalism which is computationally easier than the monotonic logic that underlies it (assuming PSPACE does not collapse to Σ^{2} _{P}).

Original language | English |
---|---|

Title of host publication | Computational Logic and Proof Theory - 3rd Kurt Godel Colloquium, KGC 1993, Proceedings |

Editors | Georg Gottlob, Alexander Leitsch, Daniele Mundici |

Pages | 313-324 |

Number of pages | 12 |

DOIs | |

State | Published - 1993 |

Event | 3rd Kurt Godel Colloquium on Computational Logic and Proof Theory, KGC 1993 - Brno, Czech Republic Duration: Aug 24 1993 → Aug 27 1993 |

### Publication series

Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|

Volume | 713 LNCS |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 3rd Kurt Godel Colloquium on Computational Logic and Proof Theory, KGC 1993 |
---|---|

Country/Territory | Czech Republic |

City | Brno |

Period | 8/24/93 → 8/27/93 |

### Bibliographical note

Publisher Copyright:© Springer-Verlag Berlin Heidelberg 1993.

## ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science (all)