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

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

doi:10.4204/EPTCS.152.6

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

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

2 Citaten (Scopus)

1 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
Titel	Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014)
Redacteuren	F. Verbeek, J. Schmaltz
Uitgeverij	EPTCS
Pagina's	77-85
DOI's	https://doi.org/10.4204/EPTCS.152.6
Status	Gepubliceerd - 2014
Evenement	conference; Twelfth International Workshop on the ACL2 Theorem Prover and its Applications; 2014-07-12; 2014-07-13 - Duur: 12 jul. 2014 → 13 jul. 2014

Publicatie series

Naam	Electronic Proceedings in Theoretical Computer Science
Volume	152
ISSN van geprinte versie	2075-2180

Congres

Congres	conference; Twelfth International Workshop on the ACL2 Theorem Prover and its Applications; 2014-07-12; 2014-07-13
Periode	12/07/14 → 13/07/14
Ander	Twelfth International Workshop on the ACL2 Theorem Prover and its Applications

Toegang tot document

10.4204/EPTCS.152.6

Citeer dit

Joosten, S. J. C., Kaliszyk, C., & Urban, J. (2014). Initial experiments with TPTP-style automated theorem provers on ACL2 problems. In F. Verbeek, & J. Schmaltz (editors), Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014) (blz. 77-85). (Electronic Proceedings in Theoretical Computer Science; Vol. 152). EPTCS. https://doi.org/10.4204/EPTCS.152.6

Joosten, S.J.C. ; Kaliszyk, C. ; Urban, J. / Initial experiments with TPTP-style automated theorem provers on ACL2 problems. Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014). redacteur / F. Verbeek ; J. Schmaltz. EPTCS, 2014. blz. 77-85 (Electronic Proceedings in Theoretical Computer Science).

@inproceedings{1c73a71ca9a140caa409dd990e3f8362,

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",

doi = "10.4204/EPTCS.152.6",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science",

publisher = "EPTCS",

pages = "77--85",

editor = "F. Verbeek and J. Schmaltz",

booktitle = "Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014)",

note = "conference; Twelfth International Workshop on the ACL2 Theorem Prover and its Applications; 2014-07-12; 2014-07-13 ; Conference date: 12-07-2014 Through 13-07-2014",

}

Joosten, SJC, Kaliszyk, C & Urban, J 2014, Initial experiments with TPTP-style automated theorem provers on ACL2 problems. in F Verbeek & J Schmaltz (uitgave), Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014). Electronic Proceedings in Theoretical Computer Science, vol. 152, EPTCS, blz. 77-85, conference; Twelfth International Workshop on the ACL2 Theorem Prover and its Applications; 2014-07-12; 2014-07-13, 12/07/14. https://doi.org/10.4204/EPTCS.152.6

Initial experiments with TPTP-style automated theorem provers on ACL2 problems. / Joosten, S.J.C.; Kaliszyk, C.; Urban, J.
Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014). uitgave / F. Verbeek; J. Schmaltz. EPTCS, 2014. blz. 77-85 (Electronic Proceedings in Theoretical Computer Science; Vol. 152).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

TY - GEN

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.

U2 - 10.4204/EPTCS.152.6

DO - 10.4204/EPTCS.152.6

M3 - Conference contribution

T3 - Electronic Proceedings in Theoretical Computer Science

SP - 77

EP - 85

BT - Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014)

A2 - Verbeek, F.

A2 - Schmaltz, J.

PB - EPTCS

T2 - conference; Twelfth International Workshop on the ACL2 Theorem Prover and its Applications; 2014-07-12; 2014-07-13

Y2 - 12 July 2014 through 13 July 2014

ER -

Joosten SJC, Kaliszyk C, Urban J. Initial experiments with TPTP-style automated theorem provers on ACL2 problems. In Verbeek F, Schmaltz J, redacteurs, Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014). EPTCS. 2014. blz. 77-85. (Electronic Proceedings in Theoretical Computer Science). doi: 10.4204/EPTCS.152.6

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

Samenvatting

Publicatie series

Congres

Toegang tot document

Vingerafdruk

Citeer dit