{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:04:02Z","timestamp":1725483842569},"publisher-location":"Berlin, Heidelberg","reference-count":58,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439608"},{"type":"electronic","value":"9783540456322"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45632-5_10","type":"book-chapter","created":{"date-parts":[[2007,5,20]],"date-time":"2007-05-20T07:37:27Z","timestamp":1179646647000},"page":"231-252","source":"Crossref","is-referenced-by-count":0,"title":["An Open Research Problem: Strong Completeness of R. Kowalski\u2019s Connection Graph Proof Procedure"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Siekmann","sequence":"first","affiliation":[]},{"given":"Graham","family":"Wrightson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,17]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1145\/321466.321469","volume":"15","author":"P. B. Andrews","year":"1968","unstructured":"Andrews, P. B.: Resolution with Merging. J. ACM 15 (1968) 367\u2013381.","journal-title":"J. ACM"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"801","DOI":"10.1109\/TC.1976.1674698","volume":"8","author":"P. B. Andrews","year":"1976","unstructured":"Andrews, P. B.: Refutations by Matings. IEEE Trans. Comp. C-25, (1976) 8, 801\u2013807.","journal-title":"IEEE Trans. Comp. C-25"},{"key":"10_CR3","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P.B. Andrews","year":"1981","unstructured":"Andrews, P.B.: Theorem Proving via General Matings. J. ACM 28 (1981) 193\u2013214.","journal-title":"J. ACM"},{"key":"10_CR4","unstructured":"Antoniuo, G., Ohlbach, H.J.: Terminator. Proceedings 8th IJCAI, Karlsruhe, (1983) 916\u2013919."},{"key":"10_CR5","unstructured":"Bibel, W.: A Strong Completeness Result for the Connection Graph Proof Procedure. Bericht ATP-3-IV-80, Institut f\u00fcr Informatik, Technische Universit\u00e4t, M\u00fcnchen (1980)"},{"key":"10_CR6","first-page":"246","volume-title":"German Workshop on Artificial Intelligence","author":"W. Bibel","year":"1981","unstructured":"Bibel, W.: On the completeness of connection graph resolution. In German Workshop on Artificial Intelligence. J. Siekmann, ed. Informatik Fachberichte 47, Springer, Berlin, Germany (1981a) pp. 246\u2013247"},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W.: On matrices with connections. J.ACM, 28 (1981b) 633\u2013645","journal-title":"J.ACM"},{"key":"10_CR8","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving. (1982) Vieweg. Wiesbaden.","DOI":"10.1007\/978-3-322-90100-2"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Bibel, W.: Matings in matrices. Commun. ACM, 26, (1983) 844\u2013852","journal-title":"Commun. ACM"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1145\/256303.256313","volume":"44","author":"W. Bibel","year":"1997","unstructured":"Bibel, W., Eder, E.: Decomposition of tautologies into regular formula and strong completeness of connection-graph resolution J. ACM 44 (1997) 320\u2013344","journal-title":"J. ACM"},{"key":"10_CR11","volume-title":"SEKI report SR-86-01","author":"K. H. Bl\u00e4sius","year":"1986","unstructured":"Bl\u00e4sius, K. H.: Construction of equality graphs. SEKI report SR-86-01 (1986) Univ. Karlsruhe, Germany"},{"key":"10_CR12","volume-title":"SEKI report SR-87-01","author":"K. H. Bl\u00e4sius","year":"1987","unstructured":"Bl\u00e4sius, K. H.: Equality reasoning based on graphs. SEKI report SR-87-01 (1987) Univ. Karlsruhe, Germany"},{"key":"10_CR13","unstructured":"Bl\u00e4sius, K. H., B\u00fcrckert, H. J.: Deduktions Systeme, (1992) Oldenbourg Verlag. Also in English: Ellis Horwood, 1989"},{"key":"10_CR14","unstructured":"Bl\u00e4sius, K. H., Eisinger, N., Siekmann, J., Smolka, G., Herald A., Walter, C. The Markgraf Karl refutation procedure. Proc 7th IJCAI, Vancouver (1981)"},{"key":"10_CR15","unstructured":"Brown, F. Notes on Chains and Connection Graphs. Personal Notes, Dept. of Computation and Logic, University of Edinburgh (1976)"},{"key":"10_CR16","unstructured":"Chang, C.-L., Lee, R.C.-T.: Symbolic Logic and Mechanical Theorem Proving, Academic Press (1973)"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0004-3702(79)90015-8","volume":"12","author":"C.-L. Chang","year":"1979","unstructured":"Chang, C.-L., Slagle, J.R.: Using Rewriting Rules for Connection Graphs to Prove Theorems. Artificial Intelligence 12 (1979) 159\u2013178.","journal-title":"Artificial Intelligence"},{"key":"10_CR18","series-title":"Lect Notes Comput Sci","volume-title":"Proc of 8th Conf. on Automated Deduction","author":"N. Eisinger","year":"1986","unstructured":"Eisinger, N.: What you always wanted to know about clause graph resolution. In Proc of 8th Conf. on Automated Deduction Oxford (1986) LNCS 230, Springer"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Eisinger, N.: Subsumption for connection graphs. Proc 7th IGCAI, Vancouver (1981)","DOI":"10.1007\/978-3-662-02328-0_17"},{"key":"10_CR20","unstructured":"Eisinger, N.: Completeness, Confluence, and Related Properties of Clause Graph Resolution. Ph.D. dissertation, Universit\u00e4t Kaiserslautern (1988)"},{"key":"10_CR21","volume-title":"Completeness, Confluence, and Related Properties of Clause Graph Resolution","author":"N. Eisinger","year":"1991","unstructured":"Eisinger, N.: Completeness, Confluence, and Related Properties of Clause Graph Resolution. Pitman, London, Morgan Kaufmann Publishers,Inc., San Mateo,California (1991)"},{"key":"10_CR22","unstructured":"Eisinger, N., Siekmann, J., Unvericht, E.: The Markgraf Karl refutation procedure. Proc of Conf on Automated Deduction, Austin, Texas (1979)"},{"key":"10_CR23","unstructured":"Eisinger, N., Ohlbach, H. J., Pr\u00e4cklein, A.: Elimination of redundancies in clause sets and clause graphs (1989) SEKI report, SR-89-01, University of Karlsruhe"},{"key":"10_CR24","unstructured":"Gabbay, D., Siekmann, J.: Logical encoding of the clause graph proof procedure, 2002, forthcoming"},{"key":"10_CR25","doi-asserted-by":"crossref","unstructured":"H\u00e4hnle, R., Murray, N. V., Rosenthal, E.: Ordered resolution versus connection graph resolution. In: R. Gor\u00e9, A. Leitsch, T. Nipkow Automated Reasoning, Proc of IJ-CAR 2001 (2001) LNAI 2083, Springer","DOI":"10.1007\/3-540-45744-5_14"},{"key":"10_CR26","first-page":"181","volume-title":"Machine Intelligence","author":"R. Kowalski","year":"1970","unstructured":"Kowalski, R.: Search Strategies for Theorem Proving. Machine Intelligence (B. Meltzer and D. Michie, eds.), 5 Edinburgh University Press, Edinburgh, (1970) 181\u2013201"},{"key":"10_CR27","doi-asserted-by":"publisher","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"Kowalski, R.:. A proof procedure using connection graphs. J.ACM 22 (1975) 572\u2013595","journal-title":"J.ACM"},{"key":"10_CR28","series-title":"Lecture Notes in Math","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BFb0060630","volume-title":"Proc. of Symp. on Automatic Demonstration","author":"D. W. Loveland","year":"1970","unstructured":"Loveland, D. W.: A Linear Format for Resolution. Proc. of Symp. on Automatic Demonstration. Lecture Notes in Math 125, Springer Verlag, Berlin, (1970) 147\u2013162. Also in Siekmann and Wrightson [1983b], 377\u2013398"},{"key":"10_CR29","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.: Automated Theorem Proving: A Logical Basis North-Holland, New York (1978)"},{"key":"10_CR30","unstructured":"Meagher D., Hext, J.: Link deletion in resolution theorem proving (1998) unpublished manuscript"},{"key":"10_CR31","unstructured":"Murray, N. V., Rosenthal, E.: Path resolution with link deletion. Proc. of 9th IJCAII Los Angeles (1985)"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Murray, N. V., Rosenthal, E.: Dissolution: making paths vanish. J. ACM 40 (1993)","DOI":"10.1145\/174130.174135"},{"key":"10_CR33","doi-asserted-by":"crossref","unstructured":"Ohlbach, H. J.: Ein regelbasiertes Klauselgraph Beweisverfahren. Proc. of German Conference on AI, GWAI-83 (1983) Springer Verlag IFB vol 76","DOI":"10.1007\/978-3-642-69391-5_20"},{"key":"10_CR34","doi-asserted-by":"crossref","unstructured":"Ohlbach, H. J.: Theory unification in abstract clause graphs. Proc. of German Conf. on AI GWAI-85 (1985) Springer Verlag IFB vol 118","DOI":"10.1007\/978-3-642-71145-9_6"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Ohlbach, H. J.: Link inheritance in abstract clause graphs J. Autom. Reasoning 3 (1987)","DOI":"10.1007\/BF00381143"},{"key":"10_CR36","volume-title":"Computational Logic","author":"H. J. Ohlbach","year":"1991","unstructured":"Ohlbach, H. J., Siekmann, J.: The Markgraf Karl refutation procedure. In: J. L. Lassez, G. Plotkin, Computational Logic (1991) MIT Press, Cambridge MA"},{"key":"10_CR37","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/0898-1221(82)90042-6","volume":"8","author":"E. G. Omodeo","year":"1982","unstructured":"Omodeo, E. G.: The linked conjunct method for automatic deduction and related search techniques. Computers and Mathematics with Applications 8 (1982) 185\u2013203","journal-title":"Computers and Mathematics with Applications"},{"key":"10_CR38","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1005711712356","volume":"18","author":"A. Ramesh","year":"1997","unstructured":"Ramesh, A., Beckert, B., H\u00e4hnle, R., Murray, N. V.: Fast subsumption checks using anti-links J. Autom. Reasoning 18 (1997) 47\u201383","journal-title":"J. Autom. Reasoning"},{"key":"10_CR39","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. J.ACM 12 (1965) 23\u201341","journal-title":"J.ACM"},{"key":"10_CR40","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R.E. Shostak","year":"1976","unstructured":"Shostak, R.E.: Refutation Graphs. J. Artificial Intelligence 7, (1976), 51\u201364","journal-title":"J. Artificial Intelligence"},{"key":"10_CR41","unstructured":"Shostak, R.E.: A Graph-Theoretic View of Resolution Theorem-Proving. Report SRI International, Menlo Park (1979)"},{"key":"10_CR42","doi-asserted-by":"publisher","first-page":"823","DOI":"10.1109\/TC.1976.1674701","volume":"C-25","author":"S. Sickel","year":"1976","unstructured":"Sickel, S.: A Search Technique for Clause Interconnectivity Graphs. IEEE Trans. Comp. C-25 (1976) 823\u2013835","journal-title":"IEEE Trans. Comp."},{"key":"10_CR43","unstructured":"Siekmann, J. H., Stephan, W.: Completeness and Soundness of the Connection Graph Proof Procedure. Bericht 7\/76, Fakult\u00e4t Informatik, Universit\u00e4t Karlsruhe (1976). Also in Proceedings of AISB\/GI Conference on Artificial Intelligence, Hamburg (1978)"},{"key":"10_CR44","unstructured":"Siekmann, J. H., Stephan, W.: Completeness and Consistency of the Connection Graph Proof Procedure. Interner Bericht Institut I, Fakult\u00e4t Informatik, Universit\u00e4t Karlsruhe (1980)"},{"key":"10_CR45","doi-asserted-by":"crossref","unstructured":"Siekmann, J. H., Wrightson, G.: Paramodulated connection graphs Acta Informatica 13 (1980)","DOI":"10.1007\/BF00288537"},{"key":"10_CR46","volume-title":"Automation of Reasoning","author":"J. H. Siekmann","year":"1983","unstructured":"Siekmann, J. H., Wrightson, G.: Automation of Reasoning. Springer-Verlag, Berlin, Heidelberg, New York. Vol 1 and vol 2 (1983)"},{"key":"10_CR47","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/363647.363697","volume":"48","author":"J. H. Siekmann","year":"2001","unstructured":"Siekmann, J. H., Wrightson, G.: Erratum: A counterexample to W. Bibel\u2019s and E. Eder\u2019s strong completeness result for connection graph resolution. J. ACM 48 (2001) 145","journal-title":"J. ACM"},{"key":"10_CR48","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/978-3-642-68826-3_14","volume-title":"Proceedings of GWAI-82","author":"G. Smolka","year":"1982","unstructured":"Smolka, G.: Completeness of the connection graph proof procedure for unit refutable clause sets. In Proceedings of GWAI-82. Informatik Fachberichte, vol. 58. Springer-Verlag, Berlin, Germany (1982a) 191\u2013204."},{"key":"10_CR49","unstructured":"Smolka, G.: Einige Ergebnisse zur Vollst\u00e4ndigkeit der Beweisprozedur von Kowalski. Diplomarbeit, Fakult\u00e4t Informatik, Universit\u00e4t Karlsruhe (1982b)"},{"key":"10_CR50","volume-title":"SEKI report SR-82-03","author":"G. Smolka","year":"1982","unstructured":"Smolka, G.: Completeness and confluence properties of Kowalksi\u2019s clause graph calculus (1982c) SEKI report SR-82-03, University of Karlsruhe, Germany"},{"key":"10_CR51","unstructured":"Stickel, M.: A Non-Clausal Connection-Graph Resolution Theorem-Proving Program. Proceedings AAAI-82, Pittsburgh (1982) 229\u2013233"},{"key":"10_CR52","doi-asserted-by":"crossref","unstructured":"Walthe, Chr.: Elimination of redundant links in extended connection graphs. Proc of German Workshop on AI, GWAI-81 (1981) Springer Verlag, Fachberichte vol 47","DOI":"10.1007\/978-3-662-02328-0_19"},{"key":"10_CR53","volume-title":"AFIPS Conf. Proc.","author":"L.T. Wos","year":"1964","unstructured":"Wos, L.T., Carson, D.F., Robinson, G.A.: The Unit Preference Strategy in Theorem Proving. AFIPS Conf. Proc. 26, (1964) Spartan Books, Washington. Also in Siekmann and Wrightson [1983], 387-396."},{"key":"10_CR54","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L.T. Wos","year":"1965","unstructured":"Wos, L.T., Robinson, G.A., Carson, D.F.: Efficiency and Completeness of the Set of Support Strategy in Theorem Proving. J.ACM 12, (1965) 536\u2013541. Also in Siekmann and Wrightson [1983], 484\u2013492","journal-title":"J.ACM"},{"key":"10_CR55","volume-title":"Automated Reasoning: Introduction and Applications","author":"L. T. Wos","year":"1984","unstructured":"Wos, L. T, et al.: Automated Reasoning: Introduction and Applications (1984) Englewood Cliffs, new Jersey, Prentice-Hall"},{"key":"10_CR56","volume-title":"Report 98-3","author":"G. Wrightson","year":"1989","unstructured":"Wrightson, G.: A pragmatic strategy for clause graphs or the strong completeness of connection graphs. Report 98-3, Dept Comp. Sci., Univ of Newcastle, Australia (1989)"},{"key":"10_CR57","unstructured":"Yarmush, D. L.: The linked conjunct and other algorithms for mechanical theorem-proving. Technical Report IMM 412, Courant Institute of Mathematical Sciences, New York University (1976)"},{"key":"10_CR58","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1016\/0004-3702(70)90011-1","volume":"1","author":"R. A. Yates","year":"1970","unstructured":"Yates, R. A., Raphael, B., Hart, T. P.: Resolution Graphs. Artificial Intelligence 1 (1970) 257\u2013289.","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Computational Logic: Logic Programming and Beyond"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45632-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:58:41Z","timestamp":1556431121000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45632-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439608","9783540456322"],"references-count":58,"URL":"https:\/\/doi.org\/10.1007\/3-540-45632-5_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}