{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T22:25:44Z","timestamp":1762295144283},"reference-count":38,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1984,4,1]],"date-time":"1984-04-01T00:00:00Z","timestamp":449625600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[1984,4]]},"DOI":"10.1016\/0004-3702(84)90054-7","type":"journal-article","created":{"date-parts":[[2003,3,14]],"date-time":"2003-03-14T13:02:52Z","timestamp":1047646972000},"page":"303-356","source":"Crossref","is-referenced-by-count":22,"title":["A new use of an automated reasoning assistant: Open questions in equivalential calculus and the study of infinite domains"],"prefix":"10.1016","volume":"22","author":[{"given":"L.","family":"Wos","sequence":"first","affiliation":[]},{"given":"S.","family":"Winker","sequence":"additional","affiliation":[]},{"given":"B.","family":"Smith","sequence":"additional","affiliation":[]},{"given":"R.","family":"Veroff","sequence":"additional","affiliation":[]},{"given":"L.","family":"Henschen","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0004-3702(84)90054-7_BIB1","first-page":"321","article-title":"An interactive theorem-proving program","volume":"5","author":"Allen","year":"1970"},{"key":"10.1016\/0004-3702(84)90054-7_BIB2","first-page":"173","article-title":"The two-property","volume":"1","author":"Belnap","year":"1976","journal-title":"Relevance Logic Newsletter"},{"key":"10.1016\/0004-3702(84)90054-7_BIB3","series-title":"A Spectrum of Mathematics, Essays Presented to H.G. Forder","first-page":"22","article-title":"Substitution-and-detachment systems related to abelian groups; with an appendix by C.A. Meredith","author":"Kalman","year":"1971"},{"key":"10.1016\/0004-3702(84)90054-7_BIB4","first-page":"181","article-title":"Computer studies of T \u2192 - W - I","volume":"1","author":"Kalman","year":"1976","journal-title":"Relevance Logic Newsletter"},{"key":"10.1016\/0004-3702(84)90054-7_BIB5","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1112\/jlms\/s2-14.2.193","article-title":"Axiomatizations of logics with values in groups","volume":"14","author":"Kalman","year":"1976","journal-title":"J. London Math. Soc."},{"issue":"1","key":"10.1016\/0004-3702(84)90054-7_BIB6","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1305\/ndjfl\/1093888216","article-title":"A shortest single axiom for the classical equivalential calculus","volume":"19","author":"Kalman","year":"1978","journal-title":"Notre Dame. J. Formal Logic"},{"key":"10.1016\/0004-3702(84)90054-7_BIB7","unstructured":"Kalman, J., private communication."},{"key":"10.1016\/0004-3702(84)90054-7_BIB8_1","first-page":"145","article-title":"Der \u00c4quivalenzenkalk\u00fcl","volume":"1","author":"Lukasiewicz","year":"1939","journal-title":"Collectanea Logica"},{"key":"10.1016\/0004-3702(84)90054-7_BIB8_2","first-page":"88","article-title":"Der \u00c4quivalenzenkalk\u00fcl","volume":"10","author":"Lukasiewicz","year":"1939","journal-title":"Collectanea Logica"},{"key":"10.1016\/0004-3702(84)90054-7_BIB8_3","first-page":"250","article-title":"Der \u00c4quivalenzenkalk\u00fcl","volume":"9","author":"Lukasiewicz","year":"1939","journal-title":"Collectanea Logica"},{"key":"10.1016\/0004-3702(84)90054-7_BIB9","year":"1970"},{"key":"10.1016\/0004-3702(84)90054-7_BIB10","author":"McCall","year":"1967"},{"key":"10.1016\/0004-3702(84)90054-7_BIB11","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","article-title":"Problems and experiments for and with automated theorem proving programs","volume":"25","author":"McCharen","year":"1976","journal-title":"IEEE Trans. Comput."},{"key":"10.1016\/0004-3702(84)90054-7_BIB12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","article-title":"Complexity and related enhancements for automated theorem-proving programs","volume":"2","author":"McCharen","year":"1976","journal-title":"Comput. Math. Appl."},{"issue":"3","key":"10.1016\/0004-3702(84)90054-7_BIB13","first-page":"155","article-title":"Single axioms for the systems (C, N), (C, 0) and (A, N) of the two-valued propositional calculus","volume":"i","author":"Meredith","year":"1953","journal-title":"J. Comput. Systems"},{"key":"10.1016\/0004-3702(84)90054-7_BIB14","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1305\/ndjfl\/1093957574","article-title":"Notes on the axiomatics of the Propositional Calculus","volume":"4","author":"Meredith","year":"1963","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/0004-3702(84)90054-7_BIB15","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1305\/ndjfl\/1093887534","article-title":"Shortest single axioms for the equivalential calculus","volume":"17","author":"Peterson","year":"1976","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/0004-3702(84)90054-7_BIB16","article-title":"The possible shortest single axioms for EC-tautologies","author":"Peterson","year":"1977","journal-title":"Auckland University Department of Mathematics Report Series No. 105"},{"key":"10.1016\/0004-3702(84)90054-7_BIB17","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1305\/ndjfl\/1093888213","article-title":"An automatic theorem prover for substitution and detachment systems","volume":"19","author":"Peterson","year":"1978","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/0004-3702(84)90054-7_BIB18","article-title":"Single axioms for the classical equivalential calculus","author":"Peterson","year":"1976","journal-title":"Auckland University Department of Mathematics Report Series No. 78"},{"key":"10.1016\/0004-3702(84)90054-7_BIB19","author":"Prior","year":"1962"},{"key":"10.1016\/0004-3702(84)90054-7_BIB20","author":"Quine","year":"1959"},{"key":"10.1016\/0004-3702(84)90054-7_BIB21","first-page":"135","article-title":"Paramodulation and theorem proving in first-order theories with equality","volume":"4","author":"Robinson","year":"1969"},{"key":"10.1016\/0004-3702(84)90054-7_BIB22","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(84)90054-7_BIB23","first-page":"125","article-title":"Uber die mathematische Logic","volume":"10","author":"Skolem","year":"1928","journal-title":"Norsk Mathematisk Tidskrift"},{"key":"10.1016\/0004-3702(84)90054-7_BIB24","unstructured":"Smith, B., Reference manual for the environmental theorem prover, an incarnation of AURA, Argonne National Laboratory Tech. Rept. Argonne, IL (to appear)."},{"key":"10.1016\/0004-3702(84)90054-7_BIB25","series-title":"Proc. Eighth International Symposium on Multiple-valued Logic","first-page":"251","article-title":"Automated generation of models and counterexamples and its application to open questions in ternary Boolean algebra","author":"Winker","year":"1978"},{"key":"10.1016\/0004-3702(84)90054-7_BIB26","first-page":"533","article-title":"Semigroups, antiautomorphisms, and involutions: a computer solution to an open problem, I","volume":"37","author":"Winker","year":"1981","journal-title":"Math. Comp."},{"key":"10.1016\/0004-3702(84)90054-7_BIB27","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/322307.322308","article-title":"Generation and verification of finite models and counterexamples using an automated theorem prover answering two open questions","volume":"29","author":"Winker","year":"1982","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(84)90054-7_BIB28","series-title":"6th Conf. Automated Deduction","first-page":"109","article-title":"Procedure implementation through demodulation and related tricks","volume":"Vol. 138","author":"Winker","year":"1982"},{"key":"10.1016\/0004-3702(84)90054-7_BIB29","unstructured":"Winker, S. and Wos, L., New shortest single axioms for the equivalential calculus, in preparation."},{"key":"10.1016\/0004-3702(84)90054-7_BIB30","article-title":"Some theorem-proving strategies and their implementation","author":"Wos","year":"1964"},{"key":"10.1016\/0004-3702(84)90054-7_BIB31","series-title":"Proc. Fall Joint Computer Conference","first-page":"615","article-title":"The unit preference strategy in theorem proving","author":"Wos","year":"1964"},{"key":"10.1016\/0004-3702(84)90054-7_BIB32","doi-asserted-by":"crossref","first-page":"698","DOI":"10.1145\/321420.321429","article-title":"The concept of demodulation in theorem proving","volume":"14","author":"Wos","year":"1967","journal-title":"J. ACM"},{"key":"10.1016\/0004-3702(84)90054-7_BIB33","series-title":"National Computer Conference","first-page":"697","article-title":"An automated reasoning system","volume":"Vol. 50","author":"Wos","year":"1981"},{"key":"10.1016\/0004-3702(84)90054-7_BIB34","series-title":"6th Conference on Automated Deduction","first-page":"1","article-title":"Solving open questions with an automated theorem-proving program","volume":"Vol. 138","author":"Wos","year":"1982"},{"issue":"2","key":"10.1016\/0004-3702(84)90054-7_BIB35","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1305\/ndjfl\/1093870311","article-title":"Questions concerning possible shortest single axioms for the equivalential calculus: an application of automated theorem proving to infinite domains","volume":"24","author":"Wos","year":"1983","journal-title":"Notre Dame J. Formal Logic"},{"key":"10.1016\/0004-3702(84)90054-7_BIB36","author":"Wos","year":"1984"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370284900547?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0004370284900547?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,26]],"date-time":"2019-03-26T23:51:20Z","timestamp":1553644280000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0004370284900547"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984,4]]},"references-count":38,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1984,4]]}},"alternative-id":["0004370284900547"],"URL":"https:\/\/doi.org\/10.1016\/0004-3702(84)90054-7","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1984,4]]}}}