Abstract
Systems that integrate user-programmable theorem proving with efficient algorithms for boolean formula manipulation are promising platforms for implementing special-purpose tools that combine computation and deduction. An example tool is presented in this paper in which theorem proving is used to compile a class of problems stated in terms of functions operating on sets of integers to boolean problems that can be solved using a BDD oracle. The boolean solutions obtained via BDD calculations are then converted by theorem proving to the high-level representation. Although the example is rather specialised, our goal is to illustrate methodological principles for programming tools whose operation requires embedded proof.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. In Theorem Proving in Higher Order Logics (TPHOLs’99), number 1690 in Lecture Notes in Computer Science, pages 323–340. Springer-Verlag, 1999.
Bruno Barras. Programming and computing in HOL. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 17–37. Springer-Verlag, 2000.
See web page http://www-cad.eecs.berkeley.edu/~kenmcmil/smv.
L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham. The prosper toolkit. In S. Graf and M. Schwartbach, editors, Tools and Algorithms for Constructing Systems (TACAS 2000), number 1785 in Lecture Notes in Computer Science, pages 78–92. Springer-Verlag, 2000.
Michael J.C. Gordon. Reachability programming in HOL using BDDs. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, volume 1869 of Lecture Notes in Computer Science, pages 180–197. Springer-Verlag, 2000.
Mike Gordon. Reachability programming in HOL98 using BDDs. In The 13th International Conference on Theorem Proving and Higher Order Logics. Springer-Verlag, 2000.
John Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 38:162–170, 1995.
J. Joyce and C. Seger. The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover. In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG’93, Vancouver, B.C., August 11–13 1993, volume 780 of Lecture Notes in Computer Science, pages 185–198. Spinger-Verlag, 1994.
Moscow ML interface to BuDDy by Ken Friis Larsen and Jakob Lichtenberg documented at http://www.it-c.dk/research/muddy/.
K.L. McMillan. A compositional rule for hardware design refinement. In Orna Grumberg, editor, Computer-Aided Verification, CAV’ 97, Lecture Notes in Computer Science, pages 24–35, Haifa, Israel, June 1997. Springer-Verlag.
John O’Leary, Xudong Zhao, Robert Gerth, and Carl-Johan H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, First Quarter 1999. Online at http://developer.intel.com/technology/itj/.
See web page http://www.csl.sri.com/pvs.html.
S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, CAV’95, volume 939 of Lecture Notes in Computer Science, pages 84–97, Liege, Belgium, June 1995. Springer-Verlag.
Carl-Johan H. Seger. Voss-a formal hardware verification system: User’s guide. Technical Report UBC TR 93-45, The University of British Columbia, December 1993.
Fabio Somenzi’s CUDD: CU Decision Diagram Package documented at http://vlsi.colorado.edu/~fabio/CUDD/.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gordon, M.J.C. (2002). PuzzleTool: An Example of Programming Computation and Deduction. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2002. Lecture Notes in Computer Science, vol 2410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45685-6_15
Download citation
DOI: https://doi.org/10.1007/3-540-45685-6_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44039-0
Online ISBN: 978-3-540-45685-8
eBook Packages: Springer Book Archive