A learning methodology based on semantic tableaux for software engineering education

While Computational Logic plays an important role in several areas of Software Engineering (SE), most of the educational technology developed for teaching logic ignores their application in a larger portion of the SE education domain. In this paper we describe an innovative methodology based on a prototype logic teaching tool on semantic tableaux to prepare and train the students to use logic as a formal proof technique in other topics of SE, such as the formal verification of algorithms and the declarative debugging of imperative programs, which are foundations of good development of software.