1. audit <source-filename> <theorem-number>

scans a source file for dependencies upon, and for dependencies of, a proposition in that file whose number is given as the second parameter. The theorem-number has the form num.num. The source-filename is given WITHOUT its ".tex" extension.

2. check <source-filename> <theorem-number> [<rules-filename>]

takes as a second parameter the number of a theorem whose proof is to be checked. The first parameter is the name of the file containing the proof. The optional third parameter specifies a file of inference rules to be searched. Its default value is rules.tex. If the file name given in the third parameter begins with debug then the unifier works in a verbose debugging mode that displays every attempted unification. Both files are TeX files and are given WITHOUT their ".tex" extensions.

For each step of the proof of the specified theorem check searches the rules file for a rule of inference which justifies the step and if it succeeds prints out the line number of the first such rule found, and otherwise reports that the step does not check.

3. checkall <source-filename> [<theorem-number-pattern>]

checks the proofs of all those theorems whose numbers are in the .pfs file associated with the source file, unless a second parameter is supplied. This optional parameter filters the list of proofs to be checked. Theorem numbers are matched against the theorem-number-pattern using Python regular expression syntax,

checkall reports each successful check with a "<theorem-number> checked" message and each failed attempt with just the <theorem-number> ". A list of checked theorem numbers is sent to the file checked.

The source-filename is given WITHOUT its ".tex" extension.

Example

checkall book [2-4]\.

checks all theorems in a file "book.tex" with numbers beginning "2." "3.", or "4.". Because a dot is used in regular expression patterns as a wild card the slash is necessary. Including the slash dot prevents matches with theorems numbered "29.2", "45.6", etc.

4. mathparse <source-filename>

tries to parse each TeX math expression, each expression enclosed in dollar signs in other words. It halts when it encounters an expression that it cannot parse. It uses syntax information stored in the ".dfs" file to do the parse. Any new definitions encountered are reported and the updated information is stored in the ".dfs" file.

The source-filename is given WITHOUT its ".tex" extension.

5. padscope <source-filename> <padded-output-filename>

adds horizontal space after all bound variable scope indicators such as "for all x in A". This is a minor touch up to relieve crowding.

The filenames are given WITHOUT their ".tex" extensions.

6. parse <source-filename>

searches for propositions and proofs. Any math expression numbered using the "\prop" macro is taken as a proposition. A proof is either a simple justification or a sequence of math expressions marked as notes, using the "\note" macro, together with justifications marked using the "\By" macro, and terminated by a QED, indicated with the "\Bye" macro. If a proposition is followed by a proof then parse attempts to parse the proof as well as the proposition. parse halts when it encounters a proposition or a proof which it cannot parse. Any new definitions encountered are reported as well as the number of proofs, old definitions, and unproved propositions. The number of each proposition with a proof is stored in a ".pfs" file for the use of checkall.

The source-filename is given WITHOUT its ".tex" extension.

7. renote <source-filename>

renumbers all the notes in each proof so as to make them consecutive. This allows an author to insert notes with a haphazard or arbitrary numbering while the proof is in development.

The source-filename is given WITHOUT its ".tex" extension.

8. renum <source-filename>

renumbers all the propositions in so that they are consistent with the chapter numbering (or section numbering in LaTeX). The renumbering applies to all references anywhere in the document. To avoid catching references to external documents in the renumbering the dot in these external references may be enclosed by braces: {.} renum also creates a time-stamped ".rnm" file with a map of the renumbering.

The source-filename is given WITHOUT its ".tex" extension.

9. resetdefs <source-filename>

wipes the slate of definitions in the ".dfs" file clean and restores it to just those called for by the included ".tdf" or ".ldf" files. This is necessary when definitions are changed to prevent old definitions from conflicting with new ones. It is also used to create an initial ".dfs" file when none exists. The source-filename is given WITHOUT its ".tex" extension.

10. resetprops <source-filename> [<properties-filename>]

changes the operator properties assumed by the unifier to those specified in the properties file. This change is recorded in the ".dfs" file. The default for the properties file is properties.tex. The filenames are given WITHOUT their ".tex" extensions.

1. .tdf (or .ldf) File

