We discuss equilibrium logic, first presented in Pearce (1997), as a system of nonmonotonic reasoning based on the nonclassical logic N 5 of here-and-there with strong negation. Equilibrium logic is a conservative extension of answer set inference, not only for extended, disjunctive logic programs, but also for significant extensions such as the programs with nested expressions described by Lifschitz, Tang and Turner (forthcoming). It provides a theoretical basis for extending the paradigm of answer set programming beyond current systems such as smodels and dlv. The paper provides proof systems for N 5 and for model-checking in equilibrium logic. The reduction of the latter problem to an unsatisfiability problem of classical logic yields complexity results for the various decision problems concerning equilibrium entailment. The reduction also yields a basis for the practical implementation of an automated reasoning tool.