{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:50:04Z","timestamp":1725475804760},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676645"},{"type":"electronic","value":"9783540451013"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10721959_3","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T21:12:31Z","timestamp":1167426751000},"page":"25-44","source":"Crossref","is-referenced-by-count":16,"title":["Proof Generation in the Touchstone Theorem Prover"],"prefix":"10.1007","author":[{"given":"George C.","family":"Necula","sequence":"first","affiliation":[]},{"given":"Peter","family":"Lee","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Studies in Logic and the Foundations of Mathematics","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam (1954)"},{"issue":"4","key":"3_CR2","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1137\/0209063","volume":"9","author":"B. Aspvall","year":"1980","unstructured":"Aspvall, B., Shiloach, Y.: A polynomial time algorithm for solving systems of linear inequalities with two variables per inequality. SIAM Journal on Computing\u00a09(4), 827\u2013845 (1980)","journal-title":"SIAM Journal on Computing"},{"key":"3_CR3","unstructured":"Bledsoe, W.W.: The Sup-Inf method in Presurger arithmetic. Technical report. University of Texas Math Dept. (December 1974)"},{"key":"3_CR4","volume-title":"A Computational Logic","author":"R. Boyer","year":"1979","unstructured":"Boyer, R., Moore, J.S.: A Computational Logic. Academic Press, London (1979)"},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"Boulton, R.J.: A lazy approach to fully-expansive theorem proving. In: International Workshop on Higher Order Logic Theorem Proving and its Applications, Leuven, Belgium, pp. 19\u201338. North- Holland, Amsterdam (1992) IFIP Transactions","DOI":"10.1016\/B978-0-444-89880-7.50008-5"},{"key":"3_CR6","unstructured":"Boulton, R.J.: Efficiency in a Fully-Expansive Theorem Prover. PhD thesis. University of Cambridge (December 1993)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-60275-5_58","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"R.J. Boulton","year":"1995","unstructured":"Boulton, R.J.: Combining decision procedures in the HOL system. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol.\u00a0971, pp. 75\u201389. Springer, Heidelberg (1995)"},{"key":"3_CR8","unstructured":"Detlefs, D.L., Rustan, K., Leino, M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Palo Alto (December 1998)"},{"issue":"4","key":"3_CR9","doi-asserted-by":"publisher","first-page":"758","DOI":"10.1145\/322217.322228","volume":"27","author":"P.J. Downey","year":"1980","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpressions problem. Journal of the ACM\u00a027(4), 758\u2013771 (1980)","journal-title":"Journal of the ACM"},{"key":"3_CR10","unstructured":"Gordon, M.: HOL: A machine oriented formulation of higher-order logic. Technical Report 85. University of Cambridge, Computer Laboratory (July 1985)"},{"issue":"1","key":"3_CR11","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. Journal of the Association for Computing Machinery\u00a040(1), 143\u2013184 (1993)","journal-title":"Journal of the Association for Computing Machinery"},{"issue":"4","key":"3_CR12","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1093\/logcom\/1.4.497","volume":"1","author":"D. Miller","year":"1991","unstructured":"Miller, D.: A logic programming language with lambda-abstraction, function variables, and simple unification. Journal of Logic and Computation\u00a01(4), 497\u2013536 (1991)","journal-title":"Journal of Logic and Computation"},{"key":"3_CR13","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/0168-0072(91)90068-W","volume":"51","author":"D. Miller","year":"1991","unstructured":"Miller, D., Nadathur, G., Pfenning, F., Scedrov, A.: Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic\u00a051, 125\u2013157 (1991)","journal-title":"Annals of Pure and Applied Logic"},{"key":"3_CR14","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/263699.263712","volume-title":"The 24th Annual ACM Symposium on Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: The 24th Annual ACM Symposium on Principles of Programming Languages, pp. 106\u2013119. ACM, New York (1997)"},{"key":"3_CR15","unstructured":"Necula, G.C.: Compiling with Proofs. PhD thesis, Carnegie Mellon University (September 1998), Also available as CMU-CS-98-154"},{"key":"3_CR16","unstructured":"Nelson, G.: Techniques for program verification. Technical Report CSL- 81-10, Xerox Palo Alto Research Center (1981)"},{"issue":"2","key":"3_CR17","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.: Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"2","key":"3_CR18","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery\u00a027(2), 356\u2013364 (1980)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A generic theorem prover","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle: A generic theorem prover. LNCS, vol.\u00a0828, p. 321. Springer, Heidelberg (1994)"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1017\/CBO9780511569807.008","volume-title":"Logical Frameworks","author":"F. Pfenning","year":"1991","unstructured":"Pfenning, F.: Logic programming in the LF logical framework. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 149\u2013181. Cambridge University Press, Cambridge (1991)"},{"key":"3_CR22","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"811","DOI":"10.1007\/3-540-58156-1_66","volume-title":"Automated Deduction - CADE-12","author":"F. Pfenning","year":"1994","unstructured":"Pfenning, F.: Elf: A meta-language for deductive systems (system description). In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 811\u2013815. Springer, Heidelberg (1994)"},{"key":"3_CR23","unstructured":"Pratt, V.R.: Two easy theories whose combination is hard(1977) (unpublished manuscript)"},{"key":"3_CR24","unstructured":"Stump, A., Dill, D.L.: Generating proofs from a decision procedure. In: Pnueli, A., Traverso, P. (eds.) Proceedings of the FLoC Workshop on Run-Time Result Verifiication, Trento, Italy (July 1999)"},{"issue":"4","key":"3_CR25","doi-asserted-by":"publisher","first-page":"769","DOI":"10.1145\/322276.322288","volume":"28","author":"R. Shostak","year":"1981","unstructured":"Shostak, R.: Deciding linear inequalities by computing loop residues. Journal of the ACM\u00a028(4), 769\u2013779 (1981)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction - CADE-17"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10721959_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:42:53Z","timestamp":1556019773000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10721959_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676645","9783540451013"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/10721959_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}