Back to first pageBack to first page Centre for Artificial Intelligence of UNL
Browse our site
You are here:

Publication details

Go back
Publication details
Main information
Escape to Mizar from ATPs
2013
alama2013escape
We announce a tool for mapping E prover derivations to Mizar proofs. Our mapping complements earlier work that generates problems for automated theorem provers from Mizar inference checking problems. We describe the tool, explain the mapping, and show how we solved some of the difficulties that arise in mapping proofs between different logical formalisms, even when they are based on the same notion of logical consequence, as Mizar and E are (namely, first-order classical logic with identity).
In proceedings
Jesse Alama
Pascal Fontaine, Renate Schmidt, Stephan Schulz and
PAAR 2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning
Easychair Proceedings in Computing
Easychair
-
21
3-11
-
-
-
http://www.easychair.org/publications/?page=1559779348
Export formats
Jesse Alama, Escape to Mizar from ATPs, in: Pascal Fontaine and Renate Schmidt and Stephan Schulz and (eds), PAAR 2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning, Easychair Proceedings in Computing, Easychair, Vol. 21, Pag. 3-11, (http://www.easychair.org/publications/?page=1559779348), 2013.
<a href="/people/members/view.php?code=d18f2a73808637adda0742073904f056" class="author">Jesse Alama</a>, <b>Escape to Mizar from ATPs</b>, in: Pascal Fontaine, Renate Schmidt and Stephan Schulz and (eds), <u>PAAR 2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning</u>, Easychair Proceedings in Computing, Easychair, Vol. 21, Pag. 3-11, (<a href="http://www.easychair.org/publications/?page=1559779348" target="_blank">url</a>), 2013.
@inproceedings {alama2013escape, author = {Jesse Alama}, editor = {Pascal Fontaine and Renate Schmidt and Stephan Schulz and}, title = {Escape to Mizar from ATPs}, booktitle = {PAAR 2012: Proceedings of the Third Workshop on Practical Aspects of Automated Reasoning}, series = {Easychair Proceedings in Computing}, publisher = {Easychair}, volume = {21}, pages = {3-11}, url = {http://www.easychair.org/publications/?page=1559779348}, abstract = {We announce a tool for mapping E prover derivations to Mizar proofs. Our mapping complements earlier work that generates problems for automated theorem provers from Mizar inference checking problems. We describe the tool, explain the mapping, and show how we solved some of the difficulties that arise in mapping proofs between different logical formalisms, even when they are based on the same notion of logical consequence, as Mizar and E are (namely, first-order classical logic with identity).}, year = {2013}, }
Publication's urls
/publications/view.php?code=ad8269afc53f78332856f8188b5c7425
/publications/view.php?code=alama2013escape
Go back
Centre for Artificial Intelligence of UNL
Departamento de Informática, FCT/UNL
Quinta da Torre 2829-516 CAPARICA - Portugal
Tel. (+351) 21 294 8536 FAX (+351) 21 294 8541

Fundacao_FCT