{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:58:12Z","timestamp":1725663492975},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540556022"},{"type":"electronic","value":"9783540472520"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55602-8_202","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:21:33Z","timestamp":1330251693000},"page":"677-680","source":"Crossref","is-referenced-by-count":1,"title":["The semantically guided linear deduction system"],"prefix":"10.1007","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"52_CR1","doi-asserted-by":"crossref","first-page":"240","DOI":"10.1145\/800177.810076","volume-title":"Proceedings of the Annual Conference of the ACM (Detroit, MI, 1979)","author":"V.J. Digricoli","year":"1979","unstructured":"Digricoli V.J., Automatic Deduction and Equality, In Martin A.L. (Ed.), Proceedings of the Annual Conference of the ACM (Detroit, MI, 1979) ACM Press, New York, NY, (1979), 240\u2013250."},{"key":"52_CR2","first-page":"349","volume-title":"Journal of the ACM 16(3)","author":"D.W. Loveland","year":"1969","unstructured":"Loveland D.W., A Simplified Format for the Model Elimination Theorem-Proving Procedure, In Journal of the ACM 16(3), ACM Press, New York, NY, (1969), 349\u2013363."},{"key":"52_CR3","first-page":"51","volume-title":"Artificial Intelligence 7","author":"R.E. Shostak","year":"1976","unstructured":"Shostak R.E., Refutation Graphs, In Artificial Intelligence 7, Elsevier Science, Amsterdam, The Netherlands, (1976), 51\u201364."},{"key":"52_CR4","first-page":"675","volume-title":"Lecture Notes in Artificial Intelligence 449","author":"G. Sutcliffe","year":"1990","unstructured":"Sutcliffe G., A General Clause Theorem Prover, In Stickel M.E. (Ed.), Proceedings of the 10th International Conference on Automated Deduction (Kaiserslautern, Germany, 1990), (Siekmann J.H. (Ed.), Lecture Notes in Artificial Intelligence 449), Springer-Verlag, New York, NY, (1990), 675\u2013676."},{"key":"52_CR5","volume-title":"Linear-Input Subset Analysis","author":"G. Sutcliffe","year":"1992","unstructured":"Sutcliffe G., Linear-Input Subset Analysis, In Kapur D. (Ed.), Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, NY, 1992) Springer-Verlag, New York, NY, (1992)."}],"container-title":["Lecture Notes in Computer Science","Automated Deduction\u2014CADE-11"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55602-8_202.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:32:59Z","timestamp":1619573579000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_202"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_202","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}