Prover9-Mace4 v05

1. Introduction

This is a brief introduction. Better help will be available
in the next release.

Prover9-Mace4 is a front end to the programs Prover9 (which
searches for proofs) and Mace4 (which searches for finite
models and counterexamples).  Prover9 and Mace4 have been
around for a few years, and they are ordinarily run on
a command line (without a GUI).  This introduction is
mainly about the GUI.  For detailed information on Prover9
and Mace4, see http://www.cs.unm.edu/~mccune/prover9.

The GUI is intended primarily for new users and casual
users.  Power users might not be very interested, but
they might find the displays of the options useful.

Recommendations for new users who know first-order or
equational logic:

  (1) Look at some of the examples in "File -> Sample Inputs".
      This will give an idea of the formula syntax.

  (2) Experiment by modifying the sample inputs, both formulas
      and options.  Note:

       (a) each formula ends with a period,
       (b) variables start with (lower case) u--z,
       (c) when in doubt, include parentheses.

  (3) Start from scratch, enter some assumptions and goals,
      and try to prove or disprove some things.

Although there are many options, much can be accomplished
with just Assumptions and Goals.

2. The Main Window

The main window is divided into the Setup panel on the
left, and the Run panel on the right.

2.1. The Setup Panel

The Setup panel is for specifying the input to Prover9 and/or
Mace4.  The "Language Options" and "Formulas" tabs are
used for both Prover9 and Mace4.  The "Additional Input"
tab is for some esoteric kinds of input, and it can be ignored
by most users.

2.1.1. Formulas

A few basic points about formulas (see the HTML manual for details).

  + Do not include the Prover9/Mace4 constructs
    "formulas(assumptions)" or "end_of_list".
  + Each formula ends with a period.
  + Variables start with (lower case) u--z.
  + The basic logic connectives are:  - | & -> <-> all exists.
  + Universal quantifiers at the outermost level can be omitted.
  + When in doubt, include parentheses.  The programs usually
    output formulas with the minimum number of parentheses,
    so you can look in the output to see how you could have
    written the formulas.

Goals

Prover9 always proves by contradiction, and Mace4 looks
for counterexamples by searching for a model of the negation
of the conjecture.  Each program puts the negation of the
goals together with the assumptions and then searches.
If there are no goals, Prover9 simply looks for a contradiction
among the assumptions, and Mace4 looks for a model of the
assumptions.  It's also acceptable to have no assumptions,
with the entire statement of the conjecture as a goal.

Multiple Goals  

If there are multiple goals, Prover9 assumes you want a
separate proof of each goal, and it will try to prove
all of them.

Mace4 searches for counterexamples to the goals.  If
there are multiple goals, Mace4 looks for structures
that falsify all of the goals.

From the HTML manual: "If there is more than one formula in
the goals list, each must be a positive universal
conjunctive formula; that is, a formula constructed from
atomic formulas, universal quantification, and conjunction
only."

From a logical point of view, multiple goals are a
disjunction.  Consider two goals "P. Q.".  If Prover9
proves either of them, it outputs a proof.  Mace4
looks for a counterexample by searching for a model
of the negation of the disjunction; that is, a model
in which both are false.

If there is any doubt about the meaning of multiple goals,
the user can combine them into a single goal with the
conjunction or disjunction operations.

2.1.2. Options Panels

The options panels contain most of the options accepted
by the programs Prover9 and Mace4, with the same names.
The GUI's default values are the same as the programs"
default values.  When an option has a non-default value,
its name is shown in red.

There can be more than one widget (button or entry box)
associated with an option.  For example, each of the Prover9
"Basic Options" also appears somewhere in "All Options".
When one occurrence is changed, all other occurrences are
updated.

Many of the integer-valued options specify limits and have
a range [-1, ..., some-big-number].  In these cases, -1 means
"no limit".

Prover9 and Mace4 have a notion of "dependent option":
changing some of the options causes others to be changed
automatically.  For example, when Prover9 receives
"set(breadth_first).", it automatically changes the parameters
"age_part", "weight_part", "true_part", and "false_part".
The GUI is aware of the dependent options.  Options
with dependencies are shown in blue, and when such an option
is changed, the dependent options are changed automatically.
Because the GUI handles dependent options, it tells
Prover9 and Mace4 to ignore option dependencies.

2.1.2.  Additional Input Panels

These can be used for Prover9 input that cannot yet be
specified with the widgets, including:

  + weighting rules,
  + KBO weights,
  + function_order and relation_order,
  + actions,
  + interpretations for semantic guidance, and
  + lists of hints (you must include "formulas(hints)." and
    "end_of_list.").

2.2. The Run Panel

The "Show Current Input" button at the top of the Run panel
displays the data in the Setup panel as a text file.  This
is the input that will be given to Prover9 or Mace4 when one
of the "Start" buttons is pressed.

If you want to try for both a proof and a counterexample,
the two programs can be run concurrently (and they should
take advantage of a multiple-core processor if you have one).

The "Info" button shows a few statistics about the search.
It can be pressed during a search or after a search has
finished.

When the program stops, the "Show-Save" button will be enabled.
he "Show-Save" button gives you

  (1) the input that was given to the program (not the
      "Current Input", which might have changed since
      the program was started),
  (2) the program's full output, and
  (3) if successful, proof(s) or counterexample(s).

These data will be available until the another search is started.

2.3. The Menu Bar

2.3.1.  The File Menu

"Clear Entire Setup Menu" resets everything to the initial
state: language options, formulas, options, and additional
input.

The "Open" and "Save" selections work as in many other
applications.  These apply to Prover9/Mace4 input files.
(The text that is "Save"d is the same as the text displayed
by the "Show Current Input" button in the Run panel.)
The "Append To Input" selection is similar to the "Open"
selection, except that existing state (formulas, options)
is not cleared first.

"Open Input File ..." should work not only on previously
"Save"d files, but also on most other Prover9 or Mace4 input
files.  Comments in "Open"ed files are not handled well:
most comments that are not inside of formula lists appear
in "Additional Input".

3. Proofs and Models/Counterexamples

When a proof or model/counterexample is found, it is shown
in a separate window.  Several additional operations can
be applied to the proofs or models/counterexamples.

3.1.  Proofs

Proofs found by Prover9 are usually hard to understand
and longer then necessary.  (We are conducting research on
several methods to humanize and simplify proofs.)

For now, there is a button "Reformat...", in the Proof window,
which allows the user to transform the proof in several simple
ways.  See the HTML manual, page "Prooftrans".

3.2. Models/Counterexamples

Models/Counterexamples found by Mace4 are given as function
and relation tables.  The underlying set for domain_size=n
is always {0,...,n-1}.

There is a button "Reformat...", in the Model/Counterexample window,
which allows the user to transform the model in several simple
ways.  See the HTML manual, page "Interpformat".

3.2.1.  Isofilter.

If the user asks for more than one model (option max_models),
Mace4 will keep searching until it finds that number of models
or until it reaches some other limit.  When Mace4 finds multiple
models, many are likely to be isomorphic to others.  A separate
program "Isofilter" can be used to remove isomorphic models.

Isofilter has several options.  One can specify the operations
that are checked for isomorphism, and one can specify the
operations that are output.  (For example, if one of the operations
is a Skolem function from an existentially quantified variable,
one might wish to omit it for checking and for output.)

One can select the the algorithm Isofilter will use:
"Occurrence Profiles" (the default) or "Canonical Forms".
They should produce the same results, but the relative
performance depends on the application.