Satoulouse: The Computational Power of Propositional Logic Shown to Beginners

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).
 

Online Copy

Conference version: PDF

BibTeX Entry

@inproceedings{gasquet11:_satoul,
  author    = {Olivier Gasquet and
               Fran\c{c}ois Schwarzentruber and
               Martin Strecker},
  title     = {Satoulouse: The Computational Power of Propositional Logic
               Shown to Beginners},
  booktitle = {Tools for Teaching Logic - Third International Congress,
               TICTTL 2011, Salamanca, Spain, June 1-4, 2011. Proceedings},
  year      = 2011,
  pages     = {77-84},
  doi       = {http://dx.doi.org/10.1007/978-3-642-21350-2_10},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = 6680
}