This file contains any ProofCheck macros the user cares to store pertaining to the source file. It is a TeX file and it should be invoked with an \input statement near the beginning of the source file. It contains the TeX macros needed in order for TeX (or LaTeX) to be able to process the file. These macros may be included in the source file itself and the file is therefore optional. These macros define the typesetting of the constants introduced by the author in the source file. When the number of these constants grows large it avoids clutter to put the macros for them in a separate file. The maintenance of this file is the responsibility of the author.

When the definitions in a source file are relied upon in another file this dependence is indicated by using the ".tdf" file of the first file as an include file. A ".tdf" file is therefore a kind of header file.

2. .dfs File

This file records syntax information from the mathematical definitions contained in the source file as well as other information. It is initialized by running parse on the source file. It is a Python data file. The information in it is stored cumulatively. To "undo" a definition stored in the ".dfs" file resetdefs should be run on the source file.

3. .pfs File

This file is a just a list of the numbers of all the theorems in the source file which are followed by a proof. It is produced by parse and used by checkall.

1. utility.tdf (utility.ldf)

This file contains the basic macros needed to allow parse and check to run. The author is free to add ProofCheck macros or TeX macros to it to customize the behavior of ProofCheck. The line

\input utility.tdf

needs to be one of the first statements in a source file containing proofs to be checked.

2. common.tex

References in proofs to theorems in external files may begin with lower case letters or a zero. The external file referred to by references beginning with zero is by default common.tex. This file contains mainly mathematics which is ordinarily taken for granted. Thus a reference expression such as "09.26" refers to the Theorem 9.26 in this file. To change the default use "%external_ref 0 <another-file>".

3. common.tdf (common.ldf)

The ".tdf" or ".ldf" file associated with common.tex contains macros needed to express the mathematics in common.tex. If this file is used for external references, then the line

\input common.tdf

needs near the top of the source file along with the include file, utility.tdf. Any other external file whose syntax is relied upon by the source file should also have its associated ".tdf" (or ".ldf") file included as well. When a ".dfs" file is initialized it is assembled from the ".dfs" files associated with all the included ".tdf" (or ".ldf") files.

4. properties.tex

This file contains theorems stating properties such as the commutative and associative properties of "\And". Its syntax is rigid and hence the file should not be carelessly edited. The unifier relies by default on this file for properties and so does the multi-line note parser. If an operator such as "<" has its transitive property stored in this file then this transitivity is recognized by the parser and is used in checking proofs. To use a different file as the properties file call resetprops, which stores a set of properties in the ".dfs" file.

5. rules.tex

This file is the default rules of inference file. In this file, or any file used as a file of rules, a line is parsed as a rule if it contains a dollar sign. Other lines are effectively comment lines. The format of a rule of inference is:

<goal> <= <mathematical formulas and reference punctuators>

where the reference punctuators come the following list

( ) + , - : ; | U

and the goal and other mathematical formulas are dollar delimited. The modus ponens rule for example is stated in rules.tex as follows:

$\qvar$ <= $(\pvar \c \qvar)$;$\pvar$

which is TeX for

q <= (p --> q) ; p

The sole reference punctuator used in this rule is the semi-colon. A note can be justified by the modus ponens rule if it carries a justification such as:

\By 1.2;.3

and the expression formed by the note followed by Theorem 1.2, the semi-colon, and note 3 can be unified with the modus ponens rule. In order for the unification to succeed Theorem 1.2 must have the form (p --> q) and where note 3 is p and the note being justified is q.

The punctuation in a justification must match that of the rule of inference it is to match exactly. The goal and the propositions referred to in the justification are matched against the corresponding formulas in the rule of inference and the unifier looks for a match. A different rule of inference file may be used if its name is supplied as the third parameter of check. Variables near the beginning of the alphabet in the list fixed_variables are fixed when given to the unifier and other variables must be replaced to match them (and not vice versa).

1. %def_symbol <user-symbol> <support-file-symbol>

allows an author to set up a symbol which will function as the equivalent of symbol used in ProofCheck's default supporting files, such as the rules of inference or common notions files. This only works for symbols that are written in TeX beginning with a backslash.

Example: The inverted letter 'A', written in TeX as '\forall', is generally used as the universal quantifier. The default rules of inference file uses an inverted 'V', written as '\Each'. To use '\forall' in documents an author may define:

%def_symbol \forall \Each

This definition may occur in either the document itself or in one of the document's include files.

2. %external_ref <prefix> <external-filename>

