Among the goals of building a logic system we have the problem of modelling and verifying the validity of formulae. To find a proof in a logic system that extend conservatively Classical Propositonal Logic may request hard work. Automatic theorem provers deal with this problem, but to build them it is necessary to deal with advanced programming aspects. This work presents an extensible automatic theorem prover for Classical Propositional Logic based in clausal resolution. Any deductive system that extends this logic may be implemented only dealing with what is not present in this logic.