Prover9 Exercises

A wide variety of automated theorem provers have been developed since their origin in the 1960's. However, this kind of program is difficult to implement and often difficult to use. Thus, very few theorem provers have gained many users beyond the researchers who developed them. One of the more popular was Otter, which at one time was arguably the most powerful prover around, and was able to verify a number of theorems that mathematicians had hypothesised but not been able to prove. Prover9 is an improved version of the original Otter. Although it is not usually regarded as one of the most powerful, it does have the advantage of being relatively simple compared to most of the more modern provers.

Contents

• Setting Up Prover9
• Prover9's Proof Method
• Simple Examples
• A More Complex Example
• Some Points to Note

Exercises

• Propositional logic problem exercises -- you should do all of these.
• Introductory first-order logic problem exercises -- you should do all of these.
• More challenging logic problems -- do as many as you can to develop your skills of logical analysis and representation.

Running Prover9

Installing Prover9 on your own Machine (Windows or Linux)

Probably the most convenient way to use Prover9 is by installing it on your machine.
Documentation and downloads can be found on the Prover9 home page at:
http://www.cs.unm.edu/~mccune/prover9/

Running Prover9 via Colab

• Link to Prover9 Colab notebook interface

Videos

• Getting Started With Prover9
• Doing the Prover9 exercises and submitting to Gradescope

Automatic Feedback using Gradescope

Prover9's Proof Method

The primary mode of inference used by Prover9 is resolution. It repeatedly makes resolution inferences with the aim of detecting inconsistency by deriving a contradiction. As discussed in the lecture notes, resolution provides a complete proof procedure for detecting inconsistency of formulae that are expressed in clausal form.

Prover9 will first do some preprocessing on the input file to convert it into the form it uses for inferencing. First it negates the formula given as a goal¹. It then translates all formulae into clausal form. (In some cases it will do some further pre-processing, but you do not need to worry about this.) Then it will compute inferences and by default write these standard output. Unless the input is very simple it will often generate a large number of inferences. If it detects an inconsistency it will stop and print out a proof consisting of the sequence of resolution rules that generated the inconsistency. It will also print out various statistics associated with the proof.

1. Actually Prover9 allows multiple goal formulae, but it is best to use just one, since the semantics of multiple goals is potentially confusing.

Simple Examples

Here is an example of a very simple Prover9 file:

formulas(assumptions).
p & s.		% '&' symbol is for conjunction, 'and'
p -> q. 	% '->' symbol is for implication, 'implies'
q -> -r.	% '-' symbol is for negation, 'not'
end_of_list.

formulas(goals).
-r | t.		% '|' symbol is for disjunction 'or'
end_of_list.

Note: If you are using the GUI version you don't need the lines declaring the formula list and goal list. You just enter the formulae into the appropriate boxes in the interface.

Here is a slightly more complex example using quantifiers (borrowed from the intro- ductory material on the Prover9 web site):

formulas(assumptions).
all x all y (subset(x,y) <-> (all z (member(z,x) -> member(z,y)))).
end_of_list.

formulas(goals).
all x all y all z (subset(x,y) & subset(y,z) -> subset(x,z)).
end_of_list.

A More Complex Example

Here is a much more complex example devised by Len Schubert. It was originally known as "The Steamroller" because at the time (in the 80s) it was very difficult for automated theorem provers to solve (it would flatten them). However, it presents no problem for a modern theorem prover such as Prover9 running on a modern computer.

% Schubert's "Steamroller" Problem
% 
% Wolves, foxes, birds, caterpillars, and snails are animals,
% and there are some of each of them.
%
% Also there are some grains, and grains are plants.
%
% Every animal either likes to eat all plants or all animals much
% smaller than itself that like to eat some plants.
%
% Caterpillars and snails are much smaller than birds, which are much
% smaller than foxes, which are in turn much smaller than wolves.
%
% Wolves do not like to eat foxes or grains, while birds like to eat
% caterpillars but not snails.
%
% Caterpillars and snails like to eat some plants.

% Prove there is an animal that likes to eat a grain-eating animal.
% (where a grain eating animal is one that eats all grains)

formulas(assumptions).
all x (Wolf(x) -> animal(x)).
all x (Fox(x) -> animal(x)).
all x (Bird(x) -> animal(x)).
all x (Caterpillar(x) -> animal(x)).
all x (Snail(x) -> animal(x)).
all x (Grain(x) -> plant(x)).

exists x Wolf(x).
exists x Fox(x).
exists x Bird(x).
exists x Caterpillar(x).
exists x Snail(x).
exists x Grain(x).


% All animals either eat all plants or eat all smaller animals that eat some plants.

all x ( animal(x) -> (  (all y ( plant(y) -> eats(x,y)))
                        |
	 		(all z ( animal(z) & Smaller(z,x) &
				 (exists u (plant(u) & eats(z,u)))
				 ->
				 eats(x,z)
                               )
                        )
                     )
      ).
%% Notice the use of indentation. This is not required, but is very
%% helpful in preventing mistakes in complex formulae.


all x all y (Caterpillar(x) & Bird(y) -> Smaller(x,y)).
all x all y (Snail(x) & Bird(y) -> Smaller(x,y)).
all x all y (Bird(x) & Fox(y) -> Smaller(x,y)).
all x all y (Fox(x) & Wolf(y) -> Smaller(x,y)).
all x all y (Bird(x) & Caterpillar(y) -> eats(x,y)).

all x (Caterpillar(x) -> (exists y (plant(y) & eats(x,y)))).
all x (Snail(x) -> (exists y (plant(y) & eats(x,y)))).

all x all y (Wolf(x) & Fox(y) -> -eats(x,y)).
all x all y (Wolf(x) & Grain(y) -> -eats(x,y)).
all x all y (Bird(x) & Snail(y) -> -eats(x,y)).

end_of_list.

formulas(goals).
% "there is an animal that eats {an animal that eats all grains}".
exists x exists y (animal(x) & animal(y) & eats(x,y) &
					(all z (Grain(z) -> eats(y,z)))).
end_of_list.

Some points to note