This package contains the program completeusersproof.c, a second version of
that program, completeusersproofp.c, which may be used as an aid for reading
the program and error detection, and associated files.
Program name: completeusersproof.c
Copyright (C) 2017 NORMAN MEGILL nm at alum.mit.edu http://metamath.org
(for the metamath.c base code)and ALAN SARE alansare at alumni.cmu.edu
(for the completeusersproof() function and functions it
(directly) calls).
License terms: GNU General Public License
This program is built on top of the metamath.c code in order to utilize
the Metamath tools commands. c-emulations of the Metamath tools commands
have been added as functions, created by minor revisions to the
metamath.c code. These functions are called by the
completeusersproof() function and by the functions called by it. The
original metamath.c code is retained in its entirety, including its
comments, except for minor revisions. Most of it is not used by the
functions added to metamath.c.
completeusersproof is intended to automatically complete User's Proofs
written as Virtual Deduction proofs. A Virtual Deduction proof is
a Metamath-specific version of a Natural Deduction proof.
completeusersproof() first invokes mmj2 alone to unify any subproofs it
can. If run in default mode, it then generates a unification theorem for
each incomplete subproof in a second attempt to automatically complete
it. If the unification theorem is not in set.mm but is a semantic
variation of one that is, then it attempts to 2-step prove the
unification theorem to complete the subproof. If the User inserts the
matchstring "don't skip completeusersproofmv()" in any comment line of
the User's Proof, then completeusersproof will also attempt to complete
each subproof not completed by mmj2 alone by adding non-unionized
assertion permutations for unification with a metavariable deduction in
set.mm.
Inputs:
proofworksheet.txt This text file is a Proof Worksheet
conforming to mmj2 requirements. It
initially contains the User's Proof.
The path of set.mm and fd.txt is the
default path specified in
mmj2FalseDeductions.bat and
mmj2StepProver.bat. This default path is
specified to be c:\metamath\ and may be
changed by the User. The program runs
correctly if the folders containing the
mmj2 files are the default folders
generated by the mmj2 download and all
other files of the completeusersproof
download are placed in the mmj2jar folder
of the mmj2 download.
labels.txt This text file is a list of 1-hypothesis
set.mm labels, each with the potential to
to deduce some step in the Proof Worksheet
from some theorem in set.mm.
fd.txt An mmj2 input file of "false deductions".
A false deduction is a true deduction
for which one hypothesis, a "unification
theorem", is implicit.
completeusersproof explicates the
implicit hypothesis and 2-step proves it if
it is not in set.mm and a semantic
variation of it is. For example, syl is the
true deduction corresponding to
the false deduction ff1,
|- (. ph ->. ps ). infers |- (. ph ->. ch ).
The implicit hypothesis is ( ps -> ch ) .
A deduction with an implicit unification
theorem as a hypothesis which is true from
the User's perspective is false from
Metamath's perspective because Metamath
is implicit-hypothesis-blind.
mapFfToEelUunNumPerm.txt This file specifies the one-one
correspondence between each false deduction
in fd.txt and its true counterpart in
set.mm. Column one contains the false
deduction labels and column two contains
the true deduction labels.
This file also specifies the mapping of
each ff* false deduction label into its
corresponding 0th premutation uun* label.
That label is in the 3rd column of the same
row. In the 4th column of the same row is
the number of permutations of uun* labels
corresponding to the ff* label. The uun*
deductions are described at the beginning
of the completeusersproof() function
defintion.
RunParmsFalseDeductions.txt A text file of mmj2 run parameters
referenced by mmj2FalseDeductions.bat.
Two input files are loaded. The first
is set.mm and the second is fd.txt.
mmj2FalseDeductions.bat A .bat file which executes mmj2 using the
run parameters specified by
RunParmsFalseDeductions.txt. It is the
value of the second argument of the first
call of mmj2Unify() by
completeusersproof(). False deductions are
intended to unify with all deductions of
the User's Proof which do not unify with
a true deduction in set.mm.
RunParmsStepProver.txt A text file of mmj2 run parameters
referenced by mmj2StepProver.bat which
invokes the mmj2 unification command.
Distinguishing RunParmsStepProver.txt from
RunParmsFalseDeductions.txt, set.mm is the
sole mmj2 input file of the former.
mmj2StepProver.bat A .bat file which executes mmj2 using the
run parameters specified by
RunParmsStepProver.txt.
Output:
proofWorksheet.txt The User's Proof is edited by
completeusersproof. If the User's Proof
is correct and sufficiently detailed, the
output file may contain a
Metamath-generated RPN proof. Otherwise,
as many subproofs of the User's Proof
will be completed as possible.
Primary Functions:
completeusersproof()
addMvSubtheoremTs()
addMvAssertionSteps()
completeusersproofmv()
addUnionizedAssertionPermutations()
pickAPermutationOfEachUnionizedAssertion()
pickALabelPermutation()
substituteLabels()
stepprover()
removeUnneededFfLabels()
Some Utility Functions:
mmj2Unify()
translate()
tagLabeledSteps()
endTag()
addMTLast()
addMTMT()
addMTMF()
addMT()
substituteMTMT()
deleteEx()
THE VirtualDeductionProofs.txt FILE:
This text file contains Virtual Deduction Users' Proofs of theorems. A Virtual
Deduction proof is a Natural Deduction proof using conventional or virtual
deduction notation. More information about Virtual Deduction may be found in
the web page description of the set.mm syntax definition wvd1 .
Each proof contained in VirtualDeductionProofs.txt may be input into
completeusersproof by copying it onto proofWorksheet.txt. Upon execution of
completeusersproof an RPN Metamath proof in conventional notation is
generated. If the labels specified in the brief description are excluded
from the unification search, then any distinct variable requirements will
not be violated.
PROCEDURE FOR USING completeusersproof.c
step 1. It is assumed that set.mm is in the c:\metamath folder and the mmj2
files exist in the default c:\mmj2 and c:\mmj2\mmj2jar folders.
Download completeusersproof.zip using the link found on the Metamath
web site.
step 2. Unzip it.
step 3. Place fd.txt in c:\metamath folder. If the default path of set.mm
and fd.txt, as specified in mmj2FalseDeductions.bat and
mmj2StepProver.bat, is not c:\metamath, then use the differrent
specified path for fd.txt.
step 4. Place all other extracted files in the c:\mmj2\mmj2jar folder. If
mmj2.bat and associated files are in another folder, then place all
other files in that folder.
step 5. Create a proof of a theorem on a valid mmj2 Proof Worksheet. Use
mmj2 to verify it contains no errors such as, for example, that there
is an invalid symbol in a proof step or a formula contains one or more
grammatical parse errors. Whether the proof is intentionally
constructed as a Natural Deduction proof using Virtual Deduction
notation or not, any valid mmj2 Proof Worksheet constitutes is
acceptable.
step 6. Copy the Proof Worksheet created in step 5 onto proofWorksheet.txt.
step 7. To attempt to complete subproofs by the method of unifying them with
metavariable deductions in set.mm having non-unionized assertions as
well as by the method of mmj2 unification alone and by the unification
theorem method, type "don't skip completeusersproofmv()" on a comment
line of Proof Worksheet. Otherwise, completion of subproofs will be
attempted only by the method of mmj2 unification alone and by the
unification theorem method.
step 8. Double-click on the completeusersproof.exe file to execute
the program. Assuming no errors, the proof will be translated into
conventional notation and completed as much as possible. If the proof
is completed in its entirety an RPN Metamath proof will be generated.
If the User did not intentionally construct the input proof to be
a Virtual Deduction proof, completeusersproof will nevertheless
complete the proof as much as possible.
DESCRIPTION OF completeusersproofp.c
completeusersproofp.c is identical to completeusersproof.c except for
intermittent printf("point *"); and getchar(); pairs of statements
which pause execution until the User presses . "point **"
identifies the line in the program at which execution has paused. At each
pause the User is afforded the opportunity to observe any text file being
edited by the program and to observe which statement executions caused
the observed alterations.
Files which the User may be interested in observing include proofWorksheet.txt,
unifThms.txt, and duplicateUnificationThms.txt.
To observe a text file as it changes, keep the text file displayed during
execution of the program. While execution is paused, click anywhere in the text
file window. This will minimize the ms-dos window and, if TextPad is the text
editor being used, cause a window to pop up stating: "Another application has
updated file c:\mmj2\mmj2jar\.txt. Reload it?" Press "Yes" to update the
file. After viewing the updated text file, maximize the ms-dos window and press
enter to resume execution. Repeat this procedure for every pause in program
execution or only for pauses at points of interest. If completeusersproofp.c
is also kept open during execution of completeusersproofp.exe, then one may
concurrently observe the text file changes and the statements of the code
causing them. The code statements causing changes may be identified by the
statements printed in the console. For example, the changes made to
proofWorksheet.txt immediately preceding the pause at "Point 7 of
completeusersproofmv()" are due to the three statements occurring between the
"Point 6 of completeusersproofmv()" (line 1879 of completeusersproofp.c) and
"Point 7 of completeusersproofmv()" (line 1893 of completeusersproofp.c) print
statements.
The real-time observation of text file changes and the code statements causing
them may be useful for learning the program, for finding program bugs, for
finding deficiencies in data files used by the program, and for finding errors
in the input Proof Worksheet.
AVOIDING UNIFICATIONS WITH REFERENCE THEOREMS WITH UNNECESSARY DISTINCT
VARIABLE REQUIREMENTS
completeusersproof may sometimes unify some proof steps with a reference
theorem(s) with distinct variable requirements which are not necessary to the
proof. In such a case, another(other) reference theorem(s) without distinct variable
requirements or with fewer distinct variable requirements also unifies(unify) with
the relevant proof step(s). The only reason the reference theorem(s) with the
unnecessary distinct variable requirements is(are) picked by completeusersproof.c
over the reference theorem(s) with no or lesser distinct variable requirements is
because it(they) precede(s) the latter reference theorem(s) in set.mm.
The unnecessary distinct variable requirements may be avoided by temporarily
adding the offending theorem(s) to the list of theorems to be excluded
from the mmj2 unification search of the RunParmsStepProver.txt and
RunParsmsFalseDeductions.txt command ProofAsstUnifySearchExclude. If the
program is run again on the original User's Proof, unless another reference
theorem(s) with unnecessary distinct variable requirements unifies(unify) with
the same step(s), the completed proof will not have any unnecessary distinct
variable requirements for that(those) step(s). If a non-excluded reference
theorem(s) with distinct variable requirements unifies with the same step(s),
it(they) too should be excluded. This may be repeated until a completed proof
with the minimum distinct variable requirements is found. If a reference
theorem(s) with distinct variable requirements is(are) excluded and the
User's Proof does not complete, then it is easily determined which reference
theorems with distinct variable requirements are necessary with respect to the
input User's Proof. It is possible that a different proof may exist with fewer
or no distinct variable requirements.
A search exclusion(s) should be specific to a particular proof and should be
removed from the search exclusion list after applying it(them) to that proof.
Otherwise, a future proof may not complete only because a step(s) of the proof
require(s) an excluded reference theorem(s).
A similar strategy may be employed as an alternative means of avoiding
unifications with theorems not in the main set.mm (theorems in Mathboxes).
A computer-assisted procedure to remove labels which violate the distinct
variable requirements of the User's Proof is as follows.
step 1. Complete the User's Proof using completeusersproof.
step 2. If the distinct variable requirements of the Proof
generated by completeusersproof are greater than necessary,
add the proof to set.mm and specify the lesser distinct variable
requirements of the User's Proof. Run the "verify proof" command
of the metamath program. The program will identify the distinct
variable requirement violations.
step 3. Add the offending labels as labels to be excluded to the run parms.
step 4. Run completeusersproof again.
step 5. Repeat steps 2, 3, and 4 until all distinct variable violations
are removed.
DETAILED DESCRIPTION OF THE completeusersproof.c PROGRAM
MOTIVATION FOR COMPLETEUSERSPROOF. As explained in the description of
wvd1, Natural Deduction is a powerful strategy for proving theorems
and deductions. Natural Deduction uses a Gentzen-type system. We are
motivated to write Natural Deduction proofs (for the power of proving
using a Gentzen-type system) and verify them using Metamath's
proofchecking capability. Metamath uses a Hilbert-type deductive system.
As explained in wvd1, the virtual deduction notation has been added to
set.mm to have a language of a Hilbert-type deductive system which
can be used like a Gentzen-type system. Using the virtual deduction
notation of set.mm, one can effectively write Natural Deduction Proofs
in the virtual deduction language of Metamath. We call these proofs
Virtual Deduction proofs. A Virtual Deduction proof is the
Metamath-specific version of a Natural Deduction Proof.
A Virtual Deduction proof generally cannot be directly input on a mmj2
Proof Worksheet and completed by the mmj2 tool because it is usually
missing some technical proof steps which are not part of the Virtual
Deduction proof but are necessary for a complete Metamath Proof. These
missing technical steps may be automatically added by an automated
proof assistant. completeusersproof is such a proof assistant.
completeusersproof adds the missing technical steps and finds the
reference theorems and deductions in set.mm which unify with the
subproofs of the proof.
The User may write a Virtual Deduction proof and automatically transform
it into a complete Metamath proof using the completeusersproof tool. The
completed proof has been checked by the Metamath program. The task of
writing a complete Metamath proof is reduced to writing what is
essentially a Natural Deduction Proof.
Generally, proving using Virtual Deduction and completeusersproof
reduces the amount Metamath-specific knowledge required by the User.
Often, no knowledge of the specific theorems and deductions in set.mm
is required to write some of the subproofs of a Virtual Deduction
proof. Often, no knowledge of the Metamath-specific names of reference
theorems and deductions in set.mm is required for writing some of the
subproofs of a User's Proof. Often, the User may write subproofs of
a proof using theorems or deductions commonly used in mathematics and
correctly assume that some form of each is contained in set.mm and that
completeusersproof will automatically generate the technical steps
necessary to utilize them to complete the subproofs. Often, the fraction
of the work which may be considered tedious is reduced and the total
amount of work is reduced.
* * *
completeusersproof() is the single primary function of the
completeusersproof program. All other functions used by the
completeusersproof program are called by completeusersproof().
The input Proof Worksheet is the "User's Proof". It is intended to be a
correct Virtual Deduction proof. completeusersproof completes each
subproof of the translated User's Proof which it is capable of
completing.
What do we mean by the term "subproof"? A subproof of the User's
Proof could have been called simply a deduction within the User's Proof.
We do not call it a deduction because a technical step or steps may be
automatically added to the proof which are associated with the deduction
may change the deduction into a deduction with more steps or may create
an additional deduction associated with the modified or unmodified
original deduction. The new collection of associated steps may not be a
single deduction and therefore cannot properly be called a deduction.
Therefore, we call this new collection of steps arising from the original
deduction a subproof. Our narrow definition differs from the general
definition of subproof. For the general definition of subproof, a subproof
may include many deductions of a proof. For our narrow definition, a
subproof arises from and is associated with only a single deduction of the
original User's Proof.
DEFINITION OF A VIRTUAL DEDUCTION. In the written description of wvd1 a
virtual deduction is defined to be the analog in H of a sequent in G1. The
connective ->. (a mediator connective) separates the virtual hypothesis
collection on the left side of ->. from the virtual conclusion on the
right side of ->. . A virtual deduction with no ->. connective is a
virtual deduction with no virtual hypotheses. A virtual deduction with no
virtual hypotheses may be alternatively written in "standard T form".
A no-virtual-hypotheses virtual deduction in standard T form has a ->.
connective and an empty virtual hypothesis collection. The empty virtual
hypothesis collection is defined to be T. . |- and
|- (. T. ->. ). denote equivalent virtual deductions, the latter
being the former in standard T form.
DEFINITION OF A CONVENTIONAL NOTATION VIRTUAL DEDUCTION. A conventional
notation virtual deduction is a virtual deduction with conventional
notation symbols substituted for virtual deduction symbols. If a
conventional notation virtual deduction has no -> connective, then it
has no virtual hypotheses. If one or more -> connectives occur in it,
then the outermost -> connective is the mediator connective or(excl.)
none of the -> connectives is the mediator connective and there are no
virtual hypotheses.
Some conventional notation virtual deductions are susceptible to more than
one interpretation. Hopefully, the virtual deduction's context fully
determines which interpretation is the correct one. As an example of
ambiguity, the conventional notation virtual deduction
|- ( x e. A -> x C_ B ) may correspond to the virtual deduction
|- (. x e. A ->. x C_ B ). or(excl.) to the no-virtual-hypotheses
virtual deduction |- ( x e. A -> x C_ B ) .
The reason each step of a User's Proof is specified to be a virtual
deduction with virtual deduction notation is to assure that each
step of the proof has a unique interpretation. After the proof is
translated, the correct interpretation of any original step, now a
conventional notation virtual deduction, may be determined by its
interpretation prior to translation if context alone is insufficient for
disambiguation.
The completeusersproof program relies on the virtual deduction notation
because there is no ambiguity. Therefore, it is necessary for the User's
Proof to be in virtual deduction notation in order to utilize the full
potential of completeusersproof to complete as many of the subproofs of
the User's Proof as possible. If a User's Proof is not written as a
Virtual Deduction proof, then completeusersproof will interpret each step
of the proof to be a virtual deduction with no virtual hypotheses.
One sufficient reason why conventional notation virtual deductions are
used is because the theorems and deductions in set.mm are in conventional
notation and are fully utilized if and only if the steps of the User's
Proof are translated into the same conventional notation after the
disambiguation information contained in the original Virtual Deduction
proof is extracted and saved. It is saved in the ff* labels. A virtual
deduction subproof cannot unify with a theorem or deduction in the main
set.mm unless it is in conventional notation.
The power of Natural Deduction in simplifying proving is fully realized
by writing proofs using virtual deduction wwfs, which are the analog in H
of sequents in G1 (see: the description of wvd1). It is possible to use
only conventional notation virtual deductions and prove by Natural
Deduction, but, in so doing, the proof writer has the burden of writing
in a language for which some wffs are subject to more than one
interpretation. More importantly, completeusersproof cannot be used to
effectively to complete such proofs.
* * *
We will sometimes refer to a conventional notation virtual deduction as
a "virtual deduction". Hopefully context will determine whether
"virtual deduction" means a virtual deduction in non-conventional
notation or a conventional notation virtual deduction.
It is intended that any User's Proof to which completeusersproof will
be applied is input as a Virtual Deduction proof in non-conventional
notation. A proof is a Virtual Deduction proof in non-conventional
notation if every step of the proof is a virtual deduction in
non-conventional notation.
Early in the execution of completeusersproof the original Virtual
Deduction proof in non-conventional notation is translated into
a conventional notation Virtual Deduction proof. Of the steps of the
proof automatically generated by completeusersproof towards the goal
of completing the original proof, each added step is a conventional
notation virtual deduction unless it is a non-unionized assertion
step. The wff of a non-unionized assertion step is not a virtual
deduction unless every element of its collection of virtual
hypothesis collections is a virtual hypothesis. These terms are
defined below.
Early in the execution of completeusersproof(), the virtual deduction
steps of the User's Proof are translated into conventional notation
virtual deductions. For example, the virtual deduction
|- (. (. Tr A ,. ( z e. y /\ y e. A ) ). ->. z e, A ). (wff1)
is automatically translated to be
|- ( ( Tr A /\ ( z e. y /\ y e. A ) ) -> z e, A ) (wff2)
wff2 is the conventional notation virtual deduction counterpart of
virtual deduction wff1. ( Tr A /\ ( z e. y /\ y e. A ) ) is the virtual
hypothesis collection of wff2.
With translation, " ,. " becomes " /\ ", " ->. " becomes " -> ", " (. "
becomes " ( ", and " ), " becomes " ) ".
A metavariable deduction is a deduction for which each hypothesis step may
be interpreted to be a conventional notation virtual deduction having a
virtual hypothesis collection which is a wff variable. We use the term
"metavariable" for the wff variable as Mario Carneiro has in his
presentation "Natural Deduction in the Metamath Proof Language" presented
in the summer of 2014. We say a metavariable deduction is in standard form
if the elements of the collection on the left side of the mediator -> of
its assertion are exactly the virtual hypothesis collections of the
hypothesis steps. Unless a standard form metavariable deduction has only
one hypothesis, its assertion is not a virtual deduction because its
collection of virtual hypothesis collections is not a virtual hypothesis
collection. We could have defined this collection to be a virtual
hypothesis collection on the ground that a wff variable is an single
variable. We don't use that definition because a wff variable is a
schemata for a virtual hypothesis collection. An example of a standard
form metavariable deduction in set.mm is trelded.
We say that the collection of virtual hypothesis collections of the
assertion of a standard form metavariable deduction with more than one
hypothesis is "non-unionized" and that the assertion is a non-unionized
assertion. We use the term "union" because unionizing a collection of
virtual hypothesis collections to obtain a virtual hypothesis collection
is analogous to taking the union of a class. We define a "unionized
assertion" to be an assertion derived from a non-unionized assertion by
unionizing its collection of virtual hypothesis collections. The
unionized collection is a virtual hypothesis collection consisting of the
elements of the elements of the collection of virtual hypothesis
collections of the non-unionized assertion. The virtual hypothesis
collection of a unionized assertion contains no duplicate elements.
One possible way a subproof may be completed is by unifying it with a
standard form metavariable deduction in set.mm. If the unifying
standard form metavariable deduction in set.mm is a 1-hypothesis
deduction, then it will unify with the original deduction of the subproof.
If the unifying standard form metavariable deduction in set.mm has more
than one hypothesis, then it will not unify with the original deduction of
the subproof because the assertion of the original deduction is unionized
whereas the assertion of the metavariable deduction in set.mm is not.
completeusersproof generates a non-unionized assertion. The deduction of
that non-unionized assertion, which has the same hypotheses as the
original deduction, unifies with the metavariable deduction in set.mm.
The assertion of the original deduction is deduced from the non-unionized
assertion with a 1-hypothesis uun* deduction, which becomes a second
deduction of the subproof. The number of steps of the subproof
increases by one step. That added step is the non-unionized assertion.
The non-unionized assertion immediately precedes the unionized assertion,
which is the original assertion of the subproof. completeusersproof
automatically generates the contents of the hypothesis field of the
non-unionized assertion step to be the same as the original contents of
the hypothesis field of the original subproof. completeusersproof deletes
the original contents of the original assertion's hypothesis field and
inserts into that hypothesis field the step number of the non-unionized
assertion step.
Each metavariable deduction in standard form in set.mm has a particular
ordering of metavariable virtual hypothesis collections within the
collection of virtual hypothesis collections of its assertion. The
ordering of the virtual hypothesis collections of the collection of
virtual hypothesis collections of the generated non-unionized assertion of
a deduction of a subproof of a Proof Worksheet to be unified with a
metavariable deduction in set.mm must match the ordering of the collection
of the assertion of the metavariable deduction in set.mm. Therefore, all
possible permutations of the ordering of the virtual hypothesis
collections within the collection of virtual hypothesis collections of the
non-unionized assertion must be tried. completeusersproof() generates from
the subproof of the original User's Proof n-1 additional subproofs, where
n is the number of possible permutations in the ordering of the virtual
hypothesis collections of the collection of virtual hypothesis collections
of the hypotheses of the subproof. The steps of each of these
subproofs are identical, except that the ordering of the virtual
hypothesis collections of the collection of virtual hypothesis collections
of each non-unionized assertion is different from every other. One of
these subproofs will unify with the metavariable deduction in set.mm
to mv-complete it. After that subproof is mv-completed, the subproofs with
the other permutations are deleted.
For each ff* false deduction corresponding to a subproof of the User's
Proof there corresponds a collection of uun* labels which contains all
possible permutations of uun* deductions which deduce the unionized
assertion from the non-unionized assertion. For example, the virtual
hypothesis collections for the two hypotheses of a subproof of a User's
Proof may be ( /\ ) and . Then there are a total of
two uun* permutations which deduce the unionized assertion from the
non-unionized assertion. One has as its hypothesis an assertion with the
collection of virtual hypothesis collections
( ( /\ ) /\ ) and the other
( /\ ( /\ ) ) . The unionized assertion for both
deductions is the same and is specified by the original User's Proof. Its
virtual hypothesis collection should be ( /\ ) or(excl.)
( /\ ) .
If the virtual hypothesis collections of the hypotheses of a metavariable
deduction in standard form in set.mm are identical, then the union of the
the collection of virtual hypothesis collections of its hypotheses is
identical to the virtual hypothesis collection of each hypothesis. Any
metavariable deduction in set.mm having the same virtual hypothesis
collection metavariable for each hypothesis may have as its assertion a
virtual deduction having the same virtual hypothesis collection as the
hypotheses. A metavariable deduction in this form will unify with a
subproof in a Proof Worksheet using mmj2 alone. Mario Carneiro has
employed this metavariable deduction form for many deductions he has
added to set.mm. He discussed it in his presentation "Natural Deduction
in the Metamath Proof Language".
Some steps of a User's Proof may have no virtual hypotheses. For example,
|- A C_ suc A (wff3)
may be such a step in a User's Proof. It is originally a virtual deduction
in non-coventional notation. Upon translation of the proof, it becomes a
conventional notation virtual deduction. Because it has no virtual
hypotheses, the syntax of wff3 is the same whether it is interpreted as a
virtual deduction in non-conventional notation or a conventional notation
virtual deduction. wff3 may be put in "standard T form" so that it is a
virtual deduction having a virtual hypothesis collection which is empty.
|- (. T. ->. A C_ suc A ). (wff4)
wff4 is wff3 in standard T form. wff4 translated is
|- ( T. -> A C_ suc A ) (wff5)
Both wff4 and wff5 are virtual deductions. wff4 is a virtual deduction in
non-conventional notation and wff5 is a conventional notation virtual
deduction. Both have the same interpretation.
In order for completeusersproof() to attempt to mv-complete a subproof
of the User's Proof (complete it by unifying it with a metavariable
deduction in set,mm) it puts each no-virtual-hypotheses step of the
subproof into standard T form. This is necessary because every
hypothesis of a metavariable deduction in set.mm must have a metavariable
virtual hypothesis collection.
The union of a singleton is its element. U. { A } = A . A virtual
hypothesis collection differs from a class in that a singleton
virtual hypothesis collection is identical to the virtual
hypothesis it contains. If x e, A is the virtual hypothesis of a singleton
virtual hypothesis collection, then that collection must be denoted by
x e, A because ( x e. A ) is syntactically invalid. The collection
on the left side of the mediator -> of the assertion of an instance of a
metavariable deduction in set.mm (e.g., trelded) is a collection of
virtual hypothesis collections. Because a singleton virtual hypothesis
collection is a virtual hypothesis, some elements of a collection of
virtual hypothesis collections may be virtual hypotheses. If each element
of a collection of virtual hypothesis collections is a singleton virtual
hypothesis collection and these are pairwise distinct, then the collection
of virtual hypothesis collections is a virtual hypothesis collection. The
requirement that the singleton virtual hypothesis collections are pairwise
distinct is based on the convention that a virtual hypothesis collection
does not contain duplicate elements.
( /\ ( /\ ) /\ T. ) is a collection of virtual
hypothesis collections occuring in a completeusersproof()-generated
non-unionized assertion of a subproof of a Proof Worksheet. is
the virtual hypothesis collection of one hypotheses of that
subproof, ( /\ ) is another, and T. is the third. The
collection of the unionized assertion for this subproof, which was a step
in the original User's Proof, is ( /\ /\ T. ) . The
collection of the non-unionized assertion is not a virtual hypothesis
collection because the element ( /\ ) is not a virtual
hypothesis because it is not atomic because it can be sub-divided into two
virtual hypotheses. Even if this element was split into two separate
virtual hypotheses, the resultant collection is not a virtual hypothesis
collection because it contains two virtual hypotheses. This is
consistent with one of the motives of the virtual hypothesis collection
definition. It is undesirable for a virtual hypothesis collection to
contain duplicate virtual hypotheses because the virtual hypothesis
collection is denoted by a longer and more complex character string which
does not contain more information.
In general, any subproof of a Proof Worksheet for which the virtual
hypothesis collection of the original assertion is identical to the
collection of the virtual hypothesis collections of the subproof's
hypotheses does not need a non-unionized assertion and will be
mv-completed by mmj2 unification alone if a unifying metavariable
deduction exists in set.mm.
Generally, a subproof of a translated User's Proof may unify with a
deduction in set.mm without any steps added to the original subproof. A
subproof with no added steps unifying with metavariable deduction in
set.mm having a unionized assertion is a special case of this. Such
subproofs are completed by mmj2 unification alone. This is one of the
means by which a subproof in a User's Proof is completed.
completeusersproof() is designed to first attempt to complete each
subproof of the User's Proof by mmj2 unification alone. If mmj2
unification alone does not complete a subproof, then each step
may be put in standard T form and all possible permutations of
non-unionized assertions are added and mv-completion may be attempted.
Another strategy for completing subproofs of a User's Proof is by
the automatic adding of a unification theorem to a subproof. Without an
explicit request by the User, by default, completeusersproof()
will first attempt mmj2 unification alone to complete each subproof of
the User's Proof. It will then attempt to complete any subproofs which
did not complete by mmj2 uification alone by adding a unification theorem
and, if necessary, by adding another step to 2-step prove that unification
theorem. If these attempts fail to complete the subproof, then that
subproof will not be completed running completeusersproof() in the default
mode.
If the User includes the matchstring "don't skip completeusersproofmv()"
on any comment line of the User's Proof, then completeusersproof() will
first attempt mmj2-alone unifications. For those subproofs not completing
by mmj2 unification alone, it will put all steps with no virtual
deductions in standard T form attempt to complete each of these subproofs
by automatically generating all possible non-unionized assertion
permutations and attempting to mv-complete those subproofs. Finally, for
any subproofs not completed by either of those methods, it will begin anew
and attempt completion by adding a unification theorem to each and, if the
unification theorem is not in set.mm, it will attempt to 2-step prove the
unification theorem.
We shall now discuss the unification theorem method of completing a
subproof. Each subproof not one step of any valid Virtual Deduction User's
Proof unifies with a deduction in set.mm, or, if it does not, with a ff*
false deduction in fd.txt. 1-step subproofs unify with a theorem in set.mm
or(excl.) do not unify. Each ff* false deduction corresponds to an eel*
deduction which is the same as the ff* deduction, except it is in
conventional notation and has an additional hypothesis, a "unification
theorem", which may make the false subproof true. completeusersproof replaces
the ff* label with the eel* label and automatically adds the unification
theorem step to the subproof. If the unification theorem unifies with a
theorem in set.mm, then the adding of the unification theorem has made the
the originally false subproof true and the subproof is completed.
The unification theorem of a virtual deduction deduction is that unique
virtual deduction whose virtual hypothesis collection is the collection of
the virtual conclusions of the hypotheses of the virtual deduction
deduction and whose virtual conclusion is the virtual conclusion of the
assertion of the virtual deduction deduction. Every unification theorem is
a theorem, which may or may not unify with a theorem in set.mm.
If set.mm is sufficiently rich with respect to the mathematics which is
the subject of the User's Proof, then it is likely that the unification
theorem of a subproof or a semantic variation of it will be a theorem in
set.mm. If the unification theorem unifies with a theorem in set.mm, then
completeusersproof completes the subproof by adding it alone. If the
unification theorem does not unify with a theorem in set.mm, then the
stepprover() function of completeusersproof() will attempt to 2-step prove
the unification theorem. If there exists in set.mm at least one semantic
variation of the unification theorem and if there exists in set.mm at
least one 1-hypothesis deduction which deduces the unification theorem
from one of its semantic variations in set.mm, then stepprover()
automatically generates an additional step which is a semantic variation
of the unification theorem and which unifies with a theorem in set.mm and
completes the subproof. Otherwise, the added unification theorem remains
unproven and the subtheorem, although proveable (assuming the original
subproof is correct), is not completed.
The capabilities of completeusersproof() which mmj2 does not have are:
1) the ability to generate a unification theorem as an additional
hypothesis step of a subproof; 2) the ability to 2-step prove a
unification theorem which does not directly unify with a theorem in set.mm
but is a semantic variation of a theorem which does unify with a theorem
in set.mm; 3) the ability to generate non-unionized assertion step
permutations of a subproof when an mv deduction in set.mm will unify
with the subproof with a non-unionized assertion permutation but will
not unify with the subproof with only the unionized assertion in the
User's Proof; and 4) the ability to automatically put
no-virtual-hypotheses steps of the original User's Proof into standard T
form, which is needed in order to mv-complete mv-completable subproofs
of the User's Proof containing such steps.
*