2026-07-072026-07-07http://salesiana.dossiersoluciones.com/handle/123456789/173529These notes provide a quick introduction to the Coq system and show how it can be used to define logical concepts and functions and reason about them. It is designed as a tutorial, so that readers can quickly start their own experiments, learning only a few of the capabilities of the system. A much more comprehensive study is provided in [1], which also provides an extensive collection of exercises to train on.Logic in Computer Sciencetext