the concept of decide-efficiency for such analysis. We outline below how standard concepts of proof complexity (Cook et al. 1979) can be adapted to the setting of transition systems.

Let A be an infinite set of atoms. We define a node over A to be a symbol *FailState*, or a finite sequence of literals over A with annotations. For a propositional formalism F over A , a proof procedure PF consists of graphs GT , where T ranges over all theories in F,
such that for every theory T (i) GT is composed of nodes over A and (ii) T is unsatisfiable if and only if there is a path p in GT from the empty (start) node to the *FailState* node. We call each such path p a proof. We say that a proof system S is based on a proof procedure PF if (i) S ⊆ F ×R, where R denotes the set of all finite sequences of nodes over A , and
(ii) S(T,p) holds if and only if p is a proof in the graph GT in PF . Predicate S is indeed a proof system in the sense of Cook (1979) because (i) S is polynomial-time computable, and (ii) T is unsatisfiable if and only if there exists a proof p such that S(T,p) holds.

In this sense, each of the graphs (transition systems) we introduced in this paper can be regarded as a proof procedure for SM(ASP) (for those involving the rule *Learn*, under additional assumptions to ensure the rule can be efficiently implemented). Thus, transition systems determine proof systems. Consequently, they can be compared, as well as solvers that they capture, in terms of the complexity of the corresponding proof systems.

## 8 Conclusions

In the paper, we proposed a formalism SM(ASP) that can be regarded as a common generalization of (clausal) propositional logic, ASP, and the logic PC(ID). The formalism offers an elegant satisfiability modulo theories perspective on the latter two. We present several characterizations of these formalisms in terms of SM(ASP) theories that differ in the explicitly identified "satisfiability" component. Next, we proposed transition systems for SM(ASP) to provide abstract models of SM(ASP) model generators. The transition systems offer a clear and uniform framework for describing model generation algorithms in SM(ASP). As SM(ASP) subsumes several propositional formalisms, such a uniform approach provides a general proof of correctness and termination that applies to a broad class of model generators designed for these formalisms. It also allows us to describe in precise mathematical terms relations between algorithms designed for reasoning with different logics such as propositional logic, logic programming under answer-set semantics and the logic PC(ID), the latter two studied in detail in the paper. For instance, our results imply that at an abstract level of transition systems, CLASP and MINISAT(ID) are essentially identical. Finally, we note that this work gives the first description of CLASP in the abstract framework rather than in pseudocode. Such high level view on state-of-the-art solvers in different, yet, related propositional formalisms will further their understanding, and help port advances in solver technology from one area to another.

## Acknowledgments

We are grateful to Marc Denecker and Vladimir Lifschitz for useful discussions. We are equally grateful to the reviewers who helped eliminate minor technical problems and improve the presentation. Yuliya Lierler was supported by a CRA/NSF 2010 Computing Innovation Fellowship. Miroslaw Truszczynski was supported by the NSF grant IIS-0913459.