{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:44:00Z","timestamp":1725493440461},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664925"},{"type":"electronic","value":"9783540482420"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48242-3_4","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T16:28:09Z","timestamp":1184603289000},"page":"44-61","source":"Crossref","is-referenced-by-count":9,"title":["Evidence Algorithm and Sequent Logical Inference Search"],"prefix":"10.1007","author":[{"given":"Anatoli I.","family":"Degtyarev","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexander V.","family":"Lyaletski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marina K.","family":"Morokhovets","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"4_CR1","first-page":"3","volume-title":"Matematicheskie osnovy sistem iskusstvennogo intellekta","author":"A. Degtyarev","year":"1981","unstructured":"Degtyarev, A., Lyaletski, A.: Logical inference in SAD (In Russian). In: Kapitonova, Yu. (ed.): Matematicheskie osnovy sistem iskusstvennogo intellekta. Institute of Cybernetics, Kiev (1981) 3\u201311"},{"key":"4_CR2","first-page":"99","volume-title":"Actes preliminaries, du Simposium Pranco-Sovetique \u201cInformatika-91\u201d","author":"A. Lyaletski","year":"1991","unstructured":"Lyaletski, A.: Gentzen calculi and admissible substitutions. In: Actes preliminaries, du Simposium Pranco-Sovetique \u201cInformatika-91\u201d. Grenoble, France (1991) 99\u2013111"},{"key":"4_CR3","first-page":"3","volume":"2","author":"V. Glushkov","year":"1970","unstructured":"Glushkov, V.: Some problems of automata theory and artificial intelligence (in Russian). Kibernetika 2 (1970) 3\u201313","journal-title":"Kibernetika"},{"key":"4_CR4","first-page":"23","volume":"1","author":"F. Anufriyev","year":"1966","unstructured":"Anufriyev, F., Fediurko, V., Letichevski, A., Asel\u2019derov, Z., Didukh I.: On one algorithm of theorem proof search in Group Theory (in Russian). Kibernetika 1 (1966) 23\u201329","journal-title":"Kibernetika"},{"key":"4_CR5","first-page":"3","volume-title":"Teoriya avtomatov","author":"F. Anufriyev","year":"1969","unstructured":"Anufriyev, F.: An algorithm of theorem proof search in logical calculi (in Russian). In: Teoriya avtomatov 5. Institute of Cybernetics, Kiev (1969) 3\u201326"},{"key":"4_CR6","first-page":"3","volume-title":"Avtomatizatsiya poiska dokazatel\u2019stv teorem v matematike","author":"V. Glushkov","year":"1974","unstructured":"Glushkov, V, Vershinin, K., Kapitonova, Yu., Letichevski, A., Malevanniy, N., Kostyrko, V.: On a formal language for description of mathematical texts (in Russian). In: Avtomatizatsiya poiska dokazatel\u2019stv teorem v matematike. Institute of Cybernetics, Kiev (1974) 3\u201336"},{"key":"4_CR7","unstructured":"Degtyarev, A.: The strategy of monotone paramodulation (in Russian). In: Proc.of 5th All Soviet Union conf.on mathematical logic. Novosibirsk (1979) 39"},{"key":"4_CR8","first-page":"36","volume-title":"Avtomatizatsiya obrabotki matematicheskikh tekstov","author":"V. Atayan","year":"1980","unstructured":"Atayan, V., Vershinin, K.: On formalization of some inference search methods (in Russian). In: Avtomatizatsiya obrabotki matematicheskikh tekstov. Institute of Cybernetics, Kiev (1980) 36\u201352"},{"key":"4_CR9","first-page":"48","volume":"2","author":"Yu. Kapitonova","year":"1979","unstructured":"Kapitonova, Yu., Vershinin, K., Degtyarev, A., Zhezherun, A., Lyaletski, A.: On a system for mathematical texts processing (in Russian). Kibernetika 2 (1979) 48","journal-title":"Kibernetika"},{"key":"4_CR10","first-page":"3","volume-title":"Avtomatizatsiya obrabotki matematicheskikh tekstov","author":"V. Glushkov","year":"1980","unstructured":"Glushkov, V.: The System for Proving Automation (in Russian). In: Avtomatizatsiya obrabotki matematicheskikh tekstov. Institute of Cybernetics, Kiev (1980) 3\u201330"},{"key":"4_CR11","first-page":"42","volume-title":"Matematicheskoye obespecheniye sistem logicheskogo vyvoda i deduktivnych postroyeniy na EVM","author":"A. Degtyarev","year":"1983","unstructured":"Degtyarev, A.: Equality handling techniques in theories with a full set of reductions (in Russian). In: Matematicheskoye obespecheniye sistem logicheskogo vyvoda i deduktivnych postroyeniy na EVM. Institute of Cybernetics, Kiev (1983) 42\u201355"},{"key":"4_CR12","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/BF02366511","volume":"32","author":"V. Atayan","year":"1996","unstructured":"Atayan, V., Morokhovets, M.: Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system. Cybernetics and System Analysis 32 (1996) 442\u2013465","journal-title":"Cybernetics and System Analysis"},{"key":"4_CR13","first-page":"151","volume-title":"Proc. Second International THEOREMA Workshop","author":"A. Degtyarev","year":"1998","unstructured":"Degtyarev, A., Kapitonova, Yu., Letichevski, A., Lyaletski, A., Morokhovets, M.: A brief historical sketch on Kiev school of automated theorem proving. In: Buch-berger, B., Jebelean, T. (eds.): Proc. Second International THEOREMA Workshop. RISC, Linz, Austria (1998) 151\u2013155"},{"key":"4_CR14","volume-title":"Logic for computer science: foundations of Automatic Theorem Proving","author":"J. Gallier","year":"1986","unstructured":"Gallier, J.: Logic for computer science: foundations of Automatic Theorem Proving. Harper and Row, Inc. New York (1986) 513 p."},{"key":"4_CR15","unstructured":"Robinson, J.: A Machine-Oriented Logic Based on Resolution Principle. JACM (1965) 23\u201341"},{"key":"4_CR16","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0049-237X(08)72020-2","volume-title":"Comp. Program. and Form. Sys.: Stud. in Logic","author":"S. Kanger","year":"1963","unstructured":"Kanger, S.: Simplified proof method for elementary logic. In: Comp. Program. and Form. Sys.: Stud. in Logic. Amsterdam, North-Holland, Publ. Co. (1963) 87\u201393"},{"key":"4_CR17","first-page":"112","volume":"1","author":"A.V. Lyaletski","year":"1981","unstructured":"Lyaletski, A.V.: Variant of Herbrand Theorem for Formulas in Prefix Form (in Russian). Kibernetika 1 (1981) 112\u2013116","journal-title":"Kibernetika"},{"key":"4_CR18","first-page":"43","volume-title":"Raspoznavaniye obrazov","author":"V. Atayan","year":"1978","unstructured":"Atayan, V., Vershinin, K., Zhezherun, A.: On structural processing of mathematical texts (in Russian). In: Raspoznavaniye obrazov. Institute of Cybernetics, Kiev (1978) 43\u201354"},{"key":"4_CR19","first-page":"157","volume-title":"Proc. Second International THEOREMA Workshop","author":"M. Morokhovets","year":"1998","unstructured":"Morokhovets, M., Luzhnykh, A.: Representing mathematical texts in a formalized natural-like language. In: Buchberger, B., Jebelean, T. (eds.): Proc. Second International THEOREMA Workshop. RISC, Linz, Austria (1998) 157\u2013160"},{"key":"4_CR20","unstructured":"http:\/\/www-formal.stanford.edu\/clt\/ARS\/systems.html"},{"key":"4_CR21","unstructured":"http:\/\/mizar.uw.bialostok.pl\/"},{"key":"4_CR22","unstructured":"Buchberger, B., Jebelean, T., Kriftner, F., Marin, M., Tomuta, E., Vasaru, D.: A survey of the Theorema project. In: Kuechlin, W. (ed.): Proc. ISSAC\u201997, Maui, Hawaii (1997) 384\u2013391"},{"key":"4_CR23","unstructured":"http:\/\/www.ags.uni-sb.de\/projects\/deduktion\/projects\/omega\/"},{"key":"4_CR24","unstructured":"http:\/\/www.cl.cam.ac.uk\/Research\/HVG\/Isabelle\/"},{"key":"4_CR25","unstructured":"http:\/\/www.Cybercom.net\/~rbjones\/rbjpub\/logic\/qedres00.htm"}],"container-title":["Lecture Notes in Computer Science","Logic for Programming and Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48242-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T23:46:05Z","timestamp":1558482365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48242-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664925","9783540482420"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-48242-3_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}