List of plans and suggestions for future MpTP versions

New functionality

Learning support

• add arities to constr_names.pl for easy printing into E_KNOWLEDGE/signature
• recommend scheme instances, fraenkel instances and top-level non-theorem lemmas for new proofs too (means including them in learning)

Reproving support

• for Mizar proofs, try to determine which references are needed on the top-level provided that all lemmas are treated as proved. This way when we find the proofs of lemmas (and thus the references needed for them), we can just merge the top-level references with the lemma references, and hopefully have cut a lot of unnecessary background.
• translate the ND proofs into reasonable TSTP

Improved presentation - not strictly needed

• use the pid attributes for reconstruction of original logical connectives as in the HTML rendering; this would probably require some fixes for handling of logical connectives in utils.pl
• human friendly names for Mizar symbols? To do this completely manually would be a lot of work since there are ca. 10000 symbols in Mizar. Unless something clever is designed, a lot of that work would be wasted when MML changes. One unsuccessful attempt to push something a bit clever into MML is at http://mizar.uwb.edu.pl/forum/archive/0309/msg00000.html (that's more than two years old now), I should keep trying though. See NiceConstructorNames for renewed effort.

Fixes

Mizar-related fixes

• possible fixes for changed Pattern position in recent Mizar XML in mizpl.xsltxt
• in diffuse reasonings replace the lowercluster with uppercluster when "take" is used

Fixes for the algorithm adding background info

• prune more existential clusters if possible: (the first two can probably be done by a smart clausifier, see the article appended to MoMM)
  • only add the strongest, then ignore the weaker ones (i.e. prune "ex X relation(X)", if adding also "ex X relation(X) & function(X)"
  • try to prefer the constructive versions which subsume the existential statements, i.e. prefer "relation({})" to "ex X relation(X)"
  • when adding existential clusters, only consider the "main attribute" in them; i.e., if symbol "relation" was added, only add "ex X relation(X)", do not add "ex X relation(X) & function(X)" too

TpTP compatibility fixes

• check that the new handling of dollar in TpTP ($true is now atom) works
• remove the empty existential quantification in t2_gate_1 for the fraenkel def

Fix of the scheme_instance slot in mizar_from inference

Currently this is:

[scheme_instance (scheme_instance_name, original_scheme_name,
  current_item_name, file_name, second_order_substitutions)]

[symbol_1/term_or_formula_1,...,symbol_n/term_or_formula_n)]

suggested TpTP-compatible format is:

[ scheme_instance_name, original_scheme_name, 
  current_item_name, file_name,
  symbol_1, term_or_formula_1,...,symbol_n, term_or_formula_n].

It's a bit fragile, I'd prefer to have the second_order_substitutions packed in one term or list, because now I'll have to remember that the substitutions start at position five in the list, and if I add some metainfo to its beginning, things will break. But I can live with this. Another option are HOL extensions to TpTP, should be explored.

-- JosefUrban - 19 Feb 2006