Hypertext navigation of ACL2 proofs with XMLEye

Antonio García-Domínguez*, Francisco Palomo-Lozano, Inmaculada Medina-Bulo

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Difficult problems often require complex solutions, and the proofs checked by ACL2 are no exception. There are steep learning curves involved both in producing the proof script and analyzing its long and complex results. Existing tools, such as DrACuLa or ACL2s, tend to focus more on the first aspect than the second one. We have developed XMLEye, a framework for creating viewers for complex structured documents. Upon this framework, we have created a tool which can reorganize ACL2 proofs and present them in a more accessible format. First, the plain text proof produced by ACL2 is converted into an intermediate form. Then, it is rendered as hypertext through a transformation described by a collection of external scripts. We introduce the overall design and implementation of XMLEye as a framework and discuss the customizations required to reorganize and render ACL2 proofs.

Original languageEnglish
Title of host publicationACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications
PublisherACM
Pages47-56
Number of pages10
ISBN (Print)9781605587424
DOIs
Publication statusPublished - 1 Dec 2009
Event8th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '09 - Boston, MA, United States
Duration: 11 May 200912 May 2009

Conference

Conference8th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '09
CountryUnited States
CityBoston, MA
Period11/05/0912/05/09

Fingerprint

Navigation

Keywords

  • ACL2
  • Formal methods
  • Proof presentation
  • XHTML
  • XML
  • XSLT

Cite this

García-Domínguez, A., Palomo-Lozano, F., & Medina-Bulo, I. (2009). Hypertext navigation of ACL2 proofs with XMLEye. In ACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications (pp. 47-56). ACM. https://doi.org/10.1145/1637837.1637845
García-Domínguez, Antonio ; Palomo-Lozano, Francisco ; Medina-Bulo, Inmaculada. / Hypertext navigation of ACL2 proofs with XMLEye. ACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications. ACM, 2009. pp. 47-56
@inproceedings{3320d0251a0a4271bf9718377a56643e,
title = "Hypertext navigation of ACL2 proofs with XMLEye",
abstract = "Difficult problems often require complex solutions, and the proofs checked by ACL2 are no exception. There are steep learning curves involved both in producing the proof script and analyzing its long and complex results. Existing tools, such as DrACuLa or ACL2s, tend to focus more on the first aspect than the second one. We have developed XMLEye, a framework for creating viewers for complex structured documents. Upon this framework, we have created a tool which can reorganize ACL2 proofs and present them in a more accessible format. First, the plain text proof produced by ACL2 is converted into an intermediate form. Then, it is rendered as hypertext through a transformation described by a collection of external scripts. We introduce the overall design and implementation of XMLEye as a framework and discuss the customizations required to reorganize and render ACL2 proofs.",
keywords = "ACL2, Formal methods, Proof presentation, XHTML, XML, XSLT",
author = "Antonio Garc{\'i}a-Dom{\'i}nguez and Francisco Palomo-Lozano and Inmaculada Medina-Bulo",
year = "2009",
month = "12",
day = "1",
doi = "10.1145/1637837.1637845",
language = "English",
isbn = "9781605587424",
pages = "47--56",
booktitle = "ACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications",
publisher = "ACM",
address = "United States",

}

García-Domínguez, A, Palomo-Lozano, F & Medina-Bulo, I 2009, Hypertext navigation of ACL2 proofs with XMLEye. in ACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications. ACM, pp. 47-56, 8th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '09, Boston, MA, United States, 11/05/09. https://doi.org/10.1145/1637837.1637845

Hypertext navigation of ACL2 proofs with XMLEye. / García-Domínguez, Antonio; Palomo-Lozano, Francisco; Medina-Bulo, Inmaculada.

ACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications. ACM, 2009. p. 47-56.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Hypertext navigation of ACL2 proofs with XMLEye

AU - García-Domínguez, Antonio

AU - Palomo-Lozano, Francisco

AU - Medina-Bulo, Inmaculada

PY - 2009/12/1

Y1 - 2009/12/1

N2 - Difficult problems often require complex solutions, and the proofs checked by ACL2 are no exception. There are steep learning curves involved both in producing the proof script and analyzing its long and complex results. Existing tools, such as DrACuLa or ACL2s, tend to focus more on the first aspect than the second one. We have developed XMLEye, a framework for creating viewers for complex structured documents. Upon this framework, we have created a tool which can reorganize ACL2 proofs and present them in a more accessible format. First, the plain text proof produced by ACL2 is converted into an intermediate form. Then, it is rendered as hypertext through a transformation described by a collection of external scripts. We introduce the overall design and implementation of XMLEye as a framework and discuss the customizations required to reorganize and render ACL2 proofs.

AB - Difficult problems often require complex solutions, and the proofs checked by ACL2 are no exception. There are steep learning curves involved both in producing the proof script and analyzing its long and complex results. Existing tools, such as DrACuLa or ACL2s, tend to focus more on the first aspect than the second one. We have developed XMLEye, a framework for creating viewers for complex structured documents. Upon this framework, we have created a tool which can reorganize ACL2 proofs and present them in a more accessible format. First, the plain text proof produced by ACL2 is converted into an intermediate form. Then, it is rendered as hypertext through a transformation described by a collection of external scripts. We introduce the overall design and implementation of XMLEye as a framework and discuss the customizations required to reorganize and render ACL2 proofs.

KW - ACL2

KW - Formal methods

KW - Proof presentation

KW - XHTML

KW - XML

KW - XSLT

UR - http://www.scopus.com/inward/record.url?scp=77952981177&partnerID=8YFLogxK

UR - https://dl.acm.org/citation.cfm?doid=1637837.1637845

U2 - 10.1145/1637837.1637845

DO - 10.1145/1637837.1637845

M3 - Conference contribution

AN - SCOPUS:77952981177

SN - 9781605587424

SP - 47

EP - 56

BT - ACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications

PB - ACM

ER -

García-Domínguez A, Palomo-Lozano F, Medina-Bulo I. Hypertext navigation of ACL2 proofs with XMLEye. In ACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications. ACM. 2009. p. 47-56 https://doi.org/10.1145/1637837.1637845