1285612Sdelphij\begin{thebibliography}{99}
2181834Sroberto
3285612Sdelphij\bibitem{SUPINFBledsoe} % OK
4330567SgordonW.~W. Bledsoe.
5181834Sroberto\newblock A new method for proving certain {P}resburger formulas.
6181834Sroberto\newblock In {\em Advance Papers 4th Int. Joint Conf. on Artif. Intell.,
7181834Sroberto  Tbilisi, Georgia, U.S.S.R.}, pages 15--21, September 1975.
8285612Sdelphij
9181834Sroberto\bibitem{EfficFullyExpTP} % OK
10285612SdelphijR.~J. Boulton.
11285612Sdelphij\newblock On efficiency in theorem provers which fully expand proofs into
12285612Sdelphij  primitive inferences.
13285612Sdelphij\newblock Technical Report 248, University of Cambridge Computer Laboratory,
14285612Sdelphij  February 1992.
15285612Sdelphij
16285612Sdelphij\bibitem{description} % OK
17181834Sroberto{\small DSTO} and {\small SRI} International,
18285612Sdelphij{\em The HOL System: DESCRIPTION}, (1991).
19285612Sdelphij
20181834Sroberto\bibitem{reduce} % OK
21316722SdelphijJ.~R.~Harrison.
22285612Sdelphij\newblock The HOL reduce Library.
23285612Sdelphij\newblock In {\em The HOL System: LIBRARIES}.
24285612Sdelphij\newblock {\small DSTO} and {\small SRI} International, 1991.
25285612Sdelphij
26285612Sdelphij\bibitem{VarElimHodes} % OK
27285612SdelphijL.~Hodes.
28285612Sdelphij\newblock Solving problems by formula manipulation.
29285612Sdelphij\newblock In {\em Advance Papers 2nd Int. Joint Conf. on Artif. Intell.,
30285612Sdelphij  London}, pages 553--559. The British Computer Society, September 1971.
31285612Sdelphij\newblock Revised version in Artificial Intelligence 3, North-Holland,
32285612Sdelphij  Amsterdam, 1972, pages 165--174.
33285612Sdelphij
34285612Sdelphij\bibitem{SUPINFShostak} % OK
35285612SdelphijR.~E. Shostak.
36285612Sdelphij\newblock On the {SUP-INF} method for proving {P}resburger formulae.
37181834Sroberto\newblock {\em Journal of the ACM}, 24(4):529--543, October 1977.
38285612Sdelphij
39181834Sroberto\end{thebibliography}
40181834Sroberto
41181834Sroberto
42181834Sroberto