Computer Assisted Reasoning with MIZAR
Proceedings of the Ninth International Joint Conference on Artificial Intelligence. AI and Education. Pages 26-27.
Abstract
We describe the MIZAR Computer Assisted Reasoning system. Several versions of MIZAR are currently implemented with varying powers of expressiveness and proof analysis. The main use of MIZAR has thus far been in mathematics education. Evolving versions of MIZAR have been under development for the past decade; consequently the s ystem has been subjected to extensive testing. Several experiments connected with the preparation of mathematics research papers have also been carried out. The naturalness and readability of MIZAR texts is demonstrated by example. A proof scanning facility that modularly splits into a proof structure analyzer and inference checker is described. We discuss our use of the facility in teaching undergraduate discrete mathematics for computer science.
@inproceedings{ijcai1985p6,
title = {Computer Assisted Reasoning with MIZAR},
author = {Trybulec, Andrzej and Blair, Howard A.},
booktitle = {Proceedings of the Ninth International Joint Conference on
Artificial Intelligence, {IJCAI-85}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Aravind Joshi},
pages = {26--27},
year = {1985},
note = {AI and Education},
url = {https://ijcai.org/proceedings/1985/6},
}
TY - CPAPER TI - Computer Assisted Reasoning with MIZAR AU - Trybulec, Andrzej AU - Blair, Howard A. T2 - Proceedings of the Ninth International Joint Conference on Artificial Intelligence, IJCAI-85 PB - International Joint Conferences on Artificial Intelligence PY - 1985 SP - 26 EP - 27 UR - https://ijcai.org/proceedings/1985/6 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
