Propositional logic decision procedures lie at the heart of many applications in hard- and software verification, artificial intelligence and automatic theorem proving. In many practical applications it is not sufficient, however,to obtain a yes/no answer from the decision procedure. Either a model, representing a sample solution, or a justification (i.e. a proof), why the formula possesses none, is required.

In this talk I will demonstrate the use of powerful proof systems (e.g. Extended Resolution) as a unifying means to compactly and concisely represent propositional logic proofs obtained from the application of different Boolean logic algorithms (e.g. Davis-Putnam, Binary Decision Diagrams).