Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Logic 2014

  News | Dates | Grading | Content | Exercises | Exam | Slides | Literature | Software

We will play with some of these tools in both the lectures and the exercises.

SAT-Solvers:

  • limboole. A SAT-solver developed by Armin Biere and colleagues at the University of Linz. (Explanation and information: [PDF])
  • limboole.tar.gz. Modified sources of limboole for Linux, including a build script and the dependencies.
BDD-tools:
  • DDcal und CUDD. BDD-calculator and API by Fabio Somenzi from the University of Colorado at Boulder.
  • BDD-Applet. Browser-Applet of the University of Hamburg.
Tarski's World
  • Java-Applet. Nice tool to get a grasp of the syntax and semantics of predicate logic, University of Plattsburgh.
Theorem provers for predicate logic
  • otter. A theorem prover for predicate logic based on resolution. Not very efficient anymore. University of New Mexico.
  • SPASS. An efficient theorem prover for predicate logic developed at the Max-Planck-Institute for Computer Science in Saarbrücken by Christoph Weidenbach and colleagues.
  • Vampire. Another efficient theorem prover developed at the University of Manchester by Andrei Voronkov and colleagues.
Hilbert Calculus
  • Java-Applet to construct derivations in Hilbert calculus, University of Wien.