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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

1 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
Title of host publication	Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014)
Editors	F. Verbeek, J. Schmaltz
Publisher	EPTCS
Pages	77-85
DOIs	https://doi.org/10.4204/EPTCS.152.6
Publication status	Published - 2014
Event	conference; Twelfth International Workshop on the ACL2 Theorem Prover and its Applications; 2014-07-12; 2014-07-13 - Duration: 12 Jul 2014 → 13 Jul 2014

Publication series

Name	Electronic Proceedings in Theoretical Computer Science
Volume	152
ISSN (Print)	2075-2180

Conference

Conference	conference; Twelfth International Workshop on the ACL2 Theorem Prover and its Applications; 2014-07-12; 2014-07-13
Period	12/07/14 → 13/07/14
Other	Twelfth International Workshop on the ACL2 Theorem Prover and its Applications

Access to Document

10.4204/EPTCS.152.6

Cite this

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 (Eds.), Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014) (pp. 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). editor / F. Verbeek ; J. Schmaltz. EPTCS, 2014. pp. 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 (eds), 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, pp. 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). ed. / F. Verbeek; J. Schmaltz. EPTCS, 2014. p. 77-85 (Electronic Proceedings in Theoretical Computer Science; Vol. 152).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › 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, editors, Proceedings Twelfth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2 2014, Vienna, Austria, July 12-13, 2014). EPTCS. 2014. p. 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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this