{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:48:06Z","timestamp":1749124086445},"publisher-location":"Berlin, Heidelberg","reference-count":27,"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_171","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:19:28Z","timestamp":1330251568000},"page":"268-280","source":"Crossref","is-referenced-by-count":5,"title":["Linear-input subset analysis"],"prefix":"10.1007","author":[{"given":"Geoff","family":"Sutcliffe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"21_CR1","first-page":"367","volume-title":"Journal of the ACM 15(3)","author":"P.B. Andrews","year":"1968","unstructured":"Andrews P.B., Resolution with Merging, In Journal of the ACM 15(3), ACM Press, New York, NY, (1968), 367\u2013381."},{"key":"21_CR2","volume-title":"SLM, Internal Memo #72","author":"F.M. Brown","year":"1974","unstructured":"Brown F.M., SLM, Internal Memo #72, Department of Artificial Intelligence, University of Edinburgh, Edinburgh, Scotland, (1974)."},{"key":"21_CR3","volume-title":"The Computer Modelling of Mathematical Reasoning","author":"A. Bundy","year":"1983","unstructured":"Bundy A., The Computer Modelling of Mathematical Reasoning, Academic Press, London, England, (1983)."},{"key":"21_CR4","first-page":"698","volume-title":"Journal of the ACM 17(4)","author":"C-L. Chang","year":"1970","unstructured":"Chang C-L., The Unit Proof and the Input Proof in Theorem Proving, In Journal of the ACM 17(4), ACM Press, New York, NY, (1970), 698\u2013707."},{"key":"21_CR5","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C-L. Chang","year":"1973","unstructured":"Chang C-L., and Lee R.C-T., Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, NY, (1973)."},{"key":"21_CR6","first-page":"124","volume-title":"Journal of the ACM 21(1)","author":"S. Fleisig","year":"1974","unstructured":"Fleisig S., Loveland D.W., Smiley A.K., and Yarmush D.L., An Implementation of the Model Elimination Proof Procedure, In Journal of the ACM 21(1), ACM Press, New York, NY, (1974), 124\u2013139."},{"key":"21_CR7","first-page":"227","volume-title":"Artificial Intellience 2","author":"R. Kowalski","year":"1971","unstructured":"Kowalski R., and Kuehner D., Linear Resolution with Selection Function, In Artificial Intellience 2, Elsevier Science, Amsterdam, The Netherlands, (1971), 227\u2013260."},{"key":"21_CR8","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":"21_CR9","first-page":"147","volume-title":"A Linear Format for Resolution","author":"D.W. Loveland","year":"1970","unstructured":"Loveland D.W., A Linear Format for Resolution, In Laudet M. et al. (Ed.), Proceedings of the IRIA Symposium on Automatic Demonstration (Versailles, France, 1968), Springer-Verlag, New York, NY, (1970), 147\u2013162."},{"key":"21_CR10","first-page":"163","volume-title":"Refinement Theorems in Resolution Theory","author":"D. Luckham","year":"1970","unstructured":"Luckham D., Refinement Theorems in Resolution Theory, In Laudet M. et al. (Ed.), Proceedings of the Symposium on Automatic Demonstration (Versailles, France, 1968), Springer-Verlag, New York, NY, (1970), 163\u2013190."},{"key":"21_CR11","first-page":"197","volume-title":"Lecture Notes in Computer Science 310","author":"M.A. McRobbie","year":"1988","unstructured":"McRobbie M.A., Meyer R.K., and Thistlewaite P.B., Towards Efficient \u201cKnowledge-Based\u201d Automated Theorem Proving for Non-Standard Logics, In Lusk E., Overbeek R. (Ed.), Proceedings of the 9th International Conference on Automated Deduction (Argonne, IL, 1988), (Goos G., Hartmanis J. (Ed.), Lecture Notes in Computer Science 310), Springer-Verlag, New York, NY, (1988), 197\u2013217."},{"key":"21_CR12","first-page":"341","volume-title":"The Computer Journal 8","author":"B. Meltzer","year":"1966","unstructured":"Meltzer B., Theorem-proving for computers: Some results on resolution and renaming, In The Computer Journal 8, The Britsh Computer Society, London, England, (1966), 341\u2013343."},{"key":"21_CR13","first-page":"191","volume-title":"Information Processing Letters 14(4)","author":"J. Minker","year":"1982","unstructured":"Minker J., and Zanon G., An Extension to Linear Resolution with Selection Function, In Information Processing Letters 14(4), Elsevier Science, Amsterdam, The Netherlands, (1982), 191\u2013194."},{"key":"21_CR14","first-page":"227","volume-title":"Artificial Intelligence 18","author":"D.A. Plaisted","year":"1982","unstructured":"Plaisted D.A., A Simplified Problem Reduction Format, In Artificial Intelligence 18, Elsevier Science, Amsterdam, The Netherlands, (1982), 227\u2013261."},{"key":"21_CR15","volume-title":"Technical Note 72","author":"R. Reboh","year":"1972","unstructured":"Reboh R., Raphael B., Yates R.A., Kling R.E., and Velarde C., Study of automatic theorem proving programs, Technical Note 72, Artificial Intelligence Center, SRI International, Menlo Park, CA, (1972)."},{"key":"21_CR16","first-page":"5","volume-title":"Logic Programming Newsletter 2(1)","author":"G.A. Ringwood","year":"1988","unstructured":"Ringwood G.A., SLD: A Folk Acronym, In Moss C. (Ed.), Logic Programming Newsletter 2(1), Association for Logic Programming, London, England, (1988), 5\u20137."},{"key":"21_CR17","first-page":"227","volume-title":"International Journal of Computer Mathematics 1","author":"J.A. Robinson","year":"1965","unstructured":"Robinson J.A., Automatic Deduction with Hyper-resolution, In International Journal of Computer Mathematics 1, Gordon and Breach, London, England, (1965), 227\u2013234."},{"key":"21_CR18","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":"21_CR19","first-page":"687","volume-title":"Journal of the ACM 14(4)","author":"J.R. Slagle","year":"1967","unstructured":"Slagle J.R., Automatic Theorem Proving with Renamable and Semantic Resolution, In Journal of the ACM 14(4), ACM Press, New York, NY, (1967), 687\u2013697."},{"key":"21_CR20","first-page":"573","volume-title":"Lecture Notes in Computer Science 230","author":"M.E. Stickel","year":"1986","unstructured":"Stickel M.E., A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler, In Siekmann J.H. (Ed.), Proceedings of the 8th International Conference on Automated Deduction (Oxford, England, 1986), (Goos G., Hartmanis J. (Ed.). Lecture Notes in Computer Science 230), Springer-Verlag, New York, NY, (1986), 573\u2013587."},{"key":"21_CR21","first-page":"3","volume-title":"Association for Automated Reasoning Newsletter (13)","author":"G. Sutcliffe","year":"1989","unstructured":"Sutcliffe G., Complete Linear Derivation Systems for General Clauses, In Wos L. (Ed.), Association for Automated Reasoning Newsletter (13), Association for Automated Reasoning, Argonne, Il, (1989), 3\u20134."},{"key":"21_CR22","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":"21_CR23","volume-title":"The Semantically Guided Linear Deduction System","author":"G. Sutcliffe","year":"1992","unstructured":"Sutcliffe G., The Semantically Guided Linear Deduction System, In Kapur, D. (Ed.), Proceedings of the 11th International Conference on Automated Deduction (Saratoga Springs, NY, 1992), Springer-Verlag, New York, NY, (1992)."},{"key":"21_CR24","first-page":"322","volume-title":"Lecture Notes in Artificial Intelligence 449","author":"M. Tarver","year":"1990","unstructured":"Tarver M., An Examination of the Prolog Technology Theorem Prover, In Stickel M. (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), 322\u2013335."},{"key":"21_CR25","first-page":"87","volume-title":"Lecture Notes in Artificial Intelligence 449","author":"T. Wakayama","year":"1990","unstructured":"Wakayama T., and Payne T.H., Case-Free Programs: An Abstraction of Definite Horn Programs, In Stickel M. (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), 87\u2013101."},{"key":"21_CR26","volume-title":"Automated Reasoning \u2014 33 Basic Research Problems","author":"L. Wos","year":"1988","unstructured":"Wos L., Automated Reasoning \u2014 33 Basic Research Problems, Prentice-Hall, Englewood Cliffs, New Jersey, (1988)."},{"key":"21_CR27","unstructured":"Zamov N.K., and Sharonov V.I., On a class of strategies which can be used to prove theorems by the resolution principle, In (In Russian) (Ed.), Issled, po konstruktivnoye matematikye i matematicheskoie logikye III(16), National Lending Library Russian Translating Program 5857, Boston Spa, Yorkshire, (1969), 54\u201364."}],"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_171.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:32:54Z","timestamp":1619573574000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55602-8_171"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540556022","9783540472520"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-55602-8_171","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}