Recently Ohad made significant progress in Github by implementing a proof extraction which allows negation. This is something I didn't even think was possible but apparently the code is beginning to work. Some are now asking what proof extract is and why it's so important. I'm ready to dive into the "what is proof extraction" rather than "why is proof extraction necessary". It would seem for those technically inclined that proof extraction is necessary for an optimization purpose because BDDs seem to require this step, but I'm not intimate with the code base to give the precise reasoning as to why Ohad is making that decision other than from an observer making an educated guess.
To understand what proof extraction is we first need to understand what a proof tree is. A proof tree is a sort of data structure while a proof extraction is a sort of compressed representation of the data within a proof tree. A proof tree is like a propositional logic tree for those who would like to try and visualize.
Useful quote:
The idea here is that a proof is a finite tree. Each node of the tree is labelled by some assertion, and the proof is a proof of the assertion at the bottom-most node (which is the root of the tree, so these trees are drawn upside down compared to the trees in Chapter 1 of The Mathematics of Logic, or if you prefer the right way up compared to real biological trees). The pre-conditions required to make a proof step are the labels of the immediately preceding node or nodes, and there will be finitely many of these.
One of the key points in this quote is that a proof can be represented as a "finite" tree. TML and in specific Tauchain is based on partial fixed point logic which can deal with finite rather than infinite. Binary decision diagrams or BDDs are efficient means of representing the data in a way which is more friendly to computer processing, but these BDDs seem to be in a compressed form. That is there could be information which might be lost (don't quote me on this because I'm no expert), but this lossiness possibility could be why proof extraction becomes a necessary step.
So if we know BDDs have proofs in them then we would need a way to extract them as necessary for certain optimizations or processing tasks. Proof extraction would then be a method of extracting proofs or "proof trees" from a BDD. BDD for those who need a refresh are binary decision diagrams which essentially contain the same kind of data as proof trees but in a different form, and this data must be extracted to be translated or transformed or used for something else.
Proofs can be thought of as logic programs, more specifically TML programs. If there are more questions about this I can work on a follow up post and additionally you can directly ask Ohad for the next Monthly update Q/A.
References
