Tracker for HOL features merged to master

[mezpusz]

General:

• HOL unification
• HOL matching
• SMTLIB2 parsing for lambdas and applications.

Preprocessing:

• CNF
• Function definition elimination
• Functional extensionality axiom
• Choice axiom
• Proxy axioms
• Heuristic instantiations?

Inferences:

• ArgCong
• BetaEtaISE
• BoolEqToDiseq
• BoolSimp
• Cases
• CasesSimp
• Choice
• LazyClausification
• LazyClausificationGIE
• EagerClausificationISE
• IFFXORRewriterISE
• ElimLeibniz
• FlexFlexSimplify
• Injectivity
• NegativeExt
• PositiveExt
• PrimitiveInstantiation
• ImitateProject?

Inferences that need adjusting:

• Superposition
• Demodulation
• Subsumption
• Definition introduction
• URResolution

Which inferences are incompatible with HOL?
Proof checking for HOL?

Issues:

• Fix order of arguments for app, arrowSort, lambda calls and scrutinize every call site.
• Consider replacing EqHelper::replace with SubtermReplacer that can shift DB indices if needed.
• Make all binders compatible with HO matching (no loose DB indices can be bound).
• Appify in some preprocessing step if problem is higher-order and there are non-applied constructs in it (e.g. coming from SMTLIB2.7).

[mezpusz]

@ibnyusuf do you have some intuition which axioms (choice, functional extensionality, proxy) are actually needed and which ones are handled better by the corresponding inferences? Based on some preliminary experiments comparing the current master with the HOL branch, there is some indication that the choice axiom is still needed, while the other two seems to be handled better by the inferences.

[ibnyusuf]

@ibnyusuf do you have some intuition which axioms (choice, functional extensionality, proxy) are actually needed and which ones are handled better by the corresponding inferences? Based on some preliminary experiments comparing the current master with the HOL branch, there is some indication that the choice axiom is still needed, while the other two seems to be handled better by the inferences.

That roughly matches my recollection. Choice is definitely required to solve some problems. Functional extensionality may help for a few odd TPTP problems, but in general can be handled via inference. Proxy axioms are almost always useless.

[mezpusz]

Thanks a lot, this simplifies merging a bit!