The COCOLOG (Conditional Observer and Controller Logic) system is a partially ordered family of first-order logical theories expressed in the typed first-order languages {L(k);k greater than or equal to 0} describing the controlled evolution of the state of a given partially observed finite machine M. The initial theory of the system, denoted Th-0, gives the theory of M with no data being given on the initial state. Later theories, {Th(o(1)(k)); k greater than or equal to 1}, depend upon the (partially ordered lists of) observed input-output trajectories {o(1)(k);k greater than or equal to 1}, where new data are accepted in the form of the new axioms AXM(obs)(L(k)), k greater than or equal to 1. A feedback control input U(k) is determined by the solution of a collection of control problems posed in the form of a set of conditional control rules CCR(L(k)), such a set being paired with the theory Th(o(1)(k)) for each k greater than or equal to 1. In this paper, we introduce a restricted version of COCOLOG, called a system of Markovian fragments of COCOLOG, in which a smaller amount of information is communicated from one theory to the next. Such fragment theories are associated with a restricted set of candidate control problems, denoted CCR(L(k)(m)), k greater than or equal to 1. It is shown that a Markovian fragment theory MTh(o(1)(k)) contains a large subset of Th(o(1)(k)), which includes, in particular, the stare estimation theorems of the corresponding full COCOLOG system and, for the set of control rules CCR(L(k)(m)), has what is termed the same control reasoning power. Next, it is shown that proofs of theorems in the fragment systems are necessarily shorter than their proofs in the full COCOLOG systems. Finally some computer-generated examples are given, illustrating this increased theorem-proving efficiency.