Search Options

Here is a mock-up of the Search Options screen. Note the SEARCH DATA and SEARCH PREFERENCES sections. Search Data must be entered befor each search -- or restored via the saved data on the PrevSearchData menu, whereas the SEARCH PREFERENCES are retained from one search to the next.

Pulldown menus are indicated with "|+|" .
"........." indicates pulldown text.
Single "X" indicates Toggle On/Off.
"XXXXXXX" indicates text entry/display.
"99999" indicates numeric entry.
Buttons are (crudely) indicated in the mockup at the bottom of the screen like this: "//New Search\\".

mmj2 Search Options THEOREM XXXXXXXXXXXX LOC_AFTER XXXXXXXXXXXX STEP XXXXXX
File Cancel Edit Other PrevSearchData Queries Tools Help
____SEARCH_DATA____________ //reset\\    Text-Separators: OR: OR   QUOTE: "
Search-In-What      Format     Oper   Search-For-What                 Or
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X
From Chap |.....................|+| Sec |..............................|+|
Thru Chap |.....................|+| Sec |..............................|+|
____SEARCH PREFERENCES_____ //reset\\
Exclusion: Labels: XXXXXXXXXXXXXXXXX Extended Search:
   99999 Min Times Used In Proofs     99999 Min Completed Search Results
   99999 Min Hyps                     99999 Check First N Search Results
   99999 Max Hyps                     99999 Max Incomplete Hyps
   99999 Max Search Results 99999 Max Prev Steps Checked
       X Must Be Unifiable With Step      X Reuse Derivation Steps
       X Use Chapter/Sec. Hierarchy      Output:
       X Search-Proximity Scoring     99999 Max Elapsed Seconds
                                          X Show Unification Subst.
                                            X Auto-Select (Update Proof Step)
   Output Sort Seq: |.....................................................|+|
//new   \\ //refine\\ //halt \\ //goto proof\\ //goto step\\
\\search// \\search// \\search// \\assistant // \\selector //

SCREEN FLOW

Here is how the three screens interact:

Search Screen Flow Diagram

Addition of the Search Options window is the primary enhancement we're making to the Step Selector Search.

Key points:

Double-click (or menu item) a proof step on the Proof Assistant and the next window you see is the Step Selector Search showing the results of searching using the current Search Preferences and no Search Data criteria. (Another menu option, Reuse Step Selector Search performs a search reusing existing Search Data criteria.) From the Step Selector Search window you can go either to the Search Options window to refine your search, or back to the Proof Assistant to apply a selected assertion from the search results -- or to start over.
Or, Ctrl-S (or menu item) a proof step on the Proof Assistant to pull up the Search Options window, where Search Data may be added to improve and refine the search results.
All three windows can remain open but only one can be active.
Window position, size and other state variables are maintained across session thanks to the Persistent Storage Of GUI Preferences enhancement.

LOGICAL DATA FLOW

Here is how the Search Options with the Proof Worksheet and the Sorted Assertion List used by the Proof Assistant to produce Step Selector Search results.

Search Logical Data Flow Diagram

1. SELECT DOMAIN ASSRT: The Search Domain parameters are combined with the Proof Worksheet's theorem's location to build a list of Candidate Assertions using a Sorted Assertion List as input. The Sorted Assertion List (shown twice on the diagram) is also used in the Extended Search process and is sorted by Number of Hyps (not including VarHyps), ascending, and mObjSeq (sequence within the system, which is equivalent to order of appearance within the loaded .mm file -- which can be supplemented by the Theorem Loader feature that adds theorems after the initial load).

2. FILTER EXCLUDED ASSRT: The Exclusion Preferences are applied to the list of Candidate Assertions to generate an Assertion Search List. Must Be Unifiable With Step is one of the (default) Exclusion Preferences. "Completed Search Results" items have unifiable assertions whose hypotheses are fully satisfied by the Hyp field of the designated proof step (i.e. no missing Hyps) , and for these Search Result items the following occurs:

a) updated with the data necessary to update the Proof Worksheet, if requested; and
b) updated with high scores so that they appear first in the Sorted Search Results.

