{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,18]],"date-time":"2023-01-18T20:26:40Z","timestamp":1674073600870},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bf00881874","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T23:44:45Z","timestamp":1104191085000},"page":"391-428","source":"Crossref","is-referenced-by-count":8,"title":["?-match: An inference rule for incrementally elaborating set instantiations"],"prefix":"10.1007","volume":"11","author":[{"given":"Sidney C.","family":"Bailin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dave","family":"Barker-Plummer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"CR1","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/BF00244943","volume":"4","author":"S. C. Bailin","year":"1988","unstructured":"Bailin, S. C., ?A ? unifiability test for set theory?,Journal of Automated Reasoning 4(3) 269?286 (September 1988).","journal-title":"Journal of Automated Reasoning"},{"key":"CR2","series-title":"Technical Report","volume-title":"Completeness ofSet-var","author":"W. W. Bledsoe","year":"1990","unstructured":"Bledsoe, W. W. and Feng, G., ?Completeness ofSet-var?,Technical Report ATP104, University of Texas at Austin, Department of Computer Sciences, Austin, Texas (December 1990)."},{"key":"CR3","series-title":"Technical Report","volume-title":"Soundness and incompleteness results forSet-var","author":"W. W. Bledsoe","year":"1991","unstructured":"Bledsoe, W. W. and Feng, G., ?Soundness and incompleteness results forSet-var?,Technical Report ATP105, University of Texas at Austin, Department of Computer Sciences, Austin, Texas (1991). Draft only."},{"key":"CR4","first-page":"53","volume-title":"Machine Intelligence 9","author":"W. W. Bledsoe","year":"1979","unstructured":"Bledsoe, W. W., ?A maximal method for set variables in automatic theorem proving?, inMachine Intelligence 9, pp. 53?100 Ellis Harwood, Ltd., Chichester (1979)."},{"key":"CR5","unstructured":"Bledsoe, W. W., ?TheUt interactive prover?,Memo ATP-17B, Mathematics Department, University of Texas (April 1983)."},{"key":"CR6","series-title":"Technical Report","volume-title":"The gazer theorem prover: Description and users' guide","author":"D. Barker-Plummer","year":"1989","unstructured":"Barker-Plummer, D., ?The gazer theorem prover: Description and users' guide?,Technical Report CS-1989-15, Department of Computer Science, Duke University, Durham, North Carolina (1989)."},{"key":"CR7","unstructured":"Barker-Plummer, D. and Bailin, S. C., ?Graphical theorem proving: An approach to reasoning with the help of diagrams?, inProceedings European Conference on Artificial Intelligence (ECAI-92), Vienna, Austria, 3?7 August, pp. 55?59. John Wiley and Sons (August 1992)."},{"key":"CR8","unstructured":"Barker-Plummer, D. and Bailin, S. C., ?Proofs and pictures: Proving the diamond lemma with theGrover theorem proving system?, inWorking Notes of the AAAI Symposium on Reasoning with Diagrammatic Representations, March 25?27 1992, Stanford (March 1992)."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Barker-Plummer, D., Bailin, S. C. and Merrill, A. S., ?The & theorem proving system?, in D. Kapur (Ed.),CADE-11, Lecture Notes in Artificial Intelligence, Vol. 607, pp. 716?720.11th International Conference on Automated Deduction (1992).","DOI":"10.1007\/3-540-55602-8_210"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/S0004-3702(78)80017-4","volume":"10","author":"F. M. Brown","year":"1978","unstructured":"Brown, F. M., ?Towards the automation of set theory and its logic?,Artificial Intelligence 10 281?316 (1978).","journal-title":"Artificial Intelligence"},{"key":"CR11","unstructured":"Bledsoe, W. W. and Tyson, M., ?TheUt interactive prover?,Memo ATP-17, Mathematics Department, University of Texas (May 1975)."},{"key":"CR12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(88)90030-6","volume":"35","author":"D. Cvetkovic","year":"1988","unstructured":"Cvetkovic, D. and Pevac, I., ?Man-machine theorem proving in graph theory?,Artificial Intelligence 35 1?23 (May 1988).","journal-title":"Artificial Intelligence"},{"key":"CR13","unstructured":"Gentzen, G., ?Untersuchen \u00fcber das logische schliessen? [Investigations into logical deduction], in M. E. Szabo (Ed.),The Collected Papers of Gerhard Gentzen, Ch. 3, pp. 68?131. North-Holland (1969). First appeared in 1935 as an article inMathematische Zeitschrift 39. This work was accepted as Gentzen's inaugural dissertation at the University of G\u00f6ttingen."},{"key":"CR14","first-page":"606","volume":"4","author":"A. J. Nevins","year":"1974","unstructured":"Nevins, A. J., ?A human oriented logic for automatic theorem proving?,ACM 4 606?621 (1974).","journal-title":"ACM"},{"key":"CR15","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0004-3702(75)90014-4","volume":"6","author":"A. J. Nevins","year":"1975","unstructured":"Nevins, A. J., ?A relaxation approach to splitting in an automatic theorem prover?,Artificial Intelligence 6 25?39 (1975).","journal-title":"Artificial Intelligence"},{"key":"CR16","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?,J. ACM 12 23?41 (1965).","journal-title":"J. ACM"},{"key":"CR17","first-page":"124","volume-title":"From Frege to G\u00f6del: A Sourcebook in Mathematical Logic 1879?1931","author":"B. Russell","year":"1967","unstructured":"Russell, B., Letter to Frege in J. Van Heijenoort (Ed.),From Frege to G\u00f6del: A Sourcebook in Mathematical Logic 1879?1931, Ch. 7, pp. 124?125. Harvard University Press, Cambridge, Massachusetts (1967). This letter is dated 16 June 1902."},{"key":"CR18","unstructured":"Sterling, L. and Shapiro, E.,The Art of Prolog, MIT Press (1986)."},{"issue":"1","key":"CR19","first-page":"93","volume":"5","author":"L. Wos","year":"1989","unstructured":"Wos, L., ?The problem of finding an inference rule for set theory?,Journal of Automated Reasoning 5(1), 93?95 (1989).","journal-title":"Journal of Automated Reasoning"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881874.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881874\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T00:16:22Z","timestamp":1586045782000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881874"],"URL":"https:\/\/doi.org\/10.1007\/bf00881874","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}