Initial experiments with TPTP-style automated theorem provers on ACL2 problems

S.J.C. Joosten; C. Kaliszyk; J. Urban

Initial experiments with TPTP-style automated theorem provers on ACL2 problems

S.J.C. Joosten, C. Kaliszyk, J. Urban

Onderzoeksoutput: Boek/rapport › Rapport › Academic

134 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Uitgeverij	s.n.
Aantal pagina's	9
Status	Gepubliceerd - 2014

Publicatie series

Naam	arXiv
Volume	1406.1559 [cs.AI]

Toegang tot document

691809797816384Definitieve gepubliceerde versie, 75,1 KB

Citeer dit

@book{297de9826dd84639a50f2ebfa4d4b151,

title = "Initial experiments with TPTP-style automated theorem provers on ACL2 problems",

abstract = "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.",

author = "S.J.C. Joosten and C. Kaliszyk and J. Urban",

year = "2014",

language = "English",

series = "arXiv",

publisher = "s.n.",

}

TY - BOOK

T1 - Initial experiments with TPTP-style automated theorem provers on ACL2 problems

AU - Joosten, S.J.C.

AU - Kaliszyk, C.

AU - Urban, J.

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

M3 - Report

T3 - arXiv

BT - Initial experiments with TPTP-style automated theorem provers on ACL2 problems

PB - s.n.

ER -

Initial experiments with TPTP-style automated theorem provers on ACL2 problems

Samenvatting

Publicatie series

Toegang tot document

Vingerafdruk

Citeer dit