3. APPLY SEARCH CRITERIA: The Search Criteria are applied to the Assertion Search List to produce a Selected Assertion List of size not to exceed the Max Search Results option.

Also, if Max Search Results has not been exceeded when the Assertion Search List search is complete the remaining search results may be generated using the Search-Proximity Scoring option. If "On" it will add a non-zero score to Assertions not meeting the Search Criteria but which are in the same Section as (i.e. are near to) a selected Assertion; these Assertions will appear in the Search Results after Assertions that meet the Search Criteria.

4. FINALIZE SEARCH RESULTS: The Selected Assertion List is sorted according to the Output Sort Sequence option to generate the Search Results List.

5. EXTENDED SEARCH: If Extended Search is "On" and fewer than Min Completed Search Results have been found, the Extended Search Preferences are used to scan the Search Results List looking for assertions that are:

Unifiable but which have more hypotheses than were provided by the Hyp field of the designated proof step; and
Whose missing hypotheses can be satisfied by either

a) previous proof steps in the Proof Worksheet, or
b) existing assertions which require zero hypotheses (AKA, are "theorems" in the strictest Metamath terminology.)

Once found these assertions are:

a) updated with the data necessary to update the Proof Worksheet if requested; and
b) updated with high scores so that they appear first in the Sorted Search Results; and
c) resorted in the Sorted Results list.

6. AUTO-SELECT: If Auto-Select is "On" , the first Completed Search Result in the Search Results List is passed to the Proof Assistant to update the designated proof step in the Proof Worksheet, and if necessary, to generate hypothesis proof steps.

7. STEP SELECTOR SEARCH DIALOG: Displays the Sorted Results list. The user can can select a unifiable assertion from the Search Results List to update the Proof Worksheet, or return to the Search Options window to perform a new search or refine the current search.

8. SEARCH OPTIONS: The "Refine Search" button performs another search using new search criteria using the output Search Result List from the last search as input. Or, a New Search can be initiated, either for the designated proof step or as a unrelated (global )search. The user can also jump back to the Proof Assistant or back to the Step Selector Search dialog to re-view the most recent search results (Note: all windows can be open at the same time though only one can be active at once.)

9. PROOF ASSISTANT: A selected Search Result assertion can be used to update the designated proof step on the Proof Worksheet -- and if necessary, to generate missing hypothesis steps. Or, if no assertion was selected the Proof Worksheet is simply unified and re-displayed. New, reused and refined searches can then be initiated.

SEARCH DATA

____SEARCH_DATA____________ ||reset|| Text-Separators: OR: OR QUOTE: "
Search-In-What Format Oper Search-For-What Or
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X
|...............|+| |.........|+| |..|+| |XXXXXXXXXXXXXXXXXXXXXXXXXXXX|+| X

resetThe reset button resets the Search Data to the default settings.

The Search Data has three parts: Search Data Options fields, Search Criteria fields and the Search Domain fields.

SEARCH DATA OPTIONS fields:

OR

OR is a text entry field that enables you to specify how you will specify a logical "OR" operator in the Search-For-What field when multiple search terms are used in a Search-For-What field.
By default, multiple search terms are "AND"ed together.
Evaluation within a Search-For-What field is left-to-right, with evaluation stopping as soon as truth or falsity is determined -- e.g. evaluation of the terms to the right of an OR is not performed if evaluation of the terms to the left of the OR yields True.

QUOTE

QUOTE is a text entry field that lets you specify the character(s) you will use as quotation marks to delimit search terms in the Search-For-What field.
The default is the double-quote character, ' " ' .
Enclosing QUOTE characters are required if a search term contains embedded blanks.
Enclosing QUOTE characters are required for Format types RegExpr and CharString if you wish to the search term to be applied to a character string version of the Search-In-What content instead of searching each non-whitespace token individually; this consideration does not apply to Format types ParseExpr and ParseStmt since they are searching formula parse sub-trees and parse trees, respectively.

SEARCH CRITERIA fields:

Search Criteria Line Data: Search-In-What, Format, Oper, Search-For-What and Or: Up to four lines of search criteria data may be entered. By default the search criteria lines are "AND"ed together, but you can toggle-on the Or field on a line to indicate that the next line is to be "OR"ed with it.

