perm filename PROVE[3,2] blob sn#424159 filedate 1979-03-10 generic text, type C, neo UTF8

COMMENT ā VALID 00002 PAGES C REC PAGE DESCRIPTION C00001 00001 C00002 00002 PROVE is an interactive theorem prover/simplifier. C00004 ENDMK Cā; PROVE is an interactive theorem prover/simplifier. It automatically finds a normal form for any expression over the language consisting of individual variables, the usual boolean connectives, the conditional function cond (denoting if-then-else), the integers (numerals), the arithmetic functions and predicates +, - and ā¤, the LISP constants, functions and predicates nil, car, cdr, cons and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. Individual variables range over the union of the rationals, the set of arrays, the LISP s-expressions and the booleans true and false. The constant, function and predicate symbols take their natural interpretations. The simplifier is complete; that is, it simplifies every valid formula to true. Thus it is also a decision procedure for the quantifier-free theory of rationals, arrays and s-expressions under the above functions and predicates. The prover also accepts user-defined axiomatizations. More details from DCO.