Jan Jakubův and Cezary Kaliszyk
Intelligent Computer Mathematics – 16th International Conference, CICM 2023, pp. 303-308, 2023.
pdf 
doi:10.1007/978-3-031-42753-4_22
Abstract
We present a system for the visualization of proofs originating from Automated Theorem Provers for first-order logic. The system can hide uninteresting proof parts of proofs, such as type annotations, translate first-order terms to standard math syntax, and compactly display complex formulas. We demonstrate the system on several non-trivial automated proofs of statements from Mizar Mathematical Library translated to first-order logic, and we provide a web interface where curious users can browse and investigate the proofs.
BibTex
@inproceedings{jjck-cicm23, author = {Jan Jakubuv and Cezary Kaliszyk}, editor = {Catherine Dubois and Manfred Kerber}, title = {{VizAR: V}isualization of Automated Reasoning Proofs (System Description)}, booktitle = {Intelligent Computer Mathematics - 16th International Conference, {CICM} 2023}, series = {LNCS}, volume = {14101}, pages = {303--308}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-42753-4\_22}, doi = {10.1007/978-3-031-42753-4\_22},}