  Model checking and automated theorem proving are two pillars of formal
methods. This paper investigates model checking from an automated theorem
proving perspective, aiming at combining the expressiveness of automated
theorem proving and the complete automaticity of model checking. The focus of
this paper is on the verification of temporal logic properties of Kripke
models. The main contributions of this paper are: first the definition of an
extended computation tree logic that allows polyadic predicate symbols, then a
proof system for this logic, taking Kripke models as parameters, then, the
design of a proof-search algorithm for this calculus and a new automated
theorem prover to implement it. The verification process is completely
automatic, and produces either a counterexample when the property does not
hold, or a certificate when it does. The experimental result compares well to
existing state-of-the-art tools on some benchmarks, including an application to
air traffic control and the design choices that lead to this efficiency are
discussed.
