# Prover9 and Mace4

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.