Hypertext navigation of ACL2 proofs with XMLEye

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

doi:10.1145/1637837.1637845

Hypertext navigation of ACL2 proofs with XMLEye

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

^*Corresponding author for this work

College of Engineering and Physical Sciences

Research output: Chapter in Book/Published conference output › Conference publication

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 language	English
Title of host publication	ACL2 '09 - Proceedings of the 8th International Workshop on the ACL2 Theorem Prover and its Applications
Publisher	ACM
Pages	47-56
Number of pages	10
ISBN (Print)	9781605587424
DOIs	https://doi.org/10.1145/1637837.1637845
Publication status	Published - 1 Dec 2009
Event	8th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '09 - Boston, MA, United States Duration: 11 May 2009 → 12 May 2009

Conference

Conference	8th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '09
Country/Territory	United States
City	Boston, MA
Period	11/05/09 → 12/05/09

Keywords

ACL2
Formal methods
Proof presentation
XHTML
XML
XSLT

Access to Document

10.1145/1637837.1637845

Cite this

@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 = dec,

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

note = "8th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '09 ; Conference date: 11-05-2009 Through 12-05-2009",

}

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

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 publication

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

T2 - 8th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 '09

Y2 - 11 May 2009 through 12 May 2009

ER -

Hypertext navigation of ACL2 proofs with XMLEye

Abstract

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this