{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:49:03Z","timestamp":1725558543105},"publisher-location":"Berlin, Heidelberg","reference-count":106,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642141270"},{"type":"electronic","value":"9783642141287"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14128-7_35","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T06:45:36Z","timestamp":1277793936000},"page":"411-426","source":"Crossref","is-referenced-by-count":1,"title":["Evidence Algorithm and System for Automated Deduction: A Retrospective View"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Lyaletski","sequence":"first","affiliation":[]},{"given":"Konstantin","family":"Verchinine","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","first-page":"87","volume":"2","author":"V.M. Glushkov","year":"1962","unstructured":"Glushkov, V.M.: Intelligent machines and the mental activity of a human. Soviet School\u00a02, 87\u201391 (1962) (in Russian)","journal-title":"Soviet School"},{"key":"35_CR2","first-page":"21","volume-title":"Applied Linguistic and Machine Translation","author":"L.A. Kaluzhnin","year":"1962","unstructured":"Kaluzhnin, L.A.: On an information language for mathematics. In: Applied Linguistic and Machine Translation, pp. 21\u201329. Kiev University, Kiev (1962) (in Russian)"},{"key":"35_CR3","unstructured":"Kaluzhnin, L.A., Koroliuk, V.S.: Algorithms and mathematical machines. Soviet School, 283 p. (1964) (in Ukrainian)"},{"issue":"1","key":"35_CR4","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/BF01072250","volume":"2","author":"F.V. Anufriev","year":"1966","unstructured":"Anufriev, F.V., Fedyurko, V.V., Letichevskii, A.A., Asel\u2019derov, Z.M., Didukh, I.I.: An algorithm for proving theorems in Group theory. Cybernetics and System Analysis\u00a02(1), 20\u201325 (1966)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR5","unstructured":"Anufriev, F.V.: An algorithm for proving theorems in Set theory. In: Theory of Automata, GIC, AS of UkrSSR, Kiev, vol.\u00a04, pp. 3\u201324 (1967) (in Russian)"},{"issue":"5","key":"35_CR6","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/BF01071593","volume":"3","author":"V.M. Glushkov","year":"1967","unstructured":"Glushkov, V.M., Pogrebinskii, S.B., Rabinovich, Z.L., Stognii, A.A.: Aspects of the development of digital computer architectures in the dependence of computer software systems. Cybernetics and System Analysis\u00a03(5), 13\u201324 (1967)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR7","unstructured":"Asel\u2019derov, Z.M.: Solving equations in free groups. In: Abstract of candidate dissertation in Physics and Mathematics, GIC, AS of UkrSSR, Kiev, 12 p. (1968) (in Russian)"},{"key":"35_CR8","unstructured":"Anufriyev, F.V.: An algorithm of theorem proving in logical calculi. In: Theory of Automata, GIC, AS of UkrSSR, Kiev, pp. 3\u201326 (1969) (in Russian)"},{"issue":"2","key":"35_CR9","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/BF01070496","volume":"6","author":"V.M. Glushkov","year":"1970","unstructured":"Glushkov, V.M.: Some problems in the theory of automata and artificial intelligence. Cybernetics and System Analysis\u00a06(2), 17\u201327 (1970)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR10","unstructured":"Glushkov, V.M., Kostyrko, V.F., Letichevskii, A.A., Anufriyev, F.V., Asel\u2019derov, Z.M.: On a language for the writing of formal theories. In: Theoretical Cybernetics, GIC, AS of UkrSSR, Kiev, vol.\u00a03, pp. 4\u201331 (1970) (in Russian)"},{"issue":"3","key":"35_CR11","first-page":"513","volume":"7","author":"V.M. Glushkov","year":"1971","unstructured":"Glushkov, V.M., Bodnarchuk, V.G., Grinchenko, T.A., Dorodnitsyna, A.A., Klimenko, V.P., Letichevskii, A.A., Pogrebinskii, S.B., Stognii, A.A., Fishman, Y.S.: ANALITIK algorithmic language for the description of computing processes using analytical transformations. Cybernetics and Systems Analysis\u00a07(3), 513\u2013552 (1971)","journal-title":"Cybernetics and Systems Analysis"},{"issue":"5","key":"35_CR12","doi-asserted-by":"publisher","first-page":"740","DOI":"10.1007\/BF01068446","volume":"8","author":"F.V. Anufriev","year":"1972","unstructured":"Anufriev, F.V., Asel\u2019derov, Z.M.: The obviousness algorithm. Cybernetics and System Analysis\u00a08(5), 740\u2013768 (1972)","journal-title":"Cybernetics and System Analysis"},{"issue":"5","key":"35_CR13","doi-asserted-by":"publisher","first-page":"777","DOI":"10.1007\/BF01068448","volume":"8","author":"F.V. Anufriyev","year":"1972","unstructured":"Anufriyev, F.V., Kostiakov, V.M., Malashonok, A.I.: Algorithm and computer experiment for seeking proofs of theorems in the predicate calculus. Cybernetics and System Analysis\u00a08(5), 777\u2013783 (1972)","journal-title":"Cybernetics and System Analysis"},{"issue":"5","key":"35_CR14","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/BF01068443","volume":"8","author":"V.M. Glushkov","year":"1972","unstructured":"Glushkov, V.M., Kapitonova, Y.V.: Automatic search for proofs of mathematical theorems and intelligent computers. Cybernetics and System Analysis\u00a08(5), 709\u2013713 (1972)","journal-title":"Cybernetics and System Analysis"},{"issue":"5","key":"35_CR15","doi-asserted-by":"publisher","first-page":"730","DOI":"10.1007\/BF01068445","volume":"8","author":"V.M. Glushkov","year":"1972","unstructured":"Glushkov, V.M., Kapitonova, Y.V., Letichevskii, A.A., Vershinin, K.P., Malevanyi, N.P.: Construction of a practical formal language for mathematical theories. Cybernetics and System Analysis\u00a08(5), 730\u2013739 (1972)","journal-title":"Cybernetics and System Analysis"},{"issue":"5","key":"35_CR16","doi-asserted-by":"publisher","first-page":"714","DOI":"10.1007\/BF01068444","volume":"8","author":"Y.V. Kapitonova","year":"1972","unstructured":"Kapitonova, Y.V., Kostyrko, V.F., Lyaletski, A.V., Degtyarev, A.I., Malashonok, A.I., Anufriev, F.V., Asel\u2019derov, Z.M.: A brief review and bibliography of investigations into automation of search of theorem proofs in formal theories. Cybernetics and System Analysis\u00a08(5), 714\u2013729 (1972)","journal-title":"Cybernetics and System Analysis"},{"issue":"4","key":"35_CR17","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/BF01068587","volume":"9","author":"A.I. Degtyarev","year":"1973","unstructured":"Degtyarev, A.I.: Question of constructing a problem-oriented procedure for the proof of theorems. Cybernetics and System Analysis\u00a09(4), 628\u2013629 (1973)","journal-title":"Cybernetics and System Analysis"},{"issue":"4","key":"35_CR18","doi-asserted-by":"publisher","first-page":"630","DOI":"10.1007\/BF01068588","volume":"9","author":"Y.V. Kapitonova","year":"1973","unstructured":"Kapitonova, Y.V., Degtyarev, A.I., Lyaletski, A.V.: Use of heuristic procedures in search programs for proofs of theorems (survey). Cybernetics and System Analysis\u00a09(4), 630\u2013641 (1973)","journal-title":"Cybernetics and System Analysis"},{"issue":"4","key":"35_CR19","doi-asserted-by":"publisher","first-page":"621","DOI":"10.1007\/BF01068586","volume":"9","author":"K.P. Vershinin","year":"1973","unstructured":"Vershinin, K.P.: Relationship between formal language of mathematical theories and axiomatic systems of the theory of sets. Cybernetics and System Analysis\u00a09(4), 621\u2013627 (1973)","journal-title":"Cybernetics and System Analysis"},{"issue":"5","key":"35_CR20","first-page":"755","volume":"14","author":"V.M. Glushkov","year":"1974","unstructured":"Glushkov, V.M., Vershinin, K.P., Kapitonova, Y.V., Letichevsky, A.A., Malevanyi, N.P., Kostyrko, V.F.: On a formal language for representation of mathematical texts. search of theorem proofs in formal theories. Cybernetics and System Analysis\u00a014(5), 755\u2013757 (1974)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR21","unstructured":"Degtyarev, A.I.: On heuristic procedure for proving theorems from vector spaces. In: Computer-aided Theorem Proving in Mathematics, GIC, AS of UkrSSR, Kiev, pp. 95\u201399 (1974) (in Russian)"},{"key":"35_CR22","unstructured":"Malashonok, A.I.: The soundness and completeness of the obviousness algorithm. In: Computer-aided Theorem Proving in Mathematics, GIC, AS of UkrSSR, Kiev, pp. 75\u201395 (1974) (in Russian)"},{"key":"35_CR23","unstructured":"Degtyarev, A.I.: On the use of axioms of functional reflexivity in P&R refutation procedure. Preprint 75-28, GIC, AS of UkrSSR, Kiev (1975) (in Russian)"},{"key":"35_CR24","unstructured":"Lyaletski, A.V.: On a calculus of c-clauses. In: Mathematical Issues of Intelligent Machines Theory, GIC, Kiev, pp. 34\u201348 (1975) (in Russian)"},{"key":"35_CR25","unstructured":"Lyaletski, A.V., Malashonok, A.I.: A calculus of c-clauses based on the clash-resolution rule. In: Mathematical Issues of Intelligent Machines Theory, GIC, AS of UkrSSR, Kiev, pp. 3\u201333 (1975) (in Russian)"},{"key":"35_CR26","unstructured":"Vershinin, K.P.: On the notion of the correctness of a TL-text. In: Mathematical Issues of Intelligent Machines Theory, GIC, AS of UkrSSR, Kiev, pp. 61\u201370 (1975) (in Russian)"},{"key":"35_CR27","unstructured":"Lyaletski, A.V.: On minimal inferences in calculi of c-clauses. Issues of Robot Theory and of Artificial Intelligence, GIC, AS of UkrSSR, Kiev, pp. 34\u201348 (1975) (in Russian)"},{"key":"35_CR28","unstructured":"Atayan, V.V., Vershinin, K.P., Zhezherun, A.P.: Structural processing of mathematical texts. Pattern Recognition, GIC, AS of UkrSSR, Kiev, pp. 43\u201354 (1978) (in Russian)"},{"key":"35_CR29","unstructured":"Zhezherun, A.P.: Implementation of dynamic syntax tools for mathematical text processing systems. In: Abstracts of the All-union Symposium on Artificial Intelligence and Automatization of Mathematical Research, GIC, AS of UkrSSR, Kiev (1978) (in Russian)"},{"key":"35_CR30","unstructured":"Degtyarev, A.I.: A monotonic paramodulation strategy. In: Abstracts of the Vth All-union Conference on Mathematical Logic, Novosibirsk, USSR, p. 39 (1979) (in Russian)"},{"key":"35_CR31","unstructured":"Degtyarev, A.I.: A strict paramodulation strategy. In: Semiotics and Informatics, vol.\u00a012, pp. 20\u201322. All-union Institute of Scientific and Technical Information, Moscow (1979) (in Russian)"},{"issue":"2","key":"35_CR32","first-page":"209","volume":"15","author":"Y.V. Kapitonova","year":"1979","unstructured":"Kapitonova, Y.V., Vershinin, K.P., Degtyarev, A.I., Zhezherun, A.P., Lyaletski, A.V.: System for processing mathematical texts. Cybernetics and System Analysis\u00a015(2), 209\u2013210 (1979)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR33","unstructured":"Lyaletski, A.: On a variant of Herbrand theorem. In: Abstracts of the Vth All-union Conference on Mathematical Logic, Novosibirsk, USSR, p. 87 (1979) (in Russian)"},{"key":"35_CR34","first-page":"29","volume-title":"Semiotics and Informatics","author":"A. Lyaletski","year":"1979","unstructured":"Lyaletski, A.: On a procedure of refutation search. In: Semiotics and Informatics, vol.\u00a012, pp. 29\u201332. All-union Institute of Scientific and Technical Information, Moscow (1979) (in Russian)"},{"key":"35_CR35","unstructured":"Lyaletski, A.: On the issue of the construction of refutation procedures for which preliminary skolemization is not obligatory. In: Computer-aided Mathematical Texts Processing and Issues of Robot Construction, GIC, AS of UkrSSR, Kiev, pp. 28\u201335 (1979) (in Russian)"},{"key":"35_CR36","unstructured":"Morokhovets, M.K.: On the implementation of logical inference procedures in the framework of a mathematical texts processing system. In: Computer-aided Mathematical Texts Processing and Issues of Robot Construction, GIC, AS of UkrSSR, Kiev, pp. 36\u201341 (1979) (in Russian)"},{"key":"35_CR37","first-page":"3","volume-title":"Semiotics and Informatics","author":"K.P. Vershinin","year":"1979","unstructured":"Vershinin, K.P.: Application of auxiliary propositions in inference search. In: Semiotics and Informatics, vol.\u00a012, pp. 3\u20137. All-union Institute of Scientific and Technical Information, Moscow (1979) (in Russian)"},{"key":"35_CR38","unstructured":"Vershinin, K.P.: Refutation search and \u201cnatural\u201d proofs. In: Computer-aided Mathematical Texts Processing and Issues of Robot Construction, GIC, AS of UkrSSR, Kiev, pp. 12\u201328 (1979) (in Russian)"},{"issue":"5","key":"35_CR39","first-page":"120","volume":"15","author":"A.P. Zhezherun","year":"1979","unstructured":"Zhezherun, A.P.: Decidability of the unification problem for second-order languages with unary functional symbols. Cybernetics and System Analysis\u00a015(5), 120\u2013125 (1979)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR40","doi-asserted-by":"crossref","unstructured":"Vershinin, K.P., Zhezherun, A.P.: Data representation in a system for processing of mathematical texts. In: Issues of the Construction and Application of Mathematical Methods and Computers, GIC, AS of UkrSSR, Kiev, pp. 7\u201315 (1979) (in Russian)","DOI":"10.1007\/BF01069331"},{"key":"35_CR41","unstructured":"Atayan, V.V., Vershinin, K.P.: Formalization of some deduction techniques. In: Computer-aided Processing of Mathematical Texts, GIC, AS of UkrSSR, Kiev, pp. 36\u201352 (1980) (in Russian)"},{"key":"35_CR42","unstructured":"Degtyarev, A.I.: Some special tools of Evidence Algorithm for equality handling. In: Computer-aided Processing of Mathematical Texts, GIC, AS of UkrSSR, Kiev, pp. 30\u201336 (1980) (in Russian)"},{"key":"35_CR43","unstructured":"Glushkov, V.M.: The system for automatic theorem proving (SAD) (a brief informal description). In: Computer-aided Processing of Mathematical Texts, GIC, AS of UkrSSR, Kiev, pp. 3\u201330 (1980) (in Russian)"},{"key":"35_CR44","unstructured":"Morokhovets, M.K.: On editing proofs. In: Computer-aided Processing of Mathematical Texts, GIC, AS of UkrSSR, Kiev, pp. 53\u201361 (1980) (in Russian)"},{"key":"35_CR45","unstructured":"Zhezherun, A.P.: Basic tools for data processing in an automatic theorem-proving system. In: Abstracts of the All-union Conference \u201cMethods of Mathematical Logic in Artificial Intelligence and Systematic Programming\u201d, Palanga, Lithuania, vol.\u00a0I, p. 105 (1980) (in Russian)"},{"key":"35_CR46","unstructured":"Zhezherun, A.P.: Tools for computer-aided processing of mathematical texts. In: Abstract of candidate dissertation in Physics and Mathematics, GIC, AS of UkrSSR, Kiev (1980) (in Russian)"},{"key":"35_CR47","unstructured":"Atayan, V.V.: On some tools for the construction of an information environment in a computer-aided proving system. In: Mathematical Foundations of Artificial Intelligence Systems, GIC, AS of UkrSSR, Kiev, pp. 11\u201317 (1981) (in Russian)"},{"key":"35_CR48","unstructured":"Degtyarev, A.I., Lyaletski, A.V.: Logical inference in the system for automatic theorem proving, SAD. In: Mathematical Foundations of Artificial Intelligence Systems, GIC, AS of UkrSSR, Kiev, pp. 3\u201311 (1981) (in Russian)"},{"issue":"1","key":"35_CR49","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/BF01307049","volume":"17","author":"A.V. Lyaletski","year":"1981","unstructured":"Lyaletski, A.V.: A variant of Herbrand\u2019s theorem for formulas in prenex form. Cybernetics and System Analysis\u00a017(1), 125\u2013129 (1981)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR50","unstructured":"Degtyarev, A.I.: Equality handling in proof search in theories with the complete set of reductions. In: Abstracts of the VIth All-union Conference on Mathematical Logic, Tbilisi, USSR, p. 55 (1982) (in Russian)"},{"key":"35_CR51","unstructured":"Degtyarev, A.I.: Methods and tools for equality handling in machine theorem proving. In: Abstract of candidate dissertation in Physics and Mathematics, GIC, AS of UkrSSR, Kiev, 24 p. (1982) (in Russian)"},{"key":"35_CR52","first-page":"98","volume-title":"Abstracts of the VIth All-union Conference on Mathematical Logic","author":"A.V. Lyaletski","year":"1982","unstructured":"Lyaletski, A.V.: On a modification of Kanger\u2019s method. In: Abstracts of the VIth All-union Conference on Mathematical Logic, pp. 98\u201399. Tbilisi University, Tbilisi (1982) (in Russian)"},{"key":"35_CR53","unstructured":"Lyaletski, A.V.: Methods of machine proof search in the first-order predicate calculus. In: Abstract of candidate dissertation in Physics and Mathematics, GIC, AS of UkrSSR, Kiev, 23 p. (1982) (in Russian)"},{"key":"35_CR54","unstructured":"Vershinin, K.P.: On the correctness of mathematical texts and its computer-aided verification. In: Abstract of candidate dissertation in Physics and Mathematics, GIC, AS of UkrSSR, Kiev, 20 p. (1982) (in Russian)"},{"key":"35_CR55","unstructured":"Lyaletski, A.V.: Generating sufficient statements in the SAD system. In: Abstracts of the IIIth All-union Conference \u201cApplication of Methods of Mathematical Logic\u201d, Tallinn, USSR, pp. 65\u201366 (1983) (in Russian)"},{"issue":"3","key":"35_CR56","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/BF01072145","volume":"19","author":"K.P. Vershinin","year":"1983","unstructured":"Vershinin, K.P., Morokhovets, M.K.: Strategies of the search for derivation of statements with restricted quantifiers. Cybernetics and System Analysis\u00a019(3), 298\u2013308 (1983)","journal-title":"Cybernetics and System Analysis"},{"issue":"5","key":"35_CR57","doi-asserted-by":"publisher","first-page":"702","DOI":"10.1007\/BF01074730","volume":"21","author":"M.K. Morokhovets","year":"1985","unstructured":"Morokhovets, M.K.: Deduction-seeking procedures and transitive relations. Cybernetics and System Analysis\u00a021(5), 702\u2013708 (1985)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR58","unstructured":"Degtyarev, A.I.: Equality handling methods for Horn sets. In: Methods for Algorithmization and Realization of Processes of Finding Solutions of Intelligent Problems, GIC, Kiev, pp. 19\u201326 (1986) (in Russian)"},{"issue":"3","key":"35_CR59","first-page":"298","volume":"22","author":"A.I. Degtyarev","year":"1986","unstructured":"Degtyarev, A.I., Voronkov, A.A.: Equality control methods in machine theorem proving. Cybernetics and System Analysis\u00a022(3), 298\u2013307 (1986)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR60","unstructured":"Morokhovets, M.K.: Special strategies for theorem proof search in mathematics and tools for their implementation. In: Abstract of candidate dissertation in Physics and Mathematics, GIC, AS of UkrSSR, Kiev, 14 p. (1986) (in Russian)"},{"issue":"3","key":"35_CR61","first-page":"290","volume":"22","author":"A.A. Voronkov","year":"1986","unstructured":"Voronkov, A.A., Degtyarev, A.I.: Automatic theorem proving. I. Cybernetics and System Analysis\u00a022(3), 290\u2013297 (1986)","journal-title":"Cybernetics and System Analysis"},{"issue":"4","key":"35_CR62","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1007\/BF01078915","volume":"23","author":"A.A. Voronkov","year":"1987","unstructured":"Voronkov, A.A., Degtyarev, A.I.: Automatic theorem proving. II. Cybernetics and System Analysis\u00a023(4), 547\u2013556 (1987)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR63","unstructured":"Lyaletski, A.: Gentzen calculi and admissible substitutions. In: Actes Preliminaires du Symposium Franco-Sovietique \u201cInformatika-91\u201d, Grenoble, France, pp. 99\u2013111 (October 1991)"},{"key":"35_CR64","unstructured":"Degtyarev, A.I., Kapitonova, J.V., Letichevski, A.A., Lyaletski, A.V., Morokhovets, M.K.: A brief historical sketch on Kiev school of automated theorem proving. In: Proceedings of the 2nd International THEOREMA Workshop, Linz, Austria, pp. 151\u2013156 (1998)"},{"key":"35_CR65","unstructured":"Kapitonova, Y., Letichevsky, A., Lyaletski, A., Morokhovets, M.: The Evidence Algorithm 2000 (a project). In: Proceedings of the 1st International Conference UkrPROG 1998, Kiev, Ukraine, pp. 68\u201370 (1998)"},{"key":"35_CR66","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/3-540-48242-3_4","volume-title":"Logic Programming and Automated Reasoning","author":"A. Degtyarev","year":"1999","unstructured":"Degtyarev, A., Lyaletski, A., Morokhovets, M.: Evidence Algorithm and sequent logical inference search. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol.\u00a01705, pp. 44\u201361. Springer, Heidelberg (1999)"},{"issue":"3","key":"35_CR67","first-page":"120","volume":"7","author":"K. Vershinin","year":"2000","unstructured":"Vershinin, K., Paskevich, A.: ForTheL \u2014 the language of formal theories. International Journal of Information Theories and Applications\u00a07(3), 120\u2013126 (2000)","journal-title":"International Journal of Information Theories and Applications"},{"key":"35_CR68","unstructured":"Lyaletski, A., Paskevich, A.: Goal-driven inference search in classical propositional logic. In: Proceedings of the International Workshop STRATEGIES 2001, Siena, Italy, pp. 65\u201374 (June 2001)"},{"key":"35_CR69","unstructured":"Aselderov, Z., Verchinine, K., Degtyarev, A., Lyaletski, A., Paskevich, A., Pavlov, A.: Linguistic tools and deductive technique of the System for Automated Deduction. In: Implementation of Logics, the 3rd International Workshop \u201cWIL 2002\u201d, Tbilisi, Georgia, pp. 21\u201324 (October 2002)"},{"key":"35_CR70","series-title":"Advances in Soft Computing","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/978-3-7908-1777-5_44","volume-title":"Intelligent Information Systems, the 11th International Symposium, IIS 2002","author":"A. Lyaletski","year":"2002","unstructured":"Lyaletski, A., Verchinine, K., Degtyarev, A., Paskevich, A.: System for Automated Deduction (SAD): Linguistic and deductive peculiarities. In: Klopotek, M.A., Wierzchon, S.T., Michalewicz, M. (eds.) Intelligent Information Systems, the 11th International Symposium, IIS 2002. Advances in Soft Computing, pp. 413\u2013422. Sopot, Poland. Physica-Verlag, Heidelberg (June 2002)"},{"key":"35_CR71","unstructured":"Paskevich, A.: Reasoning inside a formula. SEKI Report SR-02-06, University of Kaiserslautern (2002)"},{"key":"35_CR72","unstructured":"Verchinine, K., Degtyarev, A., Lyaletski, A., Paskevich, A.: SAD, a System for Automated Deduction: a current state. In: Kamareddine, F. (ed.) Proceedings of the Workshop on 35 Years of Automath, Edinburgh, Scotland (April 2002)"},{"issue":"4","key":"35_CR73","first-page":"388","volume":"10","author":"A. Lyaletski","year":"2003","unstructured":"Lyaletski, A.: Admissible substitutions in sequent calculi. International Journal on Information Theories and Applications\u00a010(4), 388\u2013393 (2003)","journal-title":"International Journal on Information Theories and Applications"},{"issue":"5","key":"35_CR74","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1023\/B:CASA.0000012086.56979.f4","volume":"39","author":"A. Lyaletski","year":"2003","unstructured":"Lyaletski, A.: Evidential paradigm: the logical aspect. Cybernetics and System Analysis\u00a039(5), 659\u2013667 (2003)","journal-title":"Cybernetics and System Analysis"},{"key":"35_CR75","unstructured":"Lyaletski, A., Verchinine, K., Paskevich, A.: On verification tools implemented in the System for Automated Deduction. In: Implementation Technology for Computational Logic Systems, the 2nd CoLogNet Workshop, ITCLS 2003, Pisa, Italy, pp. 3\u201314 (September 2003)"},{"key":"35_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/978-3-540-27818-4_17","volume-title":"Mathematical Knowledge Management","author":"A. Lyaletski","year":"2004","unstructured":"Lyaletski, A., Verchinine, K., Paskevich, A.: Theorem proving and proof verification in the system SAD. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 236\u2013250. Springer, Heidelberg (2004)"},{"key":"35_CR77","series-title":"Intelligent Information Processing and Web Mining","first-page":"293","volume-title":"Proceedings of the International IIS:IIPWM 2006 Conference","author":"B. Konev","year":"2006","unstructured":"Konev, B., Lyaletski, A.: Tableau method with free variables for intuitionistic logic. In: Klopotek, M., Wierzchon, S., Trojanowski, K. (eds.) Proceedings of the International IIS:IIPWM 2006 Conference. Intelligent Information Processing and Web Mining, Ustron, Poland, pp. 293\u2013305. Springer, Heidelberg (June 2006)"},{"issue":"1-2","key":"35_CR78","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10472-005-9017-7","volume":"46","author":"A. Lyaletski","year":"2006","unstructured":"Lyaletski, A.: Sequent forms of Herbrand theorem and their applications. Annals of Mathematics and Artificial Intelligence\u00a046(1-2), 191\u2013230 (2006)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"35_CR79","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/11853886_25","volume-title":"Logics in Artificial Intelligence","author":"A. Lyaletski","year":"2006","unstructured":"Lyaletski, A., Konev, B.: On Herbrand\u2019s theorem for intuitionistic logic. In: Fisher, M., van der Hoek, W., Konev, B., Lisitsa, A. (eds.) JELIA 2006. LNCS (LNAI), vol.\u00a04160, pp. 293\u2013305. Springer, Heidelberg (2006)"},{"key":"35_CR80","doi-asserted-by":"crossref","unstructured":"Lyaletski, A., Paskevich, A., Vershinin, K.: Deductive assistance in an intelligent linguistic environment. In: Proceedings of the 3th EIII Conference on Intelligent Systems (IEEE IS 2006), London, UK (September 2006)","DOI":"10.1109\/IS.2006.348446"},{"issue":"4","key":"35_CR81","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1016\/j.jal.2005.10.009","volume":"4","author":"A. Lyaletski","year":"2006","unstructured":"Lyaletski, A., Paskevich, A., Verchinine, K.: SAD as a mathematical assistant \u2014 how should we go from here to there? Journal of Applied Logic\u00a04(4), 560\u2013591 (2006)","journal-title":"Journal of Applied Logic"},{"key":"35_CR82","series-title":"Collegium Logicum","first-page":"41","volume-title":"Geodel Centenary 2006: Posters","author":"A. Lyaletski Sr.","year":"2006","unstructured":"Lyaletski Sr., A., Lyaletsky Jr., A.: Admissible substitutions and Herbrand\u2019s theorems for classical and intuitionistic logics. In: Baaz, M., Preining, N. (eds.) Geodel Centenary 2006: Posters, Vienna, Austria. Collegium Logicum, vol.\u00a0IX, pp. 41\u201345. Springer, Heidelberg (2006)"},{"key":"35_CR83","unstructured":"Paskevych, A.: Methodes de formalisation des connaissances et des raisonnements mathematiques: aspects appliques et theoriques. PhD thesis, Universite Paris 12 (2007) (in French)"},{"key":"35_CR84","series-title":"RISC-Linz Report Series","first-page":"77","volume-title":"Calculemus\/MKM 2007 \u2014 Work in Progress","author":"A. Paskevich","year":"2007","unstructured":"Paskevich, A., Verchinine, K., Lyaletski, A., Anisimov, A.: Reasoning inside a formula and ontological correctness of a formal mathematical text. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) Calculemus\/MKM 2007 \u2014 Work in Progress, RISC-Linz Report Series, Hagenberg, Austria, vol.\u00a007-06, pp. 77\u201391. University of Linz, Austria (2007)"},{"key":"35_CR85","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"398","DOI":"10.1007\/978-3-540-73595-3_29","volume-title":"Automated Deduction \u2013 CADE-21","author":"K. Verchinine","year":"2007","unstructured":"Verchinine, K., Lyaletski, A., Paskevich, A.: System for Automated Deduction (SAD): A tool for proof verification. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 398\u2013403. Springer, Heidelberg (2007)"},{"key":"35_CR86","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1109\/SYNASC.2008.92","volume-title":"Proceedings of the 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing","author":"A. Lyaletski","year":"2008","unstructured":"Lyaletski, A.: On some problems of efficient inference search in first-order cut-free modal sequent calculi. In: Proceedings of the 10th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania, pp. 39\u201346. IEEE Inc., Los Alamitos (2008)"},{"key":"35_CR87","unstructured":"Lyaletski, A.: Herbrand theorems: the classical and intuitionistic cases. In: Philosophical Logic, Poland. Studies in Logic, Grammar and Rhetoric, vol.\u00a014(27), pp. 101\u2013122 (2008)"},{"issue":"2\u20133","key":"35_CR88","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/s10817-007-9089-7","volume":"40","author":"A. Paskevich","year":"2008","unstructured":"Paskevich, A.: Connection tableaux with lazy paramodulation. Journal of Automated Reasoning\u00a040(2-3), 179\u2013194 (2008)","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR89","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-540-85110-3_47","volume-title":"Intelligent Computer Mathematics","author":"K. Verchinine","year":"2008","unstructured":"Verchinine, K., Lyaletski, A., Paskevich, A., Anisimov, A.: On correctness of mathematical texts from a logical and practical point of view. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 583\u2013598. Springer, Heidelberg (2008)"},{"key":"35_CR90","volume-title":"Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing","author":"A. Lyaletski","year":"2009","unstructured":"Lyaletski, A.: On Herbrand-like theorems for cut-free modal sequent logics. In: Proceedings of the 11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Timisoara, Romania. IEEE Inc., Los Alamitos (2009)"},{"key":"35_CR91","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D.: Proving theorems with the modification method. SIAM Journal of Computing\u00a04, 412\u2013430 (1975)","journal-title":"SIAM Journal of Computing"},{"key":"35_CR92","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/B978-044450813-3\/50003-5","volume-title":"Handbook of Automated Reasoning","author":"M. Davis","year":"2001","unstructured":"Davis, M.: The early history of automated deduction. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 3\u201315. MIT Press, Cambridge (2001)"},{"key":"35_CR93","unstructured":"Lifschitz, V.: Mechanical theorem proving in the USSR: The Leningrad school. Delphic Associates, Inc. (1986)"},{"issue":"1","key":"35_CR94","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00245018","volume":"5","author":"V. Lifschitz","year":"1989","unstructured":"Lifschitz, V.: What is the inverse method? Journal of Automated Reasoning\u00a05(1), 1\u201323 (1989)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"35_CR95","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli, A., Montanari, U.: An efficient unification algorithm. ACM Trans. on Prog. Languages and Systems\u00a04(2), 258\u2013282 (1982)","journal-title":"ACM Trans. on Prog. Languages and Systems"},{"issue":"1","key":"35_CR96","first-page":"17","volume":"159","author":"S.Y. Maslov","year":"1964","unstructured":"Maslov, S.Y.: The inverse method for establishing the deducibility in the classical predicate calculus. DAN SSSR\u00a0159(1), 17\u201320 (1964) (in Russian)","journal-title":"DAN SSSR"},{"issue":"6","key":"35_CR97","first-page":"239","volume":"19","author":"V.A. Matulis","year":"1964","unstructured":"Matulis, V.A.: The first All-union symposium on the problem of machine searching the logical deduction. UMN\u00a019(6), 239\u2013241 (1964) (in Russian)","journal-title":"UMN"},{"key":"35_CR98","unstructured":"McCune, W.: Otter 3.0 reference manual and guide. Tech. Report ANL-94\/6, Argonne National Laboratory, Argonne, USA"},{"key":"35_CR99","unstructured":"Prover9. Home page, http:\/\/www.cs.unm.edu\/~mccune\/prover9\/"},{"issue":"2\u20133","key":"35_CR100","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications\u00a015(2-3), 91\u2013110 (2002)","journal-title":"AI Communications"},{"issue":"1","key":"35_CR101","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. ACM\u00a012(1), 23\u201341 (1965)","journal-title":"ACM"},{"key":"35_CR102","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)"},{"key":"35_CR103","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/978-3-540-25984-8_15","volume-title":"Automated Reasoning","author":"S. Schulz","year":"2004","unstructured":"Schulz, S.: System Description: E\u00a00.81. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097, pp. 223\u2013228. Springer, Heidelberg (2004)"},{"key":"35_CR104","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1147\/rd.41.0002","volume":"4","author":"H. Wang","year":"1960","unstructured":"Wang, H.: Towards mechanical mathematics. IBM J. of Research and Development\u00a04, 2\u201322 (1960)","journal-title":"IBM J. of Research and Development"},{"key":"35_CR105","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-540-73595-3_38","volume-title":"Automated Deduction \u2013 CADE-21","author":"C. Weidenbach","year":"2007","unstructured":"Weidenbach, C., Schmidt, R., Hillenbrand, T., Rusev, R., Topic, D.: SPASS version 3.0. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 514\u2013520. Springer, Heidelberg (2007)"},{"key":"35_CR106","series-title":"Lecture Notes in Artificial Intelligence","first-page":"184","volume-title":"Seventeen provers of the world","year":"2006","unstructured":"Wiedijk, F. (ed.): The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600, 184 p. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14128-7_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,1]],"date-time":"2023-06-01T15:52:04Z","timestamp":1685634724000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14128-7_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141270","9783642141287"],"references-count":106,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14128-7_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}