Sana Stojanovic Durdevic, Julien Narboux, Predrag Janicic. Automated generation of machine verifiable and readable proofs: A case study of Tarski's geometry. Annals of Mathematics and Artificial Intelligence, 74(3-4):249-269, 2015. [doi]
Abstract is missing.