Initial Experiments with TPTP-style Automated Theorem Provers on ACL2 Problems

Autor:	Joosten, Sebastiaan, Kaliszyk, Cezary, Urban, Josef
Rok vydání:	2014
Předmět:	Computer Science - Artificial Intelligence Computer Science - Logic in Computer Science
Zdroj:	EPTCS 152, 2014, pp. 77-85
Druh dokumentu:	Working Paper
DOI:	10.4204/EPTCS.152.6
Popis:	This paper reports our initial experiments with using external ATP on some corpora built with the ACL2 system. This is intended to provide the first estimate about the usefulness of such external reasoning and AI systems for solving ACL2 problems. Comment: In Proceedings ACL2 2014, arXiv:1406.1238
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1406.1559 Zobrazit plný text záznamu View this record from Arxiv