Home

lwb Logic WorkBench

The Logic WorkBench (lwb) comprises tools for propositional, predicate, and linear temporal logic. It is written in Clojure.

lwb is a playground, it's work in progress.

Getting started

Using lwb in lwb-gui, a simple GUI for lwb

1. Download lwb-gui from github
2. Follow the documentation on github to start the GUI
3. Choose Session > New... in the menu and choose the part of lwb you like to use

You are now ready to explore all the functions for propositional logic, predicate logic, linear temporal logic, and combinatory logic.

The key combination control-shift-t evaluates the expression under the cursor in the REPL.

lwb in a Clojure development environment

1. Clone lwb from esb-lwb and create a project in your favorite setting for Clojure development
2. Put the libraires kodkod and ltl2buchi into your local maven repository, see lwb/Dependencies

You are now ready to play with the Logic Workbench

Dependencies to other programs

• Some functions of lwb use TeX, so using them you should have a running TeX distribution on your machine. The TeX code that is generated in lwb uses the following packages of TeX: standalone.cls, amssymb, MnSymbol, babel, tikz, tikz-qtree, logicproof.
• Some functions use graphviz together with dot2tex.

Propositional Logic

More about propositional logic

Binary Decision Diagrams

Examples

Predicate Logic

More about predicate logic

Examples

Linear Temporal Logic

More about ltl

Visualizing formulas

Visualisung formulas with tikz

Natural Deduction

More about natural deduction

Examples of natural deduction in propositional logic

Examples of natural deduction in predicate logic

Examples of natural deduction in linear temporal logic

Combinatory Logic

More about combinatory logic

Interactive Combinatory Logic

Examples

License

The use and distribution terms for this software are covered by the Eclipse Public License 1.0, (https://opensource.org/licenses/eclipse-1.0.php). By using this software in any fashion, you are agreeing to be bound by the terms of this license. You must not remove this notice, or any other, from this software.

Collaborators

Markus Bader, Mathias Gutenbrunner, Marcel Hoppe, Nicola Justus, Daniel Kirsten, Jens Lehnhäuser, Juan Markowich, Marco Stephan, Tobias Völzel