Skip to content

Commit

Permalink
Updated HOL Description with higher mathematics contents promoted to …
Browse files Browse the repository at this point in the history 
…chapter level
  • Loading branch information
@binghe @mn200
binghe authored and mn200 committed Mar 18, 2024
1 parent 9ac238f commit 671b4b7
Show file tree
Hide file tree
Showing 9 changed files with 4,288 additions and 162 deletions.
9 changes: 8 additions & 1 deletion Manual/Description/Holmakefile
View file
Expand Up @@ -24,7 +24,10 @@ drules.tex: drules.stex $(PS_STUFF)
tactics.tex: tactics.stex $(PS_STUFF)
$(PS_COMMAND)

theories.tex: theories.stex $(PS_STUFF) $(dprot $(SIGOBJ)/realTheory.uo) $(dprot $(HOLDIR)/src/integer/integerTheory.uo)
theories.tex: theories.stex $(PS_STUFF) $(dprot $(SIGOBJ)/realTheory.uo) \
$(dprot $(HOLDIR)/src/integer/integerTheory.uo) \
$(dprot $(SIGOBJ)/real_sigmaTheory.uo) \
$(dprot $(SIGOBJ)/iterateTheory.uo)
$(PS_COMMAND)

math.tex: math.stex $(PS_STUFF) $(dprot $(SIGOBJ)/probabilityTheory.uo) \
Expand All @@ -47,6 +50,10 @@ system.tex: system.stex $(PS_STUFF)
HolSat.tex: HolSat.stex $(PS_STUFF) zchaff.cnf
$(PS_COMMAND)

# This builds figs/0.mps, figs/1.mps, ...
figures:
mpost -mem=metafun -tex=latex figure.mp

EXTRA_CLEANS = drules.tex tactics.tex theories.tex libraries.tex \
PatternMatchesLib.tex HolSat.tex definitions.tex \
system.tex conv.tex math.tex \
Expand Down
2 changes: 1 addition & 1 deletion Manual/Description/QuantHeuristics.tex
View file
Expand Up @@ -37,7 +37,7 @@ \subsection{Motivation}

