Walking through the Forest: Fast EUF Proof-Checking Algorithms

Second International Workshop on Proof Exchange for Theorem Proving

Frederic Besson ; Pierre-Emmanuel Cornilleau ; Ronan Saillard

Others  :  http://ceur-ws.org/Vol-878/paper5.pdf
PID  :  43477

来源: CEUR

【 摘 要 】

The quantier-free logic of Equality with Uninterpreted Function symbols (EUF) is at the core of Satisability Modulo Theory (SMT) solvers. There exist several competing proof formats for EUF proofs. We propose original proof formats obtained from proof forests that are the artifacts proposed by Nieuwenhuis and Oliveras to extract eciently EUF unsatisable cores. Our proof formats can be generated by SMT solvers for almost free. Moreover, our preliminary experiments show that our novel veriers outperform other existing EUF veriers and that our proof formats appear to be more concise than existing