Satoulouse: The computational power of propositional logic shown to beginners

Abstract

We present a tool (Satoulouse) that can help teachers, particularly in computer science, to convince undergraduate students that logic may be powerful. It is to be used very early in a logic course, in order to enhance students' motivation to learn propositional logic. Satoulouse simply consists of a friendly interface that offers several syntactic facilities and which is connected with a sufficiently powerful SAT-prover (namely SAT4J) allowing to automatically solve big instances of difficult problems (such as time-tables or Sudokus). © 2011 Springer-Verlag.