How to Pretty-Print a Long Formula

- ABSTRACT:

We present a standard rendering for higher-order logic (HOL) to make specifications more readable. We propose a structured rendering that borrows greatly from Leslie Lamport's original proposal for writ- ing long mathematical formulas. Furthermore, we present a freely- available parser and pretty-printer that implements these ideas, which we call beautifHOL. We conclude by describing possible extensions to our proposed rendering and motivate the need for formatting standards for formal specifications.

- BIBTEX:

@misc{pike-pp, author = {Lee Pike}, title = {How to pretty-print a long formula}, note = {Unpublished. Available at \url{http://www.cs.indiana.edu/~lepike/pub_pages/holpp.html}}}

- PAPER DOWNLOAD: pdf

- SLIDES DOWNLOAD: To appear.

- PROGRAM DOWNLOAD: The pretty-printer, called
`beautifHOL`, is written in Haskell and is available for download from Hackage, which provides facilities to automatically build and install Haskell programs.

- OTHER FILES:

- Documentation (HTML)
- README
- LICENSE (BSD3 license)
- BNF grammar specification of the input language: pdf
- Test data (file of input formulas): examples.txt.

Issue`beautifHOL --f formulas.txt`to pretty-print every uncommented formula in the file..

Lee Pike (home) |