On the complexity of model checking and inference in minimal models extended abstract

Lefteris M. Kirousis, Phokion G. Kolaitis

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Every logical formalism gives rise to two fundamental algorithmic problems: model checking and inference. In propositional logic, the model checking problem is polynomial-time solvable, while the inference problem is coNP-complete. In propositional circumscription, however, these problems have higher computational complexity, namely the model checking problem is coNP-complete, while the inference problem is πP/2 -complete. In this paper, we survey recent results on the computational complexity of restricted cases of these problems in the context of Schaefer's framework of generalized satisfiability problems. These results establish dichotomies in the complexity of the model checking problem and the inference problem for propositional circumscription. Specifically, in each restricted case the model checking problem for propositional circumscription either is coNP-complete or is polynomial-time solvable. Furthermore, in each restricted case the inference problem for propositional circumscription either is πP/2 -complete or is in coNP. These dichotomy theorems yield a complete classification of the "hard" and the "easier" cases of the model checking problem and the inference problem for propositional circumscription. Moreover, they provide efficiently checkable criteria that tell apart the "hard" cases from the "easier" ones.

Original languageEnglish (US)
Title of host publicationLogic Programming and Nonmonotonic Reasoning - 6th International Conference, LPNMR 2001, Proceedings
Pages42-53
Number of pages12
DOIs
StatePublished - 2001
Event6th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2001 - Vienna, Austria
Duration: Sep 17 2001Sep 19 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2173 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference6th International Conference on Logic Programming and Nonmonotonic Reasoning, LPNMR 2001
Country/TerritoryAustria
CityVienna
Period9/17/019/19/01

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'On the complexity of model checking and inference in minimal models extended abstract'. Together they form a unique fingerprint.

Cite this