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},
}