{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:46Z","timestamp":1761611146478},"reference-count":27,"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\/bf00881869","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T18:44:45Z","timestamp":1104173085000},"page":"293-314","source":"Crossref","is-referenced-by-count":17,"title":["SET-VAR"],"prefix":"10.1007","volume":"11","author":[{"given":"W. W.","family":"Bledsoe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guohui","family":"Feng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Bledsoe, W. W., ?A maximal method for set variables in automatic theorem proving?,Proceedings of IJCAI-77, MIT, August 1977, pp. 501?510. AlsoMachine Intelligence 9, J. E. Hayes, D. Michie, L. I. Mikulich (Eds.), Chichester: Ellis Horwood Ltd. and New York: John Wiley, pp. 53?100 (1979)."},{"key":"CR2","first-page":"281","volume-title":"Proc. 5th Conf. on Automated Deduction","author":"W. W. Bledsoe","year":"1990","unstructured":"Bledsoe, W. W., and Hines, L., ?Variable elimination and chaining in a resolution-based prover for inequalities?,Proc. 5th Conf. on Automated Deduction, Bibel and J. Kowalski, (Eds.), New York: Springer-Verlag, pp. 281?292 (1990). Bledsoe, W. W. and Hines, L. M., ?The STR + VE prover?, Univ. of Texas CS Dept. Memo ATP 94, August (1989)."},{"key":"CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/3-540-52885-7_88","volume-title":"Proc. 10th International Conf. on Automated Deduction","author":"L. M. Hines","year":"1990","unstructured":"Hines, L. M., ?STR + VE-subset: The STR + VE subset prover?,Proc. 10th International Conf. on Automated Deduction, Berlin: Springer-Verlag, pp. 193?206 (1990)."},{"key":"CR4","first-page":"35","volume-title":"Proc. 11th International Conference on Automated Deduction","author":"L. M. Hines","year":"1992","unstructured":"Hines, L. M., ?The central variable strategy of STR + VE?,Proc. 11th International Conference on Automated Deduction, New York: Springer-Verlag, pp. 35?49 (1992)."},{"key":"CR5","unstructured":"Bledsoe, W. W., ?The paracompactness theorem?, Univ. of Texas CS Dept. Memo, ATP 96, June (1989)."},{"key":"CR6","unstructured":"Feng, Guohui, ?Hand proofs of the compact-Hausdorff-regular theorem and the attains maximum theorem?, Univ. of Texas CS Dept. Memo, ATP 98, August (1989)."},{"key":"CR7","first-page":"51","volume":"5","author":"W. W. Bledsoe","year":"1974","unstructured":"Bledsoe, W. W., and Bruell, P., ?A man-machine theorem proving system?,AI J. 5 51?72 (1974). Bledsoe, W. W., and Mabry Tyson, The UT Interactive Prover. Univ. of Texas, Math. Dept. Memos ATP17A & ATP17B.","journal-title":"AI J."},{"key":"CR8","unstructured":"Minor, John T., ?Proving a subset of second-order logic by reduction to first-order logic?, Dept. of Computer Science, UNLV, August 15 (1991). Accepted for publication byJ. Automated Reasoning."},{"key":"CR9","unstructured":"Minor, John T., ?Proving a subset of second-order logic with first-order logic proof procedures?, PhD Dissertation. Univ. of Texas at Austin, August (1979)."},{"key":"CR10","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/BF01457985","volume":"86","author":"H. Behmann","year":"1922","unstructured":"Behmann, H., ?Beitrage zur Algebra der Logik, insbesondere zum Entscheidungsproblem?,Math. Annalen 86 163?229 (1922).","journal-title":"Math. Annalen"},{"key":"CR11","unstructured":"Ackermann, W.,Solvable Cases of the Decision Problem, North Holland (1954)."},{"key":"CR12","volume-title":"Z-match: For incrementally constructuing set instantiations","author":"D. Baker-Plummer","year":"1991","unstructured":"Baker-Plummer, D., and Bailin, S. C., ?Z-match: For incrementally constructuing set instantiations?, Swarthmore College, Swarthmore, Penn., and CTA Inc., Rockville, Maryland (1991)."},{"key":"CR13","unstructured":"Andrews, P. B.,An Introduction to Mathematical Logic and Type Theory, Academic Press, 1986. Andrews, P. B., ?On connections and higher order Logic?,J. Automated Reasoning 5, 257?291 (1989). Andrews, P. B.,et al., ?The TPC theorem proving system?,Proc. CADE-10, Berlin: Springer-Verlag, pp. 641?642 (1990)."},{"key":"CR14","unstructured":"Kerber, M., ?How to prove higher order theorems in first-order logic?,Proc. IJCAI-91, Morgan Kaufmann, pp. 137?142 (1991)."},{"key":"CR15","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":"CR16","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1145\/321592.321603","volume":"17","author":"R. Anderson","year":"1970","unstructured":"Anderson, R., and Bledsoe, W. W., ?A linear format for resolution with merging and a new technique for establishing completeness?,JACM 17 525?534 (1970).","journal-title":"JACM"},{"key":"CR17","unstructured":"Miller, Dale A., ?Proofs in higher-order logic?, Dept. Computer and Information Science, Univ. of Pennsylvania, MS-CIS-83-87."},{"key":"CR18","unstructured":"Feng, G., and Ballantyne, M., ?Computing circumscription with SET-VAR methods?, EDS Technical Report AUS-1192-3, EDS Research, Austin lab (1992)."},{"key":"CR19","unstructured":"McCune, W.,OTTER 2 User's Guide, Argonne National Laboratory, ANL-90\/9, 1990. W. McCune, ?What's New in OTTER?. Mathematics and Computer Science Division, ANL\/MCS-TM-153, Argonne National Laboratory (1992)."},{"key":"CR20","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. Wos","year":"1992","unstructured":"Wos, L., Overbeek, R., Lusk, E., and Boyle, J.,Automated Reasoning: Introduction and Applications, 2nd edn., New York: McGraw-Hill (1992).","edition":"2nd edn."},{"key":"CR21","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E., ?A Prolog technology theorem prover: Implementation by an extended Prolog compiler?,J. Automated Reasoning 4 353?380, (1988).","journal-title":"J. Automated Reasoning"},{"key":"CR22","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1007\/978-94-011-3488-0_2","volume-title":"Automated Reasoning: Essays in Honor of Woody Bledsoe","author":"O. L. Astrachan","year":"1991","unstructured":"Astrachan, O. L., and Loveland, D. W., ?METEORs: High performance theorem provers using model elimination?,Automated Reasoning: Essays in Honor of Woody Bledsoe, Robert S. Boyer, (Ed.), Dordrecht: Kluwer Academic Publishers, pp. 31?59 (1991)."},{"key":"CR23","first-page":"25","volume":"9","author":"Shie-Jue Lee","year":"1992","unstructured":"Lee, Shie-Jue, and Plaisted, D. A., ?Eliminating duplication with hyper-linking strategy?,J. Automated Reasoning 9 25?42 (1992).","journal-title":"J. Automated Reasoning"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0004-3702(80)90011-9","volume":"13","author":"J. McCarthy","year":"1980","unstructured":"McCarthy, J., ?Circumscription ? a form of non-monotonic reasoning?,Artificial Intelligence 13 27?39 (1980).","journal-title":"Artificial Intelligence"},{"key":"CR25","unstructured":"Lifshitz, V., ?Circumscription?, inHandbook of Logic in AI and Logic Programming (to appear). ?Computing circumscription?,IJCAI, pp. 465?569 (1985)."},{"key":"CR26","unstructured":"Gabbay, D., and Ohlbach, H., ?Quantifier elimination in second-order predicate logic?,Proc. 3rd International Conference on Principle of Knowledge Representation and Reasoning, 1992."},{"key":"CR27","unstructured":"Bledsoe, W. W., ?SET-VAR implementation?, Univ. of Texas at Austin CS Dept. Memo ATP 115, May (1993)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881869.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881869\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881869","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T08:58:11Z","timestamp":1556528291000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881869"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881869"],"URL":"https:\/\/doi.org\/10.1007\/bf00881869","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}