Simplify(1)
NAME
Simplify -- attempt to prove first-order formulas.
SYNTAX
Simplify [-print] [-ax axfile] [-nosc] [-noprune] [-help] [-version] [file]
DESCRIPTION
Simplify accepts a sequence of first order formulas as input,
and attempts to prove each one. Simplify does not implement a
decision procedure for its inputs: it can sometimes fail to prove a
valid formula. But it is conservative in that it never claims that
an invalid formula is valid.
The PredSx
interface in the prover package specifies the syntax used to
specify the formulas; this syntax is based on S-expressions, with
one S-expression per formula. (I include this interface later in
this man page.) If the file argument is provided, S-expression
formulas are read one at a time from the file, and proved;
otherwise, Simplify enters a "read-prove-print" loop in which
the user enters formulas interactively. The input formula is not
normally echoed, but it is when the -print argument is given.
If Simplify can prove the formula, it prints valid. If it
cannot prove the formula, it normally prints a conjunction of
literals that it believes to satisfy the negation of the formula.
Computing this satisfying context takes some time, and sometimes one
may be interested only in whether the input was valid or not; the
-nosc options causes Simplify to simply output "valid" or
"invalid". The -noprune flag causes Simplify to skip the step
of "pruning" any satisfying context resulting from a failed proof;
instead, it prints the entire context.
The -version option prints out the version number of the
Simplify executable, and the -help option prints out a
usage message.
Simplify proves its formulas assuming some set of axioms.
The first step in a Simplify execution is loading the axioms.
You can customize the axiom set you use in two ways. The -ax flag
allows you to specify an alternate axiom set, and the the AXIOMDIR
environment variable allows you to specify where Simplify
should look for that axiom set. Simplify comes with a
collection of axiom sets included via the Modula-3 "bundle"
facility; currently, these consist of "def.ax" and "esc.ax".
(Simplify assumes axiom files use the ".ax" suffix.)
If the -ax flag is not used, Simplify looks for "def.ax";
if the argument -ax file is given, Simplify looks for
"file.ax". If the AXIOMDIR environment variable is set,
Simplify looks for that file in the given directory, otherwise,
it looks in its compiled-in bundle. Axiom files use the same syntax
as other input.
The Prover
interface describes (among other things) various environment
variables that can be set to control heuristic parameters that can
affect the performance of Simplify.
FORMULA SYNTAX (PredSx)
This section reproduces the part of the PredSx interface that
defines the syntax of formulas.
(* A "PredSx.T" satisfies the following grammar:
| formula ::= "(" ( AND | OR ) { formula } ")" |
| "(" NOT formula ")" |
| "(" IMPLIES formula formula ")" |
| "(" IFF formula formula ")" |
| "(" FORALL "(" var* ")" formula ")" |
| "(" EXISTS "(" var* ")" formula ")" |
| "(" PROOF formula* ")" |
| literal
|
| literal ::= "(" ( "EQ" | "NEQ" | "<" | "<=" | ">" | ">=" )
| term term ")" |
"(" "DISTINCT" term term+ ")" |
| "TRUE" | "FALSE" | <propVar>
|
| term ::= var | integer | "(" func { term } ")"
"var"'s, "func"'s, and "propVar"'s (propositional variables) are
represented as "Atom.T"'s.
The formula
| (DISTINCT term1 ... termN)
represents a conjunction of distinctions between all pairs of terms in
the list.
The formula
| (PROOF form1 ... formN)
is sugar for
| (AND (IMPLIES form1 form2)
| (IMPLIES (AND form1 form2) form3)
| ...
| (IMPLIES (AND form1 ... formN-1) formN))
"func"'s are uninterpreted, except for "+", "-", and "*", which
represent the obvious operations on integers.
*)
<func>'s are uninterpreted, except for "+", "-", and "*", which
represent the obvious operations on integers.
In addition, the following forms control the environment in which
theorems are proved.
| (BG_PUSH pred)
adds "pred" to the set of predicates assumed to be true, and
| (BG_POP)
removes the last predicate added to the set.
| (LEMMA pred*)
attempts to prove each predicate in the list, assuming all previous
predicates. If all proofs succeed, adds the last predicate in the
list to the set of assumed predicates.
DEFAULT AXIOMS
The default axiom set used by simplify interprets function symbols
defining array operations: select, store, subMap,
storeSub, and mapFill:
| (FORALL (a i x k)
| (EQ (select (store a i x) i k) x))
|
| (FORALL (a i n)
| (EQ (len (subMap a i n)) n))
|
| (FORALL (a i n j k)
| (EQ (select (subMap a i n) j k) (select a (+ i j) k)))
|
| (FORALL (a i x)
| (EQ (len (store a i x)) (len a)))
|
| (FORALL (a i n b)
| (EQ (len (storeSub a i n b)) (len a)))
|
| (FORALL (v i)
| ( EQ (select (mapFill v) i) v)
|
| #| non-unit RHS |#
|
| (FORALL (i j a x k)
| (OR (EQ i j) (EQ (select (store a i x) j k) (select a j k))))
|
| (FORALL (j i a n b k)
| (OR (AND (OR (< j i) (>= j (+ i n)))
| (EQ (select (storeSub a i n b) j k) (select a j k)))
| (AND (>= j i)
| (< j (+ i n))
| (EQ (select (storeSub a i n b) j k) (select b (- j i) k)))))
*)
The axiom set used for ESC/Modula-3 includes the axioms above.
AXIOM SETS
If you specify a customized axiom set, the axioms are S-expressions
that are read from the file using the procedure:
PROCEDURE AddAxioms(rd: Rd.T) RAISES { Error };
(* "rd" must be a reader onto a sequence of syntactically correct
axioms; if not, raises "Error". The syntax for an axiom is:
| axiom ::= "(" ( UNIT | NONUNIT ) vars pat template ")"
| | "(" UNITLHS vars opSym pat template ")"
"vars" is a list of atoms that represent {\it pattern variables} in the
S-expressions "pat" and "template". "opSym" is an atom.
The "UNIT" or "UNITLHS" forms should be used to express a rule
whose template is a literal (hence is a unit clause.) The
"UNITLHS" form should be used to gain some efficiency if the
template is a relation between that matched enode and some other
enode. In the "NONUNIT" form, "pat" is a multipattern; that is, a
list of patterns.
An axiom corresponds to a "Match.MatchingRuleSet" "mrs" such that
"mrs.unit" is "TRUE" for "UNIT" or "UNITLHS" axioms, and "FALSE"
otherwise; "mrs.pats" is the singleton list containing "pat";
"mrs.template" is "template", and "mrs.vars" is the array of atoms
corresponding to "vars". In a "UNITLHS", "mrs.opSym" is
"opSym", in other axioms, it is "NIL". (This means that the
meaning of a "UNITLHS" axiom is "(opsym pat template)".
All the axioms in "rd" are added to the global list of axioms.
*)
until the file is empty. "pat"s and "template"s should follow the
"PredSx" syntax given above.
AUTHOR
Greg Nelson and Dave Detlefs
AUTHOR OF MAN PAGE
Dave Detlefs
[ESC/Java]
[Compaq SRC]
[Compaq Research]
[Compaq]
Copyright © 1999, 2000, Compaq Computer Corporation. All Rights Reserved.
|