Tableaux verification tool

Abstract

Mientras la lógica juega un papel muy importante en varias áreas de la ciencia informática, la mayoría del software educativo desarrollado para la enseñanza lógica ignora su aplicación en una parte más amplia del dominio de la enseñanza de la ciencia informática. En este trabajo, describimos una novedosa metodología cimentada en una herramienta de enseñanza lógica. Dicha enseñanza lógica está basada en tableaux semánticos para presentar a los estudiantes una nueva aplicación de la lógica como técnica de prueba formal en otros ámbitos de la ciencia informática, tales como la verificación formal y la depuración declarativa de programas imperativos, las cuales representan la base de un buen desarrollo del software. [ABSTRACT] While logic plays an important role in several areas of Computer Science, most educational software developed for teaching logic ignores their application in a more large portion of the Computer Science education domain. In this work, we describe an innovative methodology based on a logic teaching tool on semantic tableaux to prepare students for using as a formal proof technique in other topics of Computer Science, such as the formal verification and the declarative debugging of imperative programs, which are at the basis of a good development of software.