Automated Proof Compression by Invention of New Definitions

Vyskočil, J., Stanovský, D., Urban, J.

VYSKOČIL, J., D. STANOVSKÝ, and J. URBAN. Automated Proof Compression by Invention of New Definitions. In: Logic for Programming, Artificial Intelligence, and Reasoning. 16th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Dakar, 2010-04-25/2010-05-01. Berlin: Springer, 2010. p. 447-462. ISBN 978-3-642-17510-7. DOI 10.1007/978-3-642-17511-4_25.

URL: http://www.springerlink.com/content/1w7ph58n373p50w4/