{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:56Z","timestamp":1749182816344,"version":"3.41.0"},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1997,2,1]],"date-time":"1997-02-01T00:00:00Z","timestamp":854755200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,2,1]],"date-time":"1997-02-01T00:00:00Z","timestamp":854755200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[1997,2]]},"DOI":"10.1023\/a:1005749401809","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:13:52Z","timestamp":1040512432000},"page":"105-134","source":"Crossref","is-referenced-by-count":3,"title":["Unification Algorithms for Eliminating and Introducing Quantifiers in Natural Deduction Automated Theorem Proving"],"prefix":"10.1007","volume":"18","author":[{"given":"Li","family":"Dafa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"119339_CR1","volume-title":"An Introduction to Mathematical Logic and Type Theory: To Truth through Proof","author":"P. B. Andrews","year":"1986","unstructured":"Andrews, P. B.: An Introduction to Mathematical Logic and Type Theory: To Truth through Proof, Academic Press, Orlando, FL, 1986."},{"key":"119339_CR2","volume-title":"Proc. 5th Conference on Automated Deduction, Les Arcs, France, Lecture Notes in Computer Science","author":"P. B. Andrews","year":"1980","unstructured":"Andrews, P. B.: Transforming mating into natural deduction proofs, in G. Goos and J. Hartmanis (eds), Proc. 5th Conference on Automated Deduction, Les Arcs, France, Lecture Notes in Computer Science 138, Springer-Verlag, Berlin, 1980."},{"issue":"2","key":"119339_CR3","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(91)90192-5","volume":"81","author":"K. S. H. S. R. Bhatta","year":"1991","unstructured":"Bhatta, K. S. H. S. R. and Karnick, H.: A resolution rule for well-formed formulae, Theor. Comp. Sci.\n81(2) (1991), 223\u2013235.","journal-title":"Theor. Comp. Sci."},{"key":"119339_CR4","doi-asserted-by":"crossref","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, Art. Intelligence\n9(1977), 1\u201335.","journal-title":"Art. Intelligence"},{"key":"119339_CR5","unstructured":"Bruschi, M.: The Halting Problem, AAR Newsletter No. 17, March 1991."},{"key":"119339_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-55034-8","volume-title":"Resolution Principle for a Logic with Restricted Quantifiers","author":"H.-J. Burckert","year":"1991","unstructured":"Burckert, H.-J.: Resolution Principle for a Logic with Restricted Quantifiers, Springer-Verlag, Berlin, 1991."},{"issue":"3","key":"119339_CR7","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1145\/24658.24665","volume":"18","author":"L. Burkholder","year":"1987","unstructured":"Burkholder, L.: The Halting Problem, SIGACT News 18, No. 3 (Spring 1987), 48\u201360.","journal-title":"SIGACT News"},{"key":"119339_CR8","unstructured":"Burkholder, L.: A 76th Automated Theorem Proving Problem, AAR Newsletter 8, April 1987."},{"key":"119339_CR9","unstructured":"Cerrito, S.: Herbrand methods in sequent calculi: Unification in LL, in Proc. Joint International Conference and Symposium on Logic Programming, 1992, pp. 607\u2013621."},{"key":"119339_CR10","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"Chang, C. L. and Lee, R. C. T.: Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"119339_CR11","doi-asserted-by":"crossref","unstructured":"Chu, H. and Plaisted, D.: Semantically guided first-order theorem proving using hyper-linking, in Proc. 12th Conference on Automated Deduction, Nancy, France, June 28\u2013July 1, 1994.","DOI":"10.1007\/3-540-58156-1_14"},{"key":"119339_CR12","first-page":"191","volume":"6","author":"D. De Champeaux","year":"1979","unstructured":"De Champeaux, D.: Sub-problem finder and instance checker: Two cooperating preprocessors for theorem provers, IJCAI\n6(1979), 191\u2013196.","journal-title":"IJCAI"},{"key":"119339_CR13","unstructured":"Egly, U. and Rath, T.: The Halting Problem: An Automatically Generated Proof, AAR Newsletter No. 30, Aug. 1995."},{"key":"119339_CR14","doi-asserted-by":"crossref","unstructured":"Gentzen, G.: Investigations into logical deductions, in M. E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969, pp. 68\u2013131.","DOI":"10.1016\/S0049-237X(08)70822-X"},{"key":"119339_CR15","unstructured":"Guha, A. and Zhang, H.: Andrews\u2019 Challenge Problem: Clause Conversion and Solutions, AAR Newsletter No. 14, December 1989."},{"key":"119339_CR16","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/3-540-19129-1_4","volume":"306","author":"J.-L. Lassez","year":"1987","unstructured":"Lassez, J.-L., Maher, M. J. and Marriott, K.: Unification revisited, foundations of logic and functional programming, Lecture Notes in Computer Science\n306(1987), 67.","journal-title":"Lecture Notes in Computer Science"},{"key":"119339_CR17","unstructured":"Li Dafa: Unification Algorithm with Quantifiers in the First-Order Logic, Science Report 89005, Dept. of Applied Mathematics of Tsinghua University, Nov. 1989."},{"key":"119339_CR18","unstructured":"Li Dafa: Unification algorithm with quantifiers and applications to automatic natural deduction, in Proc. 4th Florida Artificial Intelligence Research Symposium, 1992, pp. 196\u2013200."},{"key":"119339_CR19","doi-asserted-by":"crossref","unstructured":"Li Dafa: A natural deduction automated theorem proving system, in Proc. 11th International Conference on Automated Deduction, NY, June 15\u201318, 1992, pp. 668\u2013672.","DOI":"10.1007\/3-540-55602-8_200"},{"key":"119339_CR20","unstructured":"Li Dafa: A Mechanical Proof of the Halting Problem, AAR Newsletter No. 23, June 1993."},{"key":"119339_CR21","unstructured":"Li Dafa: The Algorithms for Eliminating and Introducing Quantifiers, Science Report 93019, Dept. of Applied Mathematics of Tsinghua University, Nov. 1993."},{"key":"119339_CR22","unstructured":"Li Dafa: The algorithms for eliminating and introducing quantifiers, in Proc. PRICAI\u201994: The 3rd Pacific Rim International Conference on Artificial Intelligence, Beijing, Aug. 15\u201318, 1994, pp. 208\u2013214."},{"key":"119339_CR23","unstructured":"Li Dafa: The Formalization of the Halting Problem is Not Suitable for Describing the Halting Problem, AAR Newsletter No. 27, October 1994."},{"key":"119339_CR24","doi-asserted-by":"crossref","unstructured":"Lincoln, P. D. and Shankar, N.: Proof search in first-order linear logic and other cut-free sequent calculi, in Proc. Symposium on Logic in Computer Science, 1994, pp. 282\u2013291.","DOI":"10.1109\/LICS.1994.316061"},{"key":"119339_CR25","volume-title":"Mathematical Theory of Computation","author":"Z. Manna","year":"1974","unstructured":"Manna, Z.: Mathematical Theory of Computation, McGraw-Hill, New York, 1974."},{"key":"119339_CR26","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A. and Montanari, U.: An efficient unification algorithm, in ACM Trans. on Pro-gramming Languages and Systems4, No. 2 (April 1982), pp. 258\u2013282.","journal-title":"ACM Trans. on Pro-gramming Languages and Systems"},{"key":"119339_CR27","volume-title":"Computation: Finite and Infinite Machines","author":"M. L. Minsky","year":"1967","unstructured":"Minsky, M. L.: Computation: Finite and Infinite Machines, Prentice-Hall, Englewood Cliffs, NJ, 1967."},{"key":"119339_CR28","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M. S. Pasterson","year":"1978","unstructured":"Pasterson, M. S. and Wegman, M. N.: Linear unification, J. Comp. Sys. Sci.\n16(1978), 158\u2013167.","journal-title":"J. Comp. Sys. Sci."},{"key":"119339_CR29","doi-asserted-by":"crossref","first-page":"257","DOI":"10.1016\/0004-3702(89)90035-0","volume":"38","author":"D. Pastre","year":"1989","unstructured":"Pastre, D.: MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics, Art. Intelligence\n38(1989), 257\u2013318.","journal-title":"Art. Intelligence"},{"key":"119339_CR30","series-title":"Technical Report","volume-title":"Further Developments in THINKER, an Automated Theorem Prover: Proof Condensation, Adding Identity, \u2018Empirical\u2019 Issues in Computational Complexity, Pseudo-Parallel Subproof Development","author":"J. Pelletier","year":"1987","unstructured":"Pelletier, J.: Further Developments in THINKER, an Automated Theorem Prover: Proof Condensation, Adding Identity, \u2018Empirical\u2019 Issues in Computational Complexity, Pseudo-Parallel Subproof Development, Technical Report TR-ARP-16\/87, Dept. of Computer Science, University of Alberta, Canada, 1987."},{"key":"119339_CR31","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"J. Pelletier","year":"1986","unstructured":"Pelletier, J.: Seventy-five problems for testing automatic theorem provers, J. Auto. Reas.\n2 (1986), 191\u2013216.","journal-title":"J. Auto. Reas."},{"issue":"1","key":"119339_CR32","doi-asserted-by":"crossref","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, JACM\n12(1) (1965), 23\u201341.","journal-title":"JACM"},{"key":"119339_CR33","unstructured":"Sahlin, D., Franzen, T. and Haridi, S.: An Intuitionistic Predicate Logic Theorem Prover, SICS Research Report R89001, ISSN 0283-3638, Swedish Institute of Computer Science, 1989."},{"key":"119339_CR34","first-page":"1","volume-title":"7th International Conference on Automated Deduction, Lecture Notes in Computer Science","author":"J. H. Siekmann","year":"1984","unstructured":"Siekmann, J. H.: Universal unification, in R. E. Shostak (ed.), 7th International Conference on Automated Deduction, Lecture Notes in Computer Science 170, Springer-Verlag, Berlin, 1984, pp. 1\u201342."},{"issue":"2","key":"119339_CR35","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/0743-1066(88)90015-5","volume":"5","author":"J. Staples","year":"1988","unstructured":"Staples, J. and Robinson, P. J.: Efficient unification of quantified terms, J. Log. Prog.5(2) (1988), 133\u2013149.","journal-title":"J. Log. Prog."},{"key":"119339_CR36","unstructured":"Van Vaalen, J.: An extension of unification to substitution with an application to automatic theorem proving, in\u00f6 4th International Joint Conference on Artificial Intelligence, 1975, pp. 77\u201382."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005749401809.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005749401809\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005749401809.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:46:27Z","timestamp":1749123987000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005749401809"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,2]]},"references-count":36,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1997,2]]}},"alternative-id":["119339"],"URL":"https:\/\/doi.org\/10.1023\/a:1005749401809","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1997,2]]}}}