José Duarte

XPlain2 – A code odissey

Prover9 is the offspring of a automated theorem prover family for first order logic with equality that started with ”Otter” and ”EQP”. It is a widely used math tool but its outputs are cumbersome and difficult to understand. Xplain2 is a translator that intends to give a much more pleasent and comprehensible version of the proofs generated by Prover9 while trying to close the gaps between some holes left by its ancestor, the former Xplain. This presentation is going to provide a bird’s eye view over the work in progress on this translator, looking at several aspects that influenced the code decisions taken so far through the illustration of a few obvious, or not quite so, selected cases.