The Logic Workbench (LWB) is a set of tools for playing with logic. It is written in Clojure and comprises tools for propositional logic, predicate (first order) logic, linear temporal logic, and combinatory logic.
LWB has a component for natural deduction in propositional, predicate and linear temporal logic, and furthermore a component for doing interactive combinatory logic.
LWB is a playground for logic and programming logic in Clojure.
There are a lot of examples in the Logic WorkBench!
More about LWB: Documentation ⇗ and Source Code ⇗ and Library on clojars ⇗.
It's quite convenient to use the logic workbench as a plugin in atom, see lwb-ui ⇗.