Support finding relevant facts and definitions

[muenchnerkindl]

The prover requires users to list all facts to be used and all definitions to be expanded for the proof of a step, either through USE directives that remain in effect throughout their scope or directly in the BY clause justifying the step. This helps control the search space for automatic proof backends, but it can be tedious for the user to remember all relevant facts and to figure out what may be missing just from staring at a large proof obligation.

It would therefore be useful to have an assistant capable of suggesting relevant facts and definitions. A first possibility would be to launch backend provers repeatedly while adding more and more facts and definitions that are available in the context. (Obviously, only definitions of operators that appear in the proof obligation need to be expanded.) A more ambitious approach could analyze the proof obligation in order to identify possibly relevant facts, perhaps taking into account the capabilities and limitations of the backend to be used. For example, pure first-order provers are good at handling quantified formulas, whereas SMT solvers can reason about arithmetic.

Once an obligation has been proved successfully, the facts and definitions used for the proof should be recorded so that they remain available for subsequent launches of the prover.

[lemmy]

@muenchnerkindl Do you expect AI (LLMs) to play a role in this project?

[muenchnerkindl]

I believe that purely symbolic techniques could go a long way here, but experimenting with LLMs may be interesting. Not sure if we have big enough data sets to have a chance of getting good results.