Logic 2011

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.