Prover9-Mace4

Introduction

I wrote down some important features of Prover9-Mace4 software from its Manual page¹ in this post. I expect the post can be used for improvement of the related software.

Prover9

Errors

• The make command did not run successfully on my Windows, and I found that there is a syntax error in the Makefile of provers.src from Line 65 to 84. The flag -lm must be placed at the end of each command to run the make command as it is supposed to:

prover9: prover9.o $(OBJECTS)
        $(CC) $(CFLAGS) -o prover9 prover9.o $(OBJECTS) ../ladr/libladr.a -lm

fof-prover9: fof-prover9.o $(OBJECTS)
        $(CC) $(CFLAGS) -o fof-prover9 fof-prover9.o $(OBJECTS) ../ladr/libladr.a -lm

ladr_to_tptp: ladr_to_tptp.o $(OBJECTS)
        $(CC) $(CFLAGS) -o ladr_to_tptp ladr_to_tptp.o $(OBJECTS) ../ladr/libladr.a -lm

tptp_to_ladr: tptp_to_ladr.o $(OBJECTS)
        $(CC) $(CFLAGS) -o tptp_to_ladr tptp_to_ladr.o $(OBJECTS) ../ladr/libladr.a -lm

autosketches4: autosketches4.o $(OBJECTS)
        $(CC) $(CFLAGS) -o autosketches4 autosketches4.o $(OBJECTS) ../ladr/libladr.a -lm

newauto: newauto.o $(OBJECTS)
        $(CC) $(CFLAGS) -o newauto newauto.o $(OBJECTS) ../ladr/libladr.a -lm

newsax: newsax.o $(OBJECTS)
        $(CC) $(CFLAGS) -o newsax newsax.o $(OBJECTS) ../ladr/libladr.a -lm

• The GUI version of Prover9-Mace4 raises an error. So I am using the command-line version.

Lists of Objects

In this post, I am writing about only a part of Prover9-Mace4’s feature that seems most useful to me.

formulas(sos).           p(x).     end_of_list.   % the primary input list
formulas(assumptions).   p(x).     end_of_list.   % synonym for formulas(sos)
formulas(goals).         p(x).     end_of_list.   % some restrictions
formulas(hints).         p(x).     end_of_list.   % should be used more often

How to run Prover9 from Command-Line

prover9 -f input_file.in > output_file.out

You can also specify multiple input files where separated with a space.

Formulas

Meaning	Connective
negation	-
disjunction	|
conjunction	&
implication	->
backward implication	<-
equivalence	<->
universal quantification	all
existential quantification	exists

Example Input

formulas(assumptions).   % synonym for formulas(sos).
  man(x) -> mortal(x).   % open formula with free variable x
  man(george).
end_of_list.

formulas(goals).         % to be negated and placed in the sos list
  mortal(george).
end_of_list.

Then Prover9 will parse the formulas to start searching for a refutation:

formulas(sos).           
  -man(x) | mortal(x).
  man(george).
  -mortal(george).
end_of_list.

The generated proof by Prover9 from this input is as follows:

1 man(x) -> mortal(x) # label(non_clause).  [assumption].
2 mortal(george) # label(non_clause) # label(goal).  [goal].
3 man(george).  [assumption].
4 -man(x) | mortal(x).  [clausify(1)].
5 mortal(george).  [resolve(3,a,4,a)].
6 -mortal(george).  [deny(2)].
7 $F.  [resolve(5,a,6,a)].

Mace4

Mace 4 searches for finite structures satisfying first-order and equational statements. This can be used to find a counter example of a conjecture by inputting the negation of the conjecture.

Operations

Symbol	Meaning
+	Sum
*	Product
-	Negation (unary)
/	Integer Division
mod	Modulus
min	Minimum
max	Maximum
abs	Absolute Value
domain_size	Current Domain Size

Relations

Symbol	Meaning
=	Equal
<	Less than
<=	Less than or equal
>	Greater than
=>	Greater than or equal

Example Input

This examples illustrates the n-Queen puzzle problem:

set(arithmetic).

formulas(assumptions).

% n-Queens Puzzle
%
% In this representation, Q(i)=n means that Row i Column n has a queen.
% The constraint that no queens can be in the same row is always satisfied
% in this representation, because Q is a function; that is,
% Q(x) != Q(z) -> x != z  is always satisfied.

% Note that there is no binary "minus" operation, so we have to write x + -y.

x != z -> Q(x) != Q(z).   % No 2 queens in the same column.

x != z  ->  z + -x != Q(z) + -Q(x).  % No 2 queens in \ diagonal.

x != z  ->  z + -x != Q(x) + -Q(z).  % No 2 queens in / diagonal.

end_of_list.

The command that run the example would be:

mace4 -n8 -f queens.in > queens.out

where -n8 flag represents the board size of 8.

The model that Mace4 outputs is:

interpretation( 4, [number=1, seconds=0], [

        function(Q(_), [ 1, 3, 0, 2 ])
]).

Finding Multiple Model

Use the flag -m followed by the maximum number of model to generate (1 as default, -1 for unlimited).

The isofilter module provided by Mace4 can be used to remove isomorphic structures.

Related Software

Interpfilter

filter models with formulas

1. Prover9 Manual. November, 2009. https://www.cs.unm.edu/~mccune/mace4/manual/2009-11A/. ↩︎