{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T20:09:45Z","timestamp":1725566985819},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540304951"},{"type":"electronic","value":"9783540324195"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11590156_4","type":"book-chapter","created":{"date-parts":[[2005,12,5]],"date-time":"2005-12-05T15:43:16Z","timestamp":1133797396000},"page":"60-78","source":"Crossref","is-referenced-by-count":7,"title":["Inference Systems for Logical Algorithms"],"prefix":"10.1007","author":[{"given":"Natarajan","family":"Shankar","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W.W. Bledsoe","year":"1977","unstructured":"Bledsoe, W.W.: Non-resolution theorem proving. Artificial Intelligence\u00a09, 1\u201336 (1977)","journal-title":"Artificial Intelligence"},{"key":"4_CR2","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979)"},{"issue":"2","key":"4_CR3","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1023\/B:JARS.0000009518.26415.49","volume":"31","author":"L. Bachmair","year":"2003","unstructured":"Bachmair, L., Tiwari, A., Vigneron, L.: Abstract congruence closure. Journal of Automated Reasoning\u00a031(2), 129\u2013168 (2003)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"4_CR4","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/1088216.1088219","volume":"10","author":"B. Buchberger","year":"1976","unstructured":"Buchberger, B.: A theoretical basis for the reduction of polynomials to canonical forms. ACM SIGSAM Bulletin\u00a010(3), 19\u201329 (1976)","journal-title":"ACM SIGSAM Bulletin"},{"key":"4_CR5","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R.L. Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)"},{"issue":"1","key":"4_CR6","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1145\/35043.35045","volume":"31","author":"J. Cohen","year":"1988","unstructured":"Cohen, J.: A view of the origins and development of prolog. Communications of the ACM\u00a031(1), 26\u201336 (1988)","journal-title":"Communications of the ACM"},{"key":"#cr-split#-4_CR7.1","unstructured":"Davis, M.: A computer program for Presburger???s algorithm. In: Summaries of Talks Presented at the Summer Institute for Symbolic Logic (1957);"},{"key":"#cr-split#-4_CR7.2","unstructured":"Reprinted in Siekmann and Wrightson [SW83], pp. 41???48"},{"key":"4_CR8","first-page":"589","volume-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"N.G. Bruijn de","year":"1980","unstructured":"de Bruijn, N.G.: A survey of the project Automath. In: To, H.B. (ed.) Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 589\u2013606. Academic Press, London (1980)"},{"issue":"7","key":"4_CR9","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1983","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Communications of the ACM\u00a05(7), 394\u2013397 (1983); Reprinted in Siekmann and Wrightson [SW83], pp. 267\u2013270 (1983)","journal-title":"Communications of the ACM"},{"key":"4_CR10","unstructured":"de Moura, L., Rue\u00df, H., Shankar, N.: Justifying equality. In: Proceedings of PDPAR 2004 (2004)"},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. Journal of the ACM\u00a07, 201\u2013215 (1960)","journal-title":"Journal of the ACM"},{"issue":"3","key":"4_CR12","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M., Putnam, H.: A computing procedure for quantification theory. JACM\u00a07(3), 201\u2013215 (1960)","journal-title":"JACM"},{"issue":"4","key":"4_CR13","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"},{"volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic","year":"1993","key":"4_CR14","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge (1993)"},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R., Wadsworth, C.: Edinburgh LCF: A Mechanized Logic of Computation. In: Gordon, M., Wadsworth, C.P., Milner, R. (eds.) Edinburgh LCF. LNCS, vol.\u00a078, Springer, Heidelberg (1979)"},{"key":"4_CR16","unstructured":"Ganzinger, H., Rue\u00df, H., Shankar, N.: Modularity and refinement in inference systems. Technical Report CSL-SRI-04-02, SRI International, Computer Science Laboratory, 333 Ravenswood Ave, Menlo Park, CA, 94025 (January 2004), (revised August 2004)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Harrison","year":"1996","unstructured":"Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 265\u2013269. Springer, Heidelberg (1996)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1007\/3-540-62950-5_59","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"1997","unstructured":"Kapur, D.: hostak\u2019s congruence closure as completion. In: Comon, H. (ed.) RTA 1997. LNCS, vol.\u00a01232, pp. 23\u201337. Springer, Heidelberg (1997)"},{"key":"4_CR19","first-page":"263","volume-title":"Computational Problems in Abstract Algebras","author":"D.E. Knuth","year":"1970","unstructured":"Knuth, D.E., Bendix, P.: imple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebras, pp. 263\u2013297. Pergamon Press, Oxford (1970)"},{"key":"4_CR20","volume-title":"Introduction to Metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to Metamathematics. North-Holland, Amsterdam (1952)"},{"key":"4_CR21","volume-title":"Advances in Formal Methods.","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. In: Advances in Formal Methods., vol.\u00a03, Kluwer, Dordrecht (2000)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Complexity of finitely presented algebras. In: Conference Record of the Ninth Annual ACM Symposium on Theory of Computing, Boulder, Colorado, May 2\u20134, pp. 164\u2013177 (1977)","DOI":"10.1145\/800105.803406"},{"key":"4_CR23","unstructured":"Luo, Z., Pollack, R.: The LEGO proof development system: A user\u2019s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh (1992)"},{"key":"4_CR24","first-page":"219","volume-title":"Proceedings of a Symposium in Pure Mathematics","author":"J. McCarthy","year":"1962","unstructured":"McCarthy, J.: Computer programs for checking mathematical proofs. In Recursive Function Theory. In: Proceedings of a Symposium in Pure Mathematics, vol.\u00a0V, pp. 219\u2013227. American Mathematical Society, Providence (1962)"},{"key":"4_CR25","unstructured":"McCune, W.W.: Solution of the Robbins problem, Available from \n                    \n                      ftp:\/\/info.mcs.anl.gov\/pub\/Otter\/www-misc\/robbins-jar-submitted.ps.gz\n                    \n                    \n                   (1997)"},{"issue":"2","key":"4_CR26","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: 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"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-32033-3_33","volume-title":"Term Rewriting and Applications","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-Producing Congruence Closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 453\u2013468. Springer, Heidelberg (2005)"},{"key":"4_CR28","doi-asserted-by":"crossref","unstructured":"Newell, A., Shaw, J.C., Simon, H.A.: Empirical explorations with the logic theory machine: A case study in heuristics. In: Proc. West. Joint Comp. Conf., pp. 218\u2013239 (1957), Reprinted in Siekmann and Wrightson [SW83], pp. 49\u201373 (1983)","DOI":"10.1007\/978-3-642-81952-0_4"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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. Springer, Heidelberg (1994)"},{"issue":"1","key":"4_CR30","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012(1), 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"4_CR31","first-page":"227","volume":"1","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: Automatic deduction with hyper-resolution. International Journal of Computational Mathematics\u00a01, 227\u2013234 (1965)","journal-title":"International Journal of Computational Mathematics"},{"volume-title":"Handbook of Automated Reasoning","year":"2001","key":"4_CR32","unstructured":"Robinson, A., Voronkov, A. (eds.): Handbook of Automated Reasoning. Elsevier Science, Amsterdam (2001)"},{"issue":"7","key":"4_CR33","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R.E. Shostak","year":"1978","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. Communications of the ACM\u00a021(7), 583\u2013585 (1978)","journal-title":"Communications of the ACM"},{"issue":"2","key":"4_CR34","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R.E. Shostak","year":"1979","unstructured":"Shostak, R.E.: A practical decision procedure for arithmetic with function symbols. Journal of the ACM\u00a026(2), 351\u2013360 (1979)","journal-title":"Journal of the ACM"},{"issue":"1","key":"4_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2422.322411","volume":"31","author":"R.E. Shostak","year":"1984","unstructured":"Shostak, R.E.: Deciding combinations of theories. Journal of the ACM\u00a031(1), 1\u201312 (1984)","journal-title":"Journal of the ACM"},{"issue":"2","key":"4_CR36","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G. Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.B.: The TPTP Problem Library: CNF Release v1.2.1. Journal of Automated Reasoning\u00a021(2), 177\u2013203 (1998)","journal-title":"Journal of Automated Reasoning"},{"volume-title":"Automation of Reasoning: Classical Papers on Computational Logic","year":"1983","key":"4_CR37","unstructured":"Siekmann, J., Wrightson, G. (eds.): Automation of Reasoning: Classical Papers on Computational Logic. Springer, Heidelberg (1983)"},{"key":"4_CR38","unstructured":"Coq Development Team. The Coq proof assistant reference manual, version 8.0. Technical report, INRIA, Rocquencourt, France (January 2005)"},{"issue":"4","key":"4_CR39","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"Wos, L., Robinson, G.A., Carson, D.: Efficiency and completeness of the set of support strategy in theorem proving. Journal of the ACM\u00a012(4), 536\u2013541 (1965)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11590156_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:49:16Z","timestamp":1619506156000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11590156_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540304951","9783540324195"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/11590156_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}