\newcommand{\mytablehead}[1]{\\\multicolumn{2}{l}{\textit{#1}}\\}
\begin{table}[h]
\centering\scriptsize
\centering %\scriptsize (too small, no need to save page spaces here)
\begin{tabular}{lll}
\textbf{Problem} & \textbf{Result} \\\hline

Expand Down
115 changes: 89 additions & 26 deletions Manual/Description/description.bib
View file
Expand Up @@ -467,8 +467,8 @@ @TECHREPORT{harrison-style
year = 1997,
type = "Technical Report",
number = 428,
note = "Available on the Web as
{\url{http://www.cl.cam.ac.uk/users/jrh/papers/tang.html}}"}
url = {http://www.cl.cam.ac.uk/users/jrh/papers/tang.html}
}

@Article{oleary-itj-99,
author = {O'Leary, John and Zhao, Xudong and Gerth, Robert and
Expand All @@ -478,7 +478,7 @@ @Article{oleary-itj-99
journal = {Intel Technology Journal},
year = 1999,
month = {First Quarter},
note = {Online at {\url{http://developer.intel.com/technology/itj/}}}
url = {http://developer.intel.com/technology/itj/}
}

@techreport{SegerVoss,
Expand All @@ -495,7 +495,7 @@ @techreport{McMillan99
title = {A methodology for hardware verification using compositional model checking},
institution = {Cadence Berkeley Labs},
month = apr,
note = {Available at {\url{http://www-cad.eecs.berkeley.edu/~kenmcmil/}}},
url = {http://www-cad.eecs.berkeley.edu/~kenmcmil/},
year = "1999"}


Expand Down Expand Up @@ -542,20 +542,20 @@ @techreport{YoungAutopilot
month = jul,
year = "1996"}

@misc{HoareFest,
author = "Mike Gordon",
title = {Programming combinations of deduction and {BDD}-based symbolic calculation},
note = {Draft available at
{\url{http://www.cl.cam.ac.uk/~mjcg/celebration/}}}
@article{HoareFest,
title={Programming combinations of deduction and BDD-based symbolic calculation},
author={Gordon, Michael JC},
journal={LMS Journal of Computation and Mathematics},
volume={5},
pages={56--76},
year={2002},
publisher={Cambridge University Press}
}



@misc{GordonVerilogSemantics,
author = "Mike Gordon",
title = {Synthesizable Verilog: syntax and semantics},
note = {Draft available at
{\url{http://www.cl.cam.ac.uk/users/mjcg/Verilog/V/V.ps.gz}}}
url = {http://www.cl.cam.ac.uk/users/mjcg/Verilog/V/V.ps.gz}
}

@incollection{JoyceSeger,
Expand All @@ -580,8 +580,7 @@ @misc{HenrikNotes
month = oct,
organization ="Department of Information Technology, Technical University of Denmark,
Building 344, DK-2800 Lyngby, Denmark",
note ="Lecture notes for 49285 Advanced Algorithms E97.
Available from: {\url{http://www.it.dtu.dk/~hra}}"
url = {https://course.ccs.neu.edu/cs5800gc/parent/buddy-2.4/doc/bddnotes.pdf}
}


Expand Down Expand Up @@ -817,12 +816,10 @@ @misc{Amjad:TPHOLs2001
title = "{BDD} Representation Judgements in {HOL}: A Performance Evaluation",
note = "Category B paper presented at the
{\it 14th International Conference on Theorem Proving and Higher Order Logics\/}.
Edinburgh, Scotland, UK, August 2001.
Available from \url{http://www.cl.cam.ac.uk/~ha227/}",
Edinburgh, Scotland, UK, August 2001.",
url = {https://www.inf.ed.ac.uk/publications/online/0046/b017.pdf}
}



@Book{Isabelle-book,
author = "Lawrence C. Paulson",
title = "Isabelle: A Generic Theorem Prover",
Expand All @@ -839,9 +836,6 @@ @Article{paulson-jcs
volume = 6,
pages = {85-128}}




@Book{Back,
author = "Ralph-Johan Back and Joakim von Wright",
title = "Refinement Calculus: A Systematic Introduction",
Expand Down Expand Up @@ -912,7 +906,6 @@ @inproceedings{Maranget2008
location = {Victoria, BC, Canada},
pages = {35--46},
numpages = {12},
url = {http://doi.acm.org/10.1145/1411304.1411311},
doi = {10.1145/1411304.1411311},
acmid = {1411311},
publisher = {ACM},
Expand Down Expand Up @@ -1009,7 +1002,7 @@ @book{Kolmogorov:1950
@book{Shiryaev:2016vm,
author = {Shiryaev, Albert Nikolaevich},
title = {Probability-1},
publisher = {Springer-Verlag New York},
publisher = {Springer-Verlag},
year = {2016},
volume = {95},
series = {Graduate Texts in Mathematics},
Expand All @@ -1020,9 +1013,9 @@ @book{Shiryaev:2016vm
}

@book{Shiryaev:2019kf,
author = {Albert N. Shiryaev},
author = {Shiryaev, Albert Nikolaevich},
title = {Probability-2},
publisher = {Springer-Verlag New York},
publisher = {Springer-Verlag},
year = {2019},
address = {New York, NY},
edition = {3},
Expand Down Expand Up @@ -1087,6 +1080,41 @@ @book{Gnedenko:1954vf
address = {Cambridge, MA}
}

@Manual{harrison2017hol,
title={HOL Light tutorial},
author={Harrison, John},
url={http://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial.pdf},
day = {14},
month = jan,
year = {2017}
}

@article{Harrison:2012ig,
author = {Harrison, John},
title = {{The HOL Light Theory of Euclidean Space}},
journal = {Journal of Automated Reasoning},
year = {2012},
volume = {50},
number = {2},
pages = {173--190},
month = apr,
doi = {10.1007/s10817-012-9250-9}
}

@book{Courant:1989vw,
author = {Courant, Richard and John, Fritz},
title = {{Introduction to Calculus and Analysis, Volume I}},
publisher = {Springer-Verlag},
year = {1989}
}

@book{Courant:1989tt,
author = {Courant, Richard and John, Fritz},
title = {{Introduction to Calculus and Analysis, Volume II}},
publisher = {Springer-Verlag},
year = {1989}
}

@inproceedings{ITP23,
author = {Oskar Abrahamsson and Magnus O. Myreen},
title = {Fast, Verified Computation for {Candle}},
Expand All @@ -1097,3 +1125,38 @@ @inproceedings{ITP23
url = {https://cakeml.org/itp23.pdf}
}

@incollection{Norrish:2013,
author = {Norrish, Michael and Huffman, Brian},
title = {{Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) $\omega_1$}},
booktitle = {LNCS 7998 - Interactive Theorem Proving (ITP 2013)},
year = {2013},
pages = {133--146},
publisher = {Springer},
month = jun,
doi = {10.1007/978-3-642-39634-2_12}
}

@incollection{IsaCardinals,
author = {Blanchette, Jasmin Christian and Popescu, Andrei and Traytel, Dmitriy},
title = {{Cardinals in Isabelle/HOL}},
booktitle = {LNCS 8558 - Interactive Theorem Proving (ITP 2014)},
year = {2014},
publisher = {Springer},
month = jun,
doi = {10.1007/978-3-319-08970-6_8}
}

@book{ACL2approach,
author = {Kaufmann, Matt and Manolios, Panagiotis and Moore, J Strother},
title = {{Computer-Aided Reasoning: An Approach}},
publisher = {Springer},
year = {2000},
volume = {3},
series = {Advances in Formal Methods},
address = {Boston, MA},
month = jul,
doi = {10.1007/978-1-4615-4449-4},
isbn = {9780792377443},
issn = {1567-7338}
}

30 changes: 17 additions & 13 deletions Manual/Description/description.tex
View file
Expand Up @@ -5,7 +5,11 @@
\documentclass[12pt,fleqn]{book}
\usepackage[notindex]{tocbibind}

%\usepackage{amsmath}
\usepackage[numbers,sort&compress]{natbib}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}

\usepackage{amsmath}
\usepackage{amssymb}
%\usepackage{amsbsy}
\usepackage{amsthm}
Expand All @@ -19,6 +23,7 @@

\usepackage{../../src/TeX/holtexbasic}
\usepackage{fancyvrb}
\usepackage[format=hang,justification=raggedright]{caption} % multi-line figure caption

\hyphenation{docu-ments}

Expand All @@ -36,7 +41,15 @@
%\includeonly{logic,semantics}
%\includeonly{system,theories,libraries}

\usepackage[hidelinks,hypertexnames=false,pdftitle={The HOL System DESCRIPTION}]{hyperref}
\usepackage[hidelinks,hypertexnames=false]{hyperref}
\hypersetup{
pdftitle={The HOL System DESCRIPTION},
pdfauthor={The HOL4 contributors},
pdfsubject={HOL4},
pdfkeywords={Interactive Theorem Proving; Higher Order Logic},
pdfdisplaydoctitle=true
}

\usepackage{breakurl} % it depends on hyperref

\usepackage{centernot}
Expand Down Expand Up @@ -86,7 +99,6 @@

% \part{The HOL System \label{HOL-SYS}}


\include{system} % embedding HOL logic in ML
\include{drules} % derived rules
\include{conv} % conversions
Expand All @@ -95,7 +107,6 @@
\include{math} % math theories
\include{definitions}
\include{libraries}
% \include{map}
\include{misc}

% ---------------------------------------------------------------------
Expand All @@ -111,21 +122,14 @@
% references to entire description
% ---------------------------------------------------------------------

%\include{references}
\bibliographystyle{plain}
% The "plainnat" style will show also the DOI and URL, etc.
\bibliographystyle{plainnat}
\bibliography{description}

% ---------------------------------------------------------------------
% Appendix describing Version 2.0
% ---------------------------------------------------------------------

% \include{version2}

% ---------------------------------------------------------------------
% Index
% ---------------------------------------------------------------------


\small
\emergencystretch=14pt
\printindex
Expand Down

0 comments on commit 671b4b7

Please sign in to comment.