Proof Validation

[OneManEquipe]

Persistent KnowledgeBases allow for a nice trick: loading them and then validating their content.

This requires saving proofs instead of formulas, and then, the next time the application starts, the premises for such proofs are checked against the current "new axioms", so that they are "incrementally adjusted": only those with changed premises are removed, and the others are kept.

There are a few important points:

• as stated above, proofs must be stored in the kb instead of formulas
• some provers might be "impure", meaning that even if the premises hold, there is no guarantee that the conclusions are still true (e.g. from IsProjectRootPath(somePath) a listener might prove as a consequence that the files in the project have some content, but there is no guarantee that next time, if the path is still the same, the conclusions (about the content of the files) are still valid). this will be a further issue (I already wrote a note)
• in order to check if the conclusions are still valid we must also check that we still have the same provers/listeners or something like that

This still needs further analysis before coding!

NOTE: I'm not so sure anymore that proofs should be saved INSTEAD of formulas: I could save it as an extra. Also, what if a proof is based on hypotheses?