XPlain

Translator for Prover9 proofs. 

Computer proofs are usually very difficult to follow and understand. This tool accepts Prover9 proofs (in the expanded format) and a particular proof line, and outputs a humanized proof. It will be a package for ProverX. 

Produced with José Duarte and Michael Kinyon.