{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:46:07Z","timestamp":1725453967440},"publisher-location":"Berlin\/Heidelberg","reference-count":26,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540115587"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0000054","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T06:26:23Z","timestamp":1128493583000},"page":"109-131","source":"Crossref","is-referenced-by-count":2,"title":["Procedure implementation through demodulation and related tricks"],"prefix":"10.1007","author":[{"given":"S. K.","family":"Winker","sequence":"first","affiliation":[]},{"given":"L.","family":"Wos","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","first-page":"321","volume-title":"Machine Intelligence, Vol. 5","author":"J. Allen","year":"1970","unstructured":"Allen, J. and Luckham, D., \u201cAn interactive theorem-proving program,\u201d Machine Intelligence, Vol. 5(1970), Meltzer and Michie (eds), American Elsevier, New York, pp. 321\u2013336."},{"issue":"1","key":"6_CR2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1305\/ndjfl\/1093888216","volume":"19","author":"J. Kalman","year":"1978","unstructured":"Kalman, J., \u201cA shortest single axiom for the classical equivalential calculus,\u201d Notre Dame Journal of Formal Logic, Vol. 19, No. 1, January 1978, pp. 141\u2013144.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"6_CR3","first-page":"145","volume":"1","author":"J. Lukasiewicz","year":"1939","unstructured":"Lukasiewicz, J., \u201cDer Aquivalenzenkalkul,\u201d Collectanea Logica, Vol. 1 (1939), pp. 145\u2013169. English translation in [McCall], pp. 88\u2013115 and in [Lukasiewicz\/Borkowski], pp. 250\u2013277.","journal-title":"Collectanea Logica"},{"key":"6_CR4","volume-title":"Jan Lukasiewicz: Selected Works","author":"J. Lukasiewicz","year":"1970","unstructured":"Lukasiewicz, J., Jan Lukasiewicz: Selected Works, ed. by L. Borkowski, North-Holland Publishing Co., Amsterdam (1970)."},{"key":"6_CR5","first-page":"232","volume-title":"Vol. 87, Lecture Notes in Computer Science","author":"E. Lusk","year":"1980","unstructured":"Lusk, E. and Overbeek, R., \u201cData structures and control architecture for implementation of theorem-proving programs,\u201d 5th Conference on Automated Deduction, Vol. 87, Lecture Notes in Computer Science, ed. W. Bibel and R. Kowalski, Springer-Verlag, Berlin, 1980, pp. 232\u2013249."},{"key":"6_CR6","unstructured":"Lusk, E., \u201cInput translator for the environmental theorem prover \u2014 user's guide,\u201d to be published as an Argonne National Laboratory technical report."},{"key":"6_CR7","volume-title":"Polish Logic, 1920\u20131939","author":"S. McCall","year":"1967","unstructured":"McCall, S., Polish Logic, 1920\u20131939, Clarendon Press, Oxford (1967)."},{"key":"6_CR8","doi-asserted-by":"crossref","first-page":"773","DOI":"10.1109\/TC.1976.1674696","volume":"25","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R. and Wos, L., \u201cProblems and experiments for and with automated theorem proving programs,\u201d IEEE Transactions on Computers, Vol. C-25(1976), pp. 773\u2013782.","journal-title":"IEEE Transactions on Computers"},{"key":"6_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","volume":"2","author":"J. McCharen","year":"1976","unstructured":"McCharen, J., Overbeek, R. and Wos, L., \u201cComplexity and related enhancements for automated theorem-proving programs,\u201d Computers and Mathematics with Applications, Vol. 2(1976), pp. 1\u201316.","journal-title":"Computers and Mathematics with Applications"},{"key":"6_CR10","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0898-1221(75)90019-X","volume":"1","author":"R. Overbeek","year":"1975","unstructured":"Overbeek, R., \u201cAn implementation of hyper-resolution,\u201d Computers and Mathematics with Applications, Vol. 1(1975), pp. 201\u2013214.","journal-title":"Computers and Mathematics with Applications"},{"key":"6_CR11","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1305\/ndjfl\/1093887534","volume":"17","author":"J. Peterson","year":"1976","unstructured":"Peterson, J., \u201cShortest single axioms for the equivalential calculus,\u201d Notre Dame Journal of Formal Logic, Vol. 17(1976), pp. 267\u2013271.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"6_CR12","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1305\/ndjfl\/1093888213","volume":"XIX","author":"J. Peterson","year":"1978","unstructured":"Peterson, J., \u201cAn automatic theorem prover for substitution and detachment systems,\u201d Notre Dame Journal of Formal Logic, Vol. XIX, Jan. 1978, pp. 119\u2013122.","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. Robinson","year":"1965","unstructured":"Robinson, J., \u201cA machine-oriented logic based on the resolution principle,\u201d J. ACM, Vol. 12(1965), pp. 23\u201341.","journal-title":"J. ACM"},{"key":"6_CR14","first-page":"227","volume":"1","author":"J. Robinson","year":"1965","unstructured":"Robinson, J., \u201cAutomatic deduction with hyper-resolution,\u201d International Journal of Computer Mathematics, Vol. 1(1965), pp. 227\u2013234.","journal-title":"International Journal of Computer Mathematics"},{"key":"6_CR15","unstructured":"Smith, B., \u201cReference manual for the environmental theorem prover,\u201d to be published as an Argonne National Laboratory technical report."},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Veroff, R., \u201cCanonicalization and demodulation,\u201d Argonne National Laboratory, Technical Report ANL-81-6, Argonne, Illinois, February 1981.","DOI":"10.2172\/6898399"},{"key":"6_CR17","first-page":"251","volume-title":"Automated generation of models and counterexamples and its application to open questions in ternary Boolean algebra","author":"S. Winker","year":"1978","unstructured":"Winker, S. and Wos, L., \u201cAutomated generation of models and counterexamples and its application to open questions in ternary Boolean algebra,\u201d Proc. of the Eighth International Symposium on Multiple-valued Logic, Rosemont, Illinois, 1978, IEEE and ACM Publ., pp. 251\u2013256."},{"key":"6_CR18","first-page":"533","volume":"37","author":"S. Winker","year":"1981","unstructured":"Winker, S., Wos, L. and Lusk, E., \u201cSemigroups, antiautomorphisms, and involutions: a computer solution to an open problem, I,\u201d Mathematics of Computation, Vol. 37 (1981), pp. 533\u2013545.","journal-title":"Mathematics of Computation"},{"key":"6_CR19","unstructured":"Winker, S., \u201cGeneration and verification of finite models and counterexamples using an automated theorem prover answering two open questions,\u201d to appear in J. ACM."},{"key":"6_CR20","unstructured":"Winker, S., Wos, L. and Lusk, E., \u201cSemigroups, anti automorphisms, and involutions: a computer solution to an open problem, II,\u201d in preparation."},{"key":"6_CR21","unstructured":"Wojciechowski, W. and Wojcik, A., \u201cMultiple-valued logic design by theorem proving,\u201d Proc. of the Ninth International Symposium on Multiple-valued Logic, Bath, England, 1979."},{"key":"6_CR22","first-page":"615","volume-title":"Proc. of the Fall Joint Computer Conference","author":"L. Wos","year":"1964","unstructured":"Wos, L., Carson, D. and Robinson, G., \u201cThe unit preference strategy in theorem proving,\u201d Proc. of the Fall Joint Computer Conference, 1964, Thompson Book Company, New York, pp. 615\u2013621."},{"key":"6_CR23","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"Wos, L., Carson, D. and Robinson, G., \u201cEfficiency and completeness of the set-of-support strategy in theorem proving,\u201d J. ACM, Vol. 12(1965), pp. 536\u2013541.","journal-title":"J. ACM"},{"key":"6_CR24","doi-asserted-by":"publisher","first-page":"698","DOI":"10.1145\/321420.321429","volume":"14","author":"L. Wos","year":"1967","unstructured":"Wos, L., Robinson, G., Carson, D. and Shalla, L., \u201cThe concept of demodulation in theorem proving,\u201d J. ACM, Vol. 14(1967), pp. 698\u2013709.","journal-title":"J. ACM"},{"key":"6_CR25","series-title":"National Computer Conference","first-page":"697","volume-title":"AFIPS Conference Proceedings, Vol. 50","author":"L. Wos","year":"1981","unstructured":"Wos, L., Winker, S., and Lusk, E., \u201cAn automated reasoning system,\u201d AFIPS Conference Proceedings, Vol. 50 (1981), National Computer Conference (Chicago, Ill., 1981), AFIPS Press, pp. 697\u2013702."},{"key":"6_CR26","unstructured":"Wos, L., Winker, S., Veroff, R., Smith, B. and Henschen, L., \u201cQuestions concerning possible shortest single axioms in equivalential calculus: an application of automated theorem proving to infinite domains,\u201d submitted to the Notre Dame Journal of Formal Logic for consideration for publication, May 1981."}],"container-title":["Lecture Notes in Computer Science","6th Conference on Automated Deduction"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0000054.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T09:43:05Z","timestamp":1607334185000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000054"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540115587"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0000054","relation":{},"subject":[]}}