defines a short prefix to be prepended to numerical theorem references which refer to theorems in files other than the one whose proof is being checked. The short prefix must consist of lower case letters.

Example: Suppose that an author needs to use Theorem 3.4 from a file "limits.tex." To set up the letter 'a' as an abbreviation for this external file the following definition could be used:

%external_ref a limits.tex

This would enable the author to invoke Theorem 3.4 in a proof using the reference "a3.4".

3. %major_unit: <latex-sectioning-unit>

is used with LaTeX to determine which LaTeX sectioning unit the major number of ProofCheck major.minor theorem number pairs, should keep in step with. The default is section. Other possibilities are chapter, subsection, etc.

4. %set_precedence <math-symbol> <number>

is used to assign a precedence value to an infix math-symbol. The math-symbol is given WITHOUT its TeX dollar signs.

Example: Suppose an author wanted to set up an infix operator \lessthan with a precedence value of 6 . The following assignment could be made:

%set_precedence \lessthan 6

This would allow the free infix usage of \lessthan.

5. %undefined_formula: <math-expression>

is used when a formula that is undefined needs to be declared so that it is recognized by the parser but is either inconvenient or impossible to define. The math-expression is given WITHOUT its TeX dollar signs.

6. %undefined_term: <math-expression>

is used when a term that is undefined needs to be declared so that it is recognized by the parser but is either inconvenient or impossible to define. The math-expression is given WITHOUT its TeX dollar signs.

1. \By <reference-expressions and reference-punctuators>

is the general form of most justifications. For more on justifications see Justifications

2. \Bye <reference-expressions and reference-punctuators>

signals the end of a proof. It is rendered with a QED.

3. \chap {<num>. <chapter-title >}

is used for chapter titles in a TeX file. In a LaTeX file, LaTeX section headers are used instead. Proposition numbers are arranged according to the chapter (or section numbers). The author need not enter these numbers consecutively since renum will renumber chapters and propositions so as to make them consecutive.

4. \linea, \lineb, \linec,..., \linez

These are the line indentation macros. The first seven of these 26 macros produce a line break followed by a prescribed indentation, 20 points for \linea, 40 points for \lineb, 60 points for \linec, etc. The others may be defined as needed by the author.

TeX takes expressions enclosed in dollar signs as mathematical expressions. Syntactically complete terms or formulas are sometimes too long to be conveniently handled as single TeX math expressions. ProofCheck allows complete terms or formulas to be broken into pieces provided these pieces are separated only by white space, these line indentation macros, and in the case of multi-line notes, justifications.

5. \noparse

turns off the parser for the remainder of the line in which it occurs. This is useful since it is sometimes necessary to use mathematical symbols or notation out of context in a way which cannot be parsed.

6. \note <note-number> <note> [<justification>]

A note-number is any natural number of no more than four digits. It is rendered with an initial dot. The note is some mathematical assertion used in the proof. A justification begins with a \By macro.

7. \prop <proposition-number> <proposition> [<justification>]

Every definition, axiom, or theorem which needs to be referred to later must be introduced in this way. A theorem may be followed by a proof.

The proposition-number must take the form: num1.num2 where num1 is the chapter number (or section number in LaTeX)

The proposition must be enclosed in TeX dollar signs. It may be broken into more than one math expression so as to span multiple lines, only if these expressions are separated by line indentation macros.

1. Types of Symbols

The parser recognizes two kinds symbols: constants and variables. There are in turn four types of variables: term variables and formula variables of the first order and of the second order, with first order term variables, also called object variables, by far the most common. The other three types of variables are sentential variables which are formula variables of the first order, term schemators, and formula schemators. When just variables are referred to it will be object variables referred to unless there is explicit qualification to the contrary.

2. Basic Forms

The basic forms are the elementary terms and formulas from which the language is generated by substitution. Basic forms result either from definitions -- the left side of any definition is automatically a basic form -- or they may be simply declared.

Because definitions are used as propositions internal to the inferential system along with axioms and theorems, the substitutions which generate the complex terms and formulas from the basic terms and formulas must necessarily be those which are inferentially valid.

ProofCheck's grammar does not accomodate contextual definition. For example one cannot define addition of classes [x] by defining ([x] + [y]). Here the expression ([x] + [y]) is a composite involving distinct basic forms (A + B) and [x]. These need to be defined separately. Similarly the commonly used definition of limit as ((limit x f(x) = L) if and only if For every epsilon, etc.) is contextual and not admissable. The left side contains previously defined basic forms for equality, (A = B), and functional evaluation, f(x). To define the limit as the number L having such and such a property one can use a definite description.

