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

Research output: Book/Report › Report › Academic

136 Downloads (Pure)

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.

Original language	English
Publisher	s.n.
Number of pages	9
Publication status	Published - 2014

Publication series

Name	arXiv
Volume	1406.1559 [cs.AI]

Access to Document

691809797816384Final published version, 75.1 KB

Cite this

@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

Abstract

Publication series

Access to Document

Fingerprint

Cite this