{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:46:12Z","timestamp":1725453972562},"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\/bfb0000067","type":"book-chapter","created":{"date-parts":[[2005,10,5]],"date-time":"2005-10-05T10:26:23Z","timestamp":1128507983000},"page":"309-325","source":"Crossref","is-referenced-by-count":2,"title":["Proof by matrix reduction as plan + validation"],"prefix":"10.1007","author":[{"given":"Ricardo","family":"Caferra","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"19_CR1","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"ANDREWS P.B.: \u201cTheorem proving via general mating\u201d, JACM, Vol.28 N\u22182, April 1981 (193\u2013214).","journal-title":"JACM"},{"key":"19_CR2","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1016\/0304-3975(79)90054-9","volume":"8","author":"W. Bibel","year":"1979","unstructured":"BIBEL W.: \u201cTautology testing with a generalized matrix reduction method\u201d, Theoretical Computer Science 8, 1979 (31\u201344).","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"19_CR3","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"BIBEL W.: \u201cOn matrices with connections\u201d, JACM, Vol.28 N\u22184, October 1981 (633\u2013645).","journal-title":"JACM"},{"key":"19_CR4","unstructured":"CHANG C. and LEE R.: \u201cSymbolic logic and mechanical theorem proving\u201d, Academic Press, 1973."},{"key":"19_CR5","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0004-3702(79)90015-8","volume":"12","author":"C. Chang","year":"1979","unstructured":"CHANG C. and SLAGLE J.R.: \u201cUsing rewriting rules for connection graphs to prove theorems\u201d, Artificial Intelligence 12, 1979 (159\u2013180).","journal-title":"Artificial Intelligence"},{"key":"19_CR6","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1090\/psapm\/015\/0170497","volume":"15","author":"M. Davis","year":"1963","unstructured":"DAVIS M.: \u201cEliminating the irrelevant from mechanical proofs\u201d, Symposia in Applied Mathematics Vol.15, 1963 (15\u201330).","journal-title":"Symposia in Applied Mathematics"},{"issue":"3","key":"19_CR7","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/322139.322140","volume":"26","author":"L.J. Henschen","year":"1979","unstructured":"HENSCHEN L.J.: \u201cTheorem proving by covering expressions\u201d, JACM, Vol.26, N\u22183, July 1979 (385\u2013400).","journal-title":"JACM"},{"key":"19_CR8","unstructured":"HUET G.: \u201cR\u00e9solution d'\u00e9quations dans les langages d'ordre 1,2,...,\u03c9\u201d, Th\u00e8se d'\u00e9tat, Universit\u00e9 Paris VII, 1976."},{"key":"19_CR9","unstructured":"KLEENE S.: \u201cMathematical logic\u201d, John Wiley and Sons, 1967."},{"key":"19_CR10","unstructured":"KOWALSKI R.: \u201cLogic for problem solving\u201d, North-Holland 1979."},{"issue":"2","key":"19_CR11","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D.W. Loveland","year":"1968","unstructured":"LOVELAND D.W.: \u201cMechanical theorem proving by model elimination\u201d, JACM, Vol.15, N\u22182, April 1968 (236\u2013251).","journal-title":"JACM"},{"issue":"2","key":"19_CR12","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1145\/321694.321706","volume":"19","author":"D.W. Loveland","year":"1972","unstructured":"LOVELAND D.W.: \u201cA unified view of some linear Herbrand procedures\u201d, JACM, Vol.19, N\u22182, April 1972 (366\u2013384).","journal-title":"JACM"},{"key":"19_CR13","unstructured":"LOVELAND D. W.: \u201cAutomated theorem proving: A Logical basis\u201d, North-Holland, 1978."},{"key":"19_CR14","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/0004-3702(81)90015-1","volume":"16","author":"D.A. Plaisted","year":"1981","unstructured":"PLAISTED D.A.: \u201cTheorem proving with abstraction\u201d, Artificial Intelligence 16, 1981 (47\u2013108).","journal-title":"Artificial Intelligence"},{"key":"19_CR15","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"PRAWITZ D.: \u201cAn improved proof procedure\u201d, Theoria 26, 1960 (102\u2013139).","journal-title":"Theoria"},{"key":"19_CR16","unstructured":"PRAWITZ D.: \u201cAdvances and problems in mechanical proof procedures\u201d, Machine Intelligence 4, Edinburgh Univ. Press 1969, (59\u201371)."},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"PRAWITZ D.: \u201cA proof procedure with matrix reduction\u201d, Symposium on Automatic Demonstration-Springer Verlag 1970 (207\u2013214).","DOI":"10.1007\/BFb0060634"},{"issue":"1","key":"19_CR18","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"ROBINSON J.A.: \u201cA machine oriented logic based on the resolution principle\u201d, JACM, Vol.12, N\u22181, January 1965 (23\u201341).","journal-title":"JACM"},{"key":"19_CR19","volume-title":"Logic: form and function, the mechanization of deductive reasoning","author":"J.A. Robinson","year":"1979","unstructured":"ROBINSON J.A.: \u201cLogic: form and function, the mechanization of deductive reasoning\u201d, University Press Edinburgh, 1979."},{"key":"19_CR20","unstructured":"ROUSSELL Ph.: \u201cProlog: Manuel de R\u00e9f\u00e9rence et d'Utilisation\u201d, Groupe d'Intelligence Artificielle, Universit\u00e9 d'Aix Marseille, Luminy, Sept. 1975."},{"key":"19_CR21","unstructured":"SAYA H.: \u201cCompl\u00e9tude de la strat\u00e9gie du support dans la m\u00e9thode de r\u00e9duction matricielle\u201d, R.R. Imag N\u221893, Novembre 1977."},{"key":"19_CR22","unstructured":"SAYA H. and CAFERRA R.: \u201cA structure sharing technique for matrices and substitutions in Prawitz's theorem proving method\u201d, R.R. IMAG N\u2218101, Decem. 1977."},{"key":"19_CR23","first-page":"371","volume":"2","author":"H. Saya","year":"1978","unstructured":"SAYA H. et CAFERRA R.: \u201cRepr\u00e9sentation compacte de matrices et traitement de l'\u00e9galit\u00e9 formelle dans la m\u00e9thode de Prawitz de d\u00e9monstration automatique\u201d, Congr\u00e8s AFCET 1978, tome 2 (371\u2013381).","journal-title":"Congr\u00e8s AFCET"},{"key":"19_CR24","unstructured":"SHOSTAK R.E.: \u201cA graph-theoretic view of resolution theorem proving\u201d, TR-20-74 Center of Research in Computing Technology-Harvard University 1974."},{"issue":"8","key":"19_CR25","doi-asserted-by":"crossref","first-page":"823","DOI":"10.1109\/TC.1976.1674701","volume":"25","author":"S. Sickel","year":"1976","unstructured":"SICKEL S.: \u201cA search technique for clause Interconnectivity Graphs\u201d, IEEE Transactions on Computers, Vol.C-25 N\u22188 August 1976 (823\u2013835).","journal-title":"IEEE Transactions on Computers"},{"key":"19_CR26","unstructured":"SICKEL S.: \u201cVariable range restrictions in resolution theorem proving\u201d, Machine Intelligence 8-Ellis Horwood Ltd 1977 (73\u201385)."}],"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\/BFb0000067.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,7]],"date-time":"2020-12-07T14:43:10Z","timestamp":1607352190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0000067"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540115587"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0000067","relation":{},"subject":[]}}