We present a general logic of explicit knowledge represented as finite sets of logical formulae which can evolve by nondeterministic reasoning and communication. It is partly based on Alternating-time Temporal Logic, which allows the expression of properties of cooperation. Properties of an agent’s reasoning mechanism such as “the agent knows modus ponens (MP)” can be expressed. Instead of a common closure condition such as “if the agent knows both p and p → q, he must also know q”, the following holds: “if the agent knows p, p → q and MP, he has a strategy to get to know q in the future”. Categories and Subject Descriptors I.2.4 [Artificial Intelligence]: Knowledge Representation Formalisms and Methods—Representations (procedural and rule-based), Temporal logic; I.2.11 [Artificial Intelligence]: Distributed Artificial Intelligence—Intelligent agents, Multiagent systems; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving—Nonmon. reasoning and b...