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