En este trabajo se desarrolla una formalización de sistemas de razonamiento proposicionales y se verifican automáticamente sus principales propiedades en el sistema de demostración automática ACL2.