What online tools are available, where one can enter a formula of (first order) propositional or predicate logic, and have it check whether it is valid classically, intuitionistically, or even minimally or in some other logical framework?
I found the following things that got close:
- In the past I have successfully used LWB (The Logics Workbench) at http://www.lwb.unibe.ch/shell/. However, it currently (Feb 2, 2015) fails with HTTP error 500 problems, where the server cannot connect to something on localhost port 11111.
- The Stanford Validity Checker (http://verify.stanford.edu/SVC/) has been available at least up until May 2014 (archive.org link) but it now (Feb 2, 2015) gives an HTTP 403 Forbidden error.
- Only classical logic is supported by somerby.net/mack/logic.
- Also only classical logic is supported by the ProB Logic Calculator.
The last two I found through Leslie Lamport's Logic Calculators page, which ominously proclaims: "Logic calculators are disappearing faster than I learn about them."
As background, among other things I'd like to use such a tool to help answer questions on this site like this and this.
Update. Pointers to easily available and free Linux or Windows based tools are also welcome, but the main goal of this question is for online tools.
Best Answer
A Linear Logic Prover supports propositional and unary predicate logic in three different frameworks; one is classical and the other two are intuitionistic. It seems to work ok. If you enter the statement from "Intuitionistic proof of ∀x(P(x)∨Q(x))→(∀xP(x)∨∃xQ(x))", which is "
all(X,p(X)+q(X)) -> (all(X,p(X)) + exists(X,q(X)))" in llprover's language, it finds a proof for it in the classical framework, and fails to find a proof for it in the intuitionistic framework.