3. Free and Bound Variables

A variable is free in a basic form if it occurs no more than once. It is free in other words if it occurs in none of the schematic expressions of the basic form.

A variable is free in a term or formula if every occurrence is a free occurrence. This is the case if it never occurs in a location occupied by a V in the signature of a basic form. In particular a variable that does not occur at all is free.

A basic fact noted by Morse is the following: If a variable v is free in a term or formula F and v is replaced by a term or formula G then the result is a term or formula in which any variable x is free if and only if it is free in both F and G.

A variable is bound in a basic form if it does not occur exactly once.

A variable is bound in a term or formula if every occurrence is a bound occurrence.

If s is a schematic expression occurring in a basic form B and then a term or formula obtained by replacing s by a term or formula F then a variable x is bound in the result if and only if x is bound in B and if x is not bound in F then x occurs in s. (It is assumed that F is a term if and only if the intial symbol of s is a term schemator.)

4. Rules for Definitions

If L and R are the left and right sides of some definition then then

1. Every object variable is bound in L if and only if it is bound in R.
2. Every sentential variable occurs in L if and only if it occurs in R.
3. Every schemator occurs in L if and only if it occurs in R.

On the set of definitions we require that:

4. If L is the left side of definitions D and D' then D is D'.

5. The Abbreviation Layer

The grammar also has features to allow automatic removal of some parentheses, conventional abbreviations used in connection the scope of quantifiers, and some other abbreviations. These abbreviational conventions can be enabled using definitions generated by schemes.

6. Summary

Lists of symbols occurring in the common notions file are here:

Infix Operators

Prefix Operators

Bound Variable Operators

Constants

Variables

You can test expressions here: Online Expression Parser.

1. Second order unification

The unifier handles first and second order term and formula variables. First order term variables, ordinary object variables in other words, may occur bound in expressions submitted to the unifier.

2. Variables as Constants

Variables in expressions sent to the unifier must be distinguished according to whether they are subject to substitution in order to achieve unification or whether they are to be treated as constants. Generally speaking the variables in a goal being checked are treated as constants, while those in rules of inference and theorems are not.

3. AC-unification

The unifier is an AC-unifier, in that infix operators whose associative and commutative properties have been stated in theorems stored in the properties file are matched, with these properties allowed for in the unification.

Example

(p \And q \And r) matches (r \And p \And q)

In matches between such conjunctions, a sentential variable in one may match with a subset of the conjuncts in the other.

4. Searches Refused

If a rule of inference contains a conjunction (p \And q) where p and q are not in any way distinguished, then a search for a match of this conjunction with n conjuncts would require searching over all subsets of these n conjuncts. These searches are refused by the unifier. No match will be found. Rules of inference which entail such searches are effectively ignored. The unifier is therefore incomplete as a matter of policy.

Searches in analogous situations are also refused.

Rules of inference need to be stated without the use of unnecessary variables.

1. Transitive Operators

An operator is a transitive operator if there is a theorem stating its transitive property stored in the properties file. By default the properties file is properties.tex. According to this file the implication sign, for example, is a transitive operator.

The default properties file may be changed to some other file by running resetprops.

Only infix operators can be recognized as transitive.

2. Parsing

A multi-line note is broken into subgoals called delta goals which are combined to form sigma goals.

Example

(p \And q \c x < y

< z

< w)

The first line is parsed as:

(p \And q \c x < y)

This goal is referred to as a delta goal. The second line parses into two goals, a delta goal:

(p \And q \c y < z)

and a sigma goal:

(p \And q \c x < z)

The third line also parses into a delta goal:

(p \And q \c z < w)

and a sigma goal:

(p \And q \c x < w)

When a multi-line note is invoked later in a proof it is the last sigma goal which is referred to.

3. Checking

Steps in a multi-line proof require on the average two goals to be checked instead of just one. A multi-line note with n steps produces (2n - 1) goals.

Justifications on each line of a multi-line proof are attached to the delta goals. More abstract transitivity theorems, in particular those in the properties file are invoked in order to check the sigma goals. The search for these is an exception to the general rule that ProofCheck does not search for theorems.