Evaluation of the array of search criteria lines and the individual search terms in a Search-For-What field proceeds from top-to-bottom, then left-to-right. To simplify input, the pulldown lists are linked in a hierarchy: when a Search-In-What list item is selected the contents of the Format and Oper pulldown lists are updated to reflect only the valid choices. IMPORTANT NOTE: The PrevSearchData menu lets you select any of the nine sets of Search Criteria line used in previous searches -- or a reset of the search criteria lines to the default state (empty).

Search-In-What lets you choose what part of the Metamath assertion statements to search, such as "Formulas($a$e$p)". See: Table: Valid Combinations of Oper, Search-In-What and Format.

Formatspecifies the structural view of the data applied in the search comparisons. For example, each formula is stored in mmj2 as a parse tree and as a list of non-whitespace tokens; for search purposes a character string can be constructed from a list of non-whitespace tokens with a single blank character between each token.)

ParseExpr and ParseStmt employ parse trees and are applied to formula parse sub-trees and parse-trees, respectively. Enclosing QUOTE characters are required if more than one search term is entered in the Search-For-What field because most formulas and expressions contain space characters.
CharString uses a case-insensitive character string comparison -- if enclosed in QUOTE characters the Metamath object's character string taken as a whole is searched for a match, otherwise it is applied to the character string of each Metamath token in the object;
RegExpr uses the Java-defined version of Regular Expressions (see also http://docs.oracle.com/javase/tutorial/essential/regex/index.html ) -- if the RegExpr is enclosed in QUOTE characters the Metamath object's character string taken as a whole is searched for a match, otherwise it is applied to the character string of each Metamath token in the object.
See: Table: Valid Combinations of Oper, Search-In-What and Format.

Oper lets you specify relational operators for the Format types ParseExpr and ParseStmt, and boolean operators (blank or "not" ) for all other Format types.

Table: Valid Combinations of Oper, Search-In-What and Format:

Search-In-What(Rows)/ Format(Columns) Oper(Cells)	ParseExpr	ParseStmt	CharString	RegExpr
Formulas($a$e$p) -- Axiom, Logical Hypothesis and Provable Assertion Formulas	< > <> ==	< > <> ==	blank not	blank not
Formulas($a$p) -- Axiom and Provable Assertion Formulas	< > <> ==	< > <> ==	blank not	blank not
Formulas($e) -- Logical Hypothesis Formulas	< > <> ==	< > <> ==	blank not	blank not
Comments($( $)) -- Comments preceding Axiom and Provable Assertion statements.	n/a	n/a	blank not	blank not
Labels($a$e$p) -- Axiom, Logical Hypothesis and Provable Assertion Labels	n/a	n/a	blank not	blank not
Labels($a$p) -- Axiom and Provable Assertion Labels	n/a	n/a	blank not	blank not
Labels($e) -- Logical Hypothesis Labels Labels	n/a	n/a	blank not	blank not
Labels(RPN $=) -- Lists of Labels in RPN order comprising a Metamath proof;	n/a	n/a	blank not	blank not

Search-For-What is used to enter one or more search terms in a given Format.

Multiple search terms are evaluated individually and the results are "AND"ed together unless you use the text separator OR characters between search terms.
Evaluation within the Search-For-What field is left-to-right, with evaluation stopping as soon as truth or falsity is determined -- e.g. evaluation of the terms to the right of an OR is not performed if evaluation of the terms to the left of the OR yields True.
Spaces are used to first parse the Search-For-What contents into individual search terms and OR separators. Therefore...
Enclosing QUOTE characters are required if a search term contains embedded blanks. For example, with Search-In-What = Comment and Format = CharString, then "in a set" without enclosing QUOTE characters is interpreted as three separate search terms, and the search process will be applied to each Comment token for each search term.
For Format types RegExpr and CharString, Enclosing QUOTE characters are required if you wish the content to be processed all-at-once as a single character string. Comments, Formulas and RPN-format Proof Label lists are stored in mmj2 as lists of non-whitespace tokens which can be processed individually, one-at-a-time, for each search term -- or, if you have enclosed your search term with QUOTE characters, the token list is internally converted into a character string consisting of the tokens with a single blank character in between each token. (The problem of whole vs. by-parts search is solved for formula parse trees by using two different Format types: ParseStmt and ParseExpr, the former using a whole parse tree search and the latter using a search of all parse sub-trees.)
Example: with Search-In-What = Formula and Format = RegExpr, ' "equ*" OR "num*" ' consists of two regular expression search terms, and the search process will be applied to each formula's character string as-a-whole for each search term.
Search terms are validated according to Format prior to conducting the search. Errors, such as an invalid RegExpr, or a parse error in a ParseExpr or ParseStmt produce an error message.
A pull-down list provides the nine most recently searched values of Search-For-What for the Format in use on the line.

Or Toggle-on to indicate that the next line is to be "OR"ed with the line.

The default logical operator for the array of search criteria lines is AND.
Evaluation of the array of search criteria lines is top-to-bottom with evaluation stopping as as soon as truth or falsity can be determined.

FORMAT Types:

ParseExpr and ParseStmt

These formats refer to the parse trees stored by mmj2 for each formula. When ParseExpr is specified a formula's parse tree is (unification) searched looking for a matching sub-tree (including the tree as a whole); these may be of any Metamath syntax Type (e.g. in set.mm, excluding the MathBoxes, the valid syntax Types are wff, set and class.) ParseStmt refers to an entire formula parse tree, and of course, when searching set.mm it must always be a "wff" (or whatever Provable Logic Statment Type is used by the .mm file.)

Operators <=, <, >=, >, =, ==, <>, and NA may only be applied to the ParseExpr and ParseStmtFormats. They refer to the relationships between formulas as defined by the unification operation applied to an assertion's formulas' parse trees/sub-trees and the parse tree generated for the Search-For-What field (((This may seem to be a trifle complicated but the actuality is simpler than the explanation...)))

Table: ParseExpr and ParseStmt Oper Values:

Oper	Meaning (X refers to Assertion Formula)	X	Oper	Search-For-What
<=	Search-For-What is InstanceOf X	( ph -> ps ) ph ( ph -> ps ) &W1	<= <= <= <=	( ps -> ch ) ( ps -> ch ) &W1 ( ps -> ch )
<	Search-For-What is StrictInstanceOf X	ph	<	( ps -> ch )
>=	X is InstanceOf Search-For-What	( ph -> ps ) ( ph -> ps ) ( ph -> ps ) &W1	>= >= >= >=	( ps -> ch ) ph &W1 ( ps -> ch )
>	X is StrictInstanceOf Search-For-What	( ph -> ps )	>	ch
=	X and Search-For-What are InstanceOf each other (i.e. equal, except for variable names)	( ph -> ps )	<>	( ch -> th )
==	X is IdenticalTo Search-For-What	( ph -> ps )	==	( ph -> ps )
<>	Search-For-What is strictInstanceOf X or X is StrictInstanceOf Search-For-What	ph ( ps -> ch )	<> <>	( ps -> ch ) ph
NA	Search-For-What is N/A X	( ph -> ps )	NA	( ph <-> ps )

CharString

The CharString Format employs a case-insensitive search for each search term within the character string view of the Search-In-What content.
Enclosing QUOTE characters are required if a search term contains embedded blanks.
Enclosing QUOTE characters are also required if you want one search of the Search-In-What content taken as a single character string. Otherwise the search is performed against each non-whitespace token in the content. For example: you search for "ph" within the formula character string "( ph -> ( ps -> ph ) )" or you can search for ph within the individual tokens: "(", "ph", "(", "ps", "->", ")", ")".
Metamath tokens are stored internally by mmj2 as lists of non-whitespace tokens and whitespace tokens. Since the content of the non-whitespace tokens may contain spaces, tabs, new-line characters and carriage-return characters, when creating a character string for searching, mmj2 internally creates a character string consisting of the non-whitespace tokens with a single blank character in between each token. This is done for Formulas, Comments and RPN Proof Label lists, all of which can be searched using the CharString Format.

RegExpr

RegExpr is very similar to the CharString Format except that it uses the Java-defined version of Regular Expressions (see also http://docs.oracle.com/javase/tutorial/essential/regex/index.html ) instead of a case-insensitive character match -- the Search-In-What content is still viewed as character strings, so the same considerations about enclosing QUOTE characters applies:
If the RegExpr is enclosed in QUOTE characters the Metamath object's character string taken as a whole is searched for a match, otherwise it is applied to the character string of each Metamath token in the object. For example: you search for "p*" within the formula character string "( ph -> ( ps -> ph ) )" or you can search for p* within the individual tokens: "(", "ph", "(", "ps", "->", ")", ")".
Metamath tokens are stored internally by mmj2 as lists of non-whitespace tokens and whitespace tokens. Since the content of the non-whitespace tokens may contain spaces, tabs, new-line characters and carriage-return characters, when creating a character string for searching, mmj2 internally creates a character string consisting of the non-whitespace tokens with a single blank character in between each token. This is done for Formulas, Comments and RPN Proof Label lists, all of which can be searched using the RegExpr Format.

SEARCH DOMAIN fields:

From Chap |.....................|+| Sec |..............................|+|
Thru Chap |.....................|+| Sec |..............................|+|

From Chap/Sec and Thru Chap/Sec These pulldown lists are used to specify the start and end of the range of related Chapters and/or Sections used to restrict the search domain. The default setting is from the first Chapter/Section of the loaded Metamath file thru the Chapter/Section of the Theorem being proved on the Proof Assistant -- though never to include the Theorem itself, or subsequent assertions; or if the Theorem is new and LOC_AFTER was used then up thru the LOC_AFTER statement but none of the subsequent assertions. The user may alter the From and Thru Chapter/Sections, but Thru must not be past the Theorem being proved. If a new From/Thru range is input then the search domain includes the From/Thru Chapters and/or Sections plus the Chapter or Section of the Theorem being proved -- this last detail allows for Mathbox users to add their theorems to the search domain along with a From/Thru range. Finally...From/Thru Sections may be left blank, in which case the granularity of the range is the Chapter level; otherwise granularity is set to the Section level.

About Metamath Chapters and Sections:

Metamath Chapters are denoted by special Comment lines like this:

$(
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
Propositional calculus
#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#*#
$)

Metamath Sections are denoted by special Comment lines like this:

$(
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Recursively define primitive wffs for propositional calculus
=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
$)

mmj2 captures the Chapter/Sections by default, unless the following RunParm command is input:

BookManagerEnabled,no

mmj2 defines a Section relationship as the use by one Section of another Section's math objects -- symbols and statements. Specifically, a proof reference to an assertion (logic or syntax) defined in another Section is considered "use" of that Section. In addition, a statement's formula's use of symbols defined in another Section is considered "use" of that Section.

mmj2 Chapter relationships are computed from the Section relationships via set union operations: A Chapter is related to the set of Chapters of the Sections to which it is related.

You can see the mmj2 Chapter/Section data by inserting the following RunParm commands into your RunParms.txt file:

PrintBookManagerChapters

*PrintBookManagerSections

*PrintBookManagerSectionDetails,*

Note that mmj2 breaks down each Metamath Section into four sections: Symbols, VarHyps, Syntax and Logic. For Search Option usage we will treat all four "sub-sections" as a unit. To convert the mmj2 Section numbers into indexes we do an integer divide by 4 and discard the remainder.

Here are Chapter/Section lists from mmj2 after some text-editing to remove extraneous data:
Chapters.txt
Sections.txt

SEARCH PREFERENCES

____SEARCH PREFERENCES_____ //reset\\
Exclusion: Labels: XXXXXXXXXXXXXXXXX Extended Search:
   99999 Min Times Used In Proofs     99999 Min Completed Search Results
   99999 Min Hyps                     99999 Check First N Search Results
   99999 Max Hyps                     99999 Max Incomplete Hyps
   99999 Max Search Results 99999 Max Prev Steps Checked
       X Must Be Unifiable With Step      X Reuse Derivation Steps
       X Use Chapter/Sec. Hierarchy      Output:
       X Search-Proximity Scoring     99999 Max Elapsed Seconds
                                          X Show Unification Subst.
                                            X Auto-Select (Update Proof Step)
   Output Sort Seq: |.....................................................|+|

reset The reset button resets the Search Preferences to the default settings.

The Search Preferences area has three sections: Exclusion Preferences, Extended Search Preferences and Output Preferences.

EXCLUSION PREFERENCES - These are search criteria which remain in force until changed by the user. The name, "Exclusion" is somewhat of a misnomer since only Labels and Max Search Results cause exclusion of an assertion from the Search Results if satisfied; the rest cause exclusion if not satisfied; the most important characteristic to remember is that unlike the Search Data criteria, the Exclusion Preferences remain in force from one search to the next until changed or reset.

Labels

Labels is a text entry field that uses regular expressions to specify the labels of assertions that should be excluded from the Search Results.
Multiple regular expressions are input using spaces as delimiters (e.g. 3* *OLD ee* ).
Uses the Java-defined version of Regular Expressions (see also http://docs.oracle.com/javase/tutorial/essential/regex/index.html ).
Note: this functionality of Labels is almost identical to specifying a Search Data line with Search-In-What = Labels and Format = RegExpr. The reason for providing the Labels field here is that Search Preferences area do not need to be re-entered for each new search, unlike Search Data.
Default = blank.

Min Times Used In Proofs

Excludes any assertion which is referenced by fewer than Min Times Used In Proofs times.
However, assertions in the designated theorem's own Section are not excluded for this reason.
Must be 0 thru 99999.
Default = 0.

Min Hyps and MaxHyps

Excludes any assertion with fewer than or greater than Min Hyps and Max Hyps logical hypotheses, respectively.
Must be 0 thru 99999.
Default = 0 and 99999, respectively.
Note: the input Sorted Assrt List is sorted by Number Of Hyps and mObjSeq number. Skip-sequential processing is used in the search to access the list very efficiently. Also, please note that the Extended Search process first looks for assertions with 1-missing Hyp, then 2-missing Hyps, etc. So, it is possible to reduce the search elapsed time significantly by specifying Min Hyps and Max Hyps, especially if you are using Extended Search. If your searches are taking too long or are timing out (re: Max Elapsed Seconds) -- you can efficiently break up a search into ranges of Hyps: e.g. 0 thru 2, 3 thru 3, 4 thru 4, etc. Something like 95% of assertions in set.mm use 2 or fewer Hyps...AND...the assertions with larger numbers of Hyps are the ones most likely to cause the dreaded Combinatorial Explosion of Possibilities resulting in a timeout.

Max Search Results

Limits the size of the Search Results List.
Must be 0 thru 99999.
Default = 99999.

Must Be Unifiable With Step

Checkbox field; default = On (checked).
If On, then an assertion which is not unifiable with the designated proof step is excluded from the Search Results.
Does not apply and is ignored if a non-step specific or global (non-theorem) search is requested.
Note: this is one of the most powerful criteria in the Search Options toolbox because in a deep sense, unifiability signifies similarity: in order for an assertion to be unifiable with a proof step and its Hyp fields, the proof step must be an instance of the assertion and its Hyps.

Use Related Chapter/Section Hierarchy Toggle On to specify that the search domain is to be restricted to a hierarchy of related Chapters and/or Sections of the input Metamath file -- plus the Chapter or Section of the Theorem being proved -- this last detail allows for Mathbox users to add their theorems to the search domain along with a From/Thru range.

Related Chapter/Section Hierarchy Diagram

Search-Proximity ScoringToggle-on to indicate that:

If an assertion is not excluded (according to the Exclusion Preferences) AND
It is not selected by the Search Criteria (and Search Criteria were used), AND
The assertion is in the same Section as an assertion that was selected (and not excluded), THEN
Assign the assertion a non-zero search score such that it will appear in the search results but after all assertions that were selected.

EXTENDED SEARCH PREFERENCES

"Extended Search" is a potentially computationally expensive process that looks for missing hypotheses -- those not specified by the user in the Hyp field of the designated proof step -- among the previous proof steps and zero-hypothesis theorems of the system (the latter is performed for assertions in the Search Results that require exactly one hypothesis.)
In some rare cases, when the user specifies sufficient hypotheses in the Hyp field of the designated proof step, Completed Search Results will be found during the initial search. Only when the user used a "?" in the Hyp field (e.g. "?", "1,?", "1,2,?", etc.) does Extended Search even come into play.
The main challenge for Extended Search is "Combinatorial Explosion of Possibilities". This will typically occur with long proofs where the designated proof step is at the end, and/or for assertions with more than two missing hypotheses.. Hence the Output Preference Max Elapsed Seconds.
To improve the odds of finding one or more Completed Search Results prior to Max Elapsed Seconds, the Extended Search scans the Search Results multiple times. First the one-missing hypothesis Search Results assertions are examined, then two-missing hypothesis assertions, and so on. Additionally, for the one-missing hypothesis assertions, if no previous proof step was found to be satisfactory a special search is made looking for existing zero-hypothesis assertions that unify with the missing assertion hypothesis (given simultaneous variable substitutions obtained from the step's unification with the Search Result item's assertion.)
NOTE: it is conceivable that a user might want the option to have the Search Results checked in sequence without regard for the number of missing hypotheses. That option could be added to the Extended Search Preferences without undue difficulty -- though the problem of Combinatorial Explosion of Possibilities may reduce the appeal of this option.
Extended Search is N/A for global searches or non-step specific searches.

Min Completed Search Results

Sets the minimum number of Completed Search Results.
An Extended Search only takes place if additional Completed Search Results are needed to equal the Min Completed Search Results number following the initial search.
Must be 0 thru 99999.
Default = 0 = Extended Search is OFF

Check First N Search Results

Specifies the endpoint in the Search Results to be checked in the Extended Search.
Must be 0 thru 99999.
Default = 99999
Note: the result to set this value (much) lower would be to shorten the elapsed time -- Extended Search is computationally expensive, especially for long proofs using assertions with > 2 hypotheses.

Max Incomplete Hyps

Specifies the maximum number of the incomplete hypotheses in Search Result items to be checked in the Extended Search.
Must be 0 thru 99999.
Default = 99999

Max Prev Steps Checked

Specifies the maximum number of the previous proof steps to be checked in the Extended Search.
This number does not include previous steps that are bypassed because Reuse Derivation Steps is Off.
Must be 0 thru 99999.
Default = 99999

Reuse Derivation Steps

Checkbox field; default = On (checked).
If Off, previous proof derivation steps (this excludes the theorem's hypotheses) which have already been referenced in a prior derivation step will not be checked in the Extended Search.
The idea of this is to dramatically reduce the number hypothesis combinations tested during unification of the Search Result item's assertion. For long proofs the problem of Combinatorial Explosion of Possibilities may be dramatically reduced if Reuse Derivation Steps = Off.
Because some proofs do require reuse of derivations, the user can input a special mmj2 Proof Worksheet Comment statement immediately prior to the designated proof step that specifies "<SO:REUSE>" as the first non-blank token after the "*" in column 1. This special comment designates the following derivation step as a candidate for reuse even though Reuse Derivation Steps = Off.

OUTPUT PREFERENCES

Output Sort Sequence

The Output Sort Sequence uses a pulldown list that allows the user to select the sort sequence of the output Search Results List.
The sort key field choices are listed in major to minor order. (Minor sort keys only come into play if all of the more major sort keys are equal when two items are being compared.)
If not otherwise mentioned, field sort sequence is Ascending order. Descending order is indicated with "(D)" suffixing the field name.
Note: Unless Must Be Unifiable With Step is Off, every Search Result List item assertion will be unifiable with the designated proof step (proof step formula/hyps are an instance of the assertion). So, we already know that the proof step is very similar to each of assertions! The purpose of the sort sequence is to put the Search Result items the user is most likely to want at the beginning of the Search Results List.

SORT KEY FIELDS TABLE

MObjSeq	Metamath Object Sequence Number: corresponds to position within the input Metamath file. A higher number indicates a more advanced assertion which may be more desirable in a proof step.
Nbr Hyps	Number of Logical Hypotheses in assertion. Fewer hypotheses tends to result in shorter proofs. Approximately 95% of set.mm assertions have two or fewer hypotheses.
Complexity	Combination of two Sort Key fields: ParseDepth and Formula Length. Combined here to simplify usage and documentation. "Complexity(D)" means ParseDepth(D) followed by FormulaLength(D).
ParseDepth	= Assertion's conclusion's formula's parse tree depth. Corresponds roughly to formula complexity and hence, specificity. Because in standard practice the designated proof step has already been unified with each assertion in the Search Results List, a greater Parse Depth corresponds to a higher degree of similarity -- and hence, increased likelihood of usefulness in the designated proof step. `See mmj.lang.Stmt.getExprParseTree().getMaxDepth().`
FormulaLength	= Assertion's conclusion's formula length (in tokens, not characters). Corresponds roughly to formula complexity.
Popularity	= Number of times assertion used in proofs of other assertions.
Score	This is a ranking number based on the search results and search preferences/criteria: 000 = Assertion not selected (initial Score value) 030 = Assertion excluded 030 = Assertion not excluded, but also not selected 040 = Assertion selected by virtue of Search-Proximity Scoring 050 = Assertion satisfies search criteria, if any, but is not a Completed Search Result. 100 = Assertion is a Completed Search Result: it unifies with the designated proof step and there are no missing hypotheses.

SORT SEQUENCE TABLE

SORT ID	Default Sort?	1	2	3	4	5
1	Yes	Score(D)	Complexity(D)	Popularity(D)	Nbr Hyps	MObjSeq(D)
2		Score(D)	Popularity(D)	Complexity(D)	Nbr Hyps	MObjSeq(D)
3		Score(D)	Nbr Hyps	Complexity(D)	Popularity(D)	MObjSeq(D)
4		Score(D)	Nbr Hyps	Popularity(D)	Complexity(D)	MObjSeq(D)
5		Score(D)	Complexity(D)	MObjSeq(D)
6		Score(D)	Popularity(D)	MObjSeq(D)
7		Score(D)	Nbr Hyps	MObjSeq(D)
8		Score(D)	MObjSeq(D)

Max Elapsed Seconds

Specifies the maximum number the search is allowed to run.
A helpful "timeout" message provides the progress of the search at the time it was terminated.
Must be 0 thru 99999.
Default = 2.

Show Unification Substitutions

Checkbox field, check = On.
On = default = Unifiable assertions are displayed in the Step Selector Search Dialog with the unification substitutions (from the Proof Worksheet into the assertion).
Off = Assertion formulas shown without substitutions as they exist in the input Metamath database.

Auto-Select (Update Proof Step)

Checkbox field, check = On.
Off = default
If Auto-Select is "On" , the first Completed Search Result in the Search Results List is passed to the Proof Assistant to update the designated proof step in the Proof Worksheet, and if necessary, to generate hypothesis proof steps...followed by Unification of the Proof Worksheet.
"Completed Search Result" items have unifiable assertions whose hypotheses are fully satisfied by the Hyp field of the designated proof step -- i.e. no missing Hyps. For example, the assertion is ax-mp and it is unifiable with theorem XYZ step 3 for which either the user specified Hyp field "1,2" (or "2,1", or "1,2,?", etc.) -- OR... the Extended Search feature discovered Steps 1 and/or 2 as suitable hypotheses for ax-mp, in which case the user could have specified the Hyp field as simply "?" (or "1,?", or "2,?", or "?,1", or "?,2").
The Step Selector Search Dialog will be updated with the new Search Results list even though Auto-Select is activated and the Proof Worksheet is automatically updated. Assuming that the user has a large screen capable of displaying the Proof Assistant GUI and the Step Selector Search Dialog simultaneously, both windows will be updated and visible as a result of the successful search + Auto-Select activation. Following successful update of the Proof Worksheet, the Proof Assistant GUI window will be the "top" window and will have the active cursor.

Search Options

Contents

SEARCH OPTIONS WINDOW

SCREEN FLOW

LOGICAL DATA FLOW

SEARCH DATA

SEARCH PREFERENCES

SEARCH OPTIONS WINDOW

SCREEN FLOW

LOGICAL DATA FLOW

SEARCH DATA

SEARCH PREFERENCES