Lefteris Kirousis, Phokion G. Kolaitis

A dichotomy theorem for a class of decision problems is

a result asserting that certain problems in the class

are solvable in polynomial time, while the rest are NP-complete.

The first remarkable such dichotomy theorem was proved by

T.J. Schaefer in 1978. It concerns the ...
more >>>

Olaf Beyersdorff, Leroy Chew

Circumscription is one of the main formalisms for non-monotonic reasoning. It uses reasoning with minimal models, the key idea being that minimal models have as few exceptions as possible. In this contribution we provide the first comprehensive proof-complexity analysis of different proof systems for propositional circumscription. In particular, we investigate ... more >>>

Olaf Beyersdorff, Leroy Chew

In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (J. Autom. Reasoning, 1992). Our main result shows that OTAB-proofs can be efficiently translated into MLK-proofs, i.e., MLK p-simulates OTAB. The simulation is technically very involved ... more >>>