[Matryoshka-devel] Paper draft

Haniel Barbosa haniel.barbosa at inria.fr
Tue Feb 21 21:43:26 CET 2017


I would like to share with you the draft of a paper we are gonna submit to CADE:

    An Efficient Proof-Producing Framework for Formula Processing
    Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine

The paper is about a framework for generating detailed proofs of some processing
transformations (let elimination, skolemization, rewritings) while being
efficient and easy to implement. We show the proof calculus in which it is
based, the algorithms to do the processing, their correctness and how things
were implemented in veriT and in a proof of concept checker in Isabelle.

Comments welcome, before or after the deadline (25 February).

Haniel Barbosa

More information about the matryoshka-devel mailing list