Just found two fantastic programs and a GUI for exploring first-order classical models and also automated proof, Prover9 and Mace4.Β There are many other theorem provers and model checkers out there.Β This one is special as it comes as a self-contained and easy to use package for Windows and Macs.

There are many impressive examples built in which you can play with.Β To start easy, I gave it a syllogism:

* all B are A
no B are C*

with existential presupposition, which is expressed:

exists x a(x). exists x b(x). exists x c(x). all x (b(x) -> a(x)). all x (b(x) -> -c(x)).

and asked it to find a model. Out popped a model with two individuals, named 0 and 1:

a(0). - a(1). b(0). - b(1). - c(0). c(1).

So individual 0 is an *A*, a *B*, but not a *C*. Individual 1 is not an *A*, nor a *B*, but is a *C*.

Then I requested a counterexample to the conclusion *no C are A*:

a(0). a(1). b(0). - b(1). - c(0). c(1).

The premises are true in this model, but the conclusion is false.

Finally, does the conclusion *some A are not C* follow from the premises?

2 (exists x b(x)) [assumption]. 4 (all x (b(x) -> a(x))) [assumption]. 5 (all x (b(x) -> -c(x))) [assumption]. 6 (exists x (a(x) & -c(x))) [goal]. 7 -a(x) | c(x). [deny(6)]. 9 -b(x) | a(x). [clausify(4)]. 10 -b(x) | -c(x). [clausify(5)]. 11 b(c2). [clausify(2)]. 12 c(x) | -b(x). [resolve(7,a,9,b)]. 13 -c(c2). [resolve(10,a,11,a)]. 16 c(c2). [resolve(12,b,11,a)]. 17 $F. [resolve(16,a,13,a)].

Indeed it does. Unfortunately the proofs aren’t very pretty as everything is rewritten in normal forms.Β One thing I want to play with is how non-classical logics may be embedded in this system.