Store proofs instead of expressions

[OneManEquipe]

So... currently we have an ExpressionStorage class which stores Expressions :P

But in order to allow for proof validation (#10 ) we need the proofs to actually be persisted, or we wouldn't have anything to validate at startup-time.

So, how should we do this?

Ideas so far, pretending we have a graph db:

• we define a new ProofStorage, with an API similar to ExpressionStorage
• it should also support ponderings
• when we store a proof/pondering, we store all expressions in it as nodes, associated with a boolean named explicitlyAdded
• the conclusion of the proof has explicitlyAdded=true, all other expressions have false (I don't know why, but this seems like a useful piece of information)
• metadata on each proof should also be stored, such as a version number/timestamp or anything that allows to know which proof was before which other
• for each step in the proof we also store that as a node, with the inference rule name, a reference to the proof metadata and the step substitution
  • to allow for this I'll need to give a unique name to each inference rule in a KnowledgBase
• of course, we add arcs going from premises to steps and from steps to conclusions

This should allow for efficient storage of proofs, since expressions are stored only once (without duplicates).

---

As a bonus, can this be taken to the extreme?

For example, suppose we have a predicate HasTruth such that HasTruth(P, x) where P is a proposition and x a value between 0 and 1 (think fuzzy logic). If two proofs determine Animal(dylan) with different values for x, the two expressions would be distinct, just for a tiny difference.

So... what if we write every term as a node and link them with arcs? This would allow complete reuse.

On the other hand, I don't think it would be worth it (performance would be slower, and formulas might be mostly small), so here is my proposal:

• I'll think about it in the context of this issue, if it seems reasonable, I'll either do it or open an issue for it
• it might be still useful to provide some special way of saving wrapped objects, since they can be huge (for example an image)