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/Published conference outputConference 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 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
Country/TerritoryUnited States
CityBoston, MA
Period11/05/0912/05/09

Keywords

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

Fingerprint

Dive into the research topics of 'Hypertext navigation of ACL2 proofs with XMLEye'. Together they form a unique fingerprint.

Cite this