{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:38:20Z","timestamp":1743140300832,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540230298"},{"type":"electronic","value":"9783540278184"}],"license":[{"start":{"date-parts":[[2004,1,1]],"date-time":"2004-01-01T00:00:00Z","timestamp":1072915200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-27818-4_17","type":"book-chapter","created":{"date-parts":[[2010,2,25]],"date-time":"2010-02-25T14:26:47Z","timestamp":1267108007000},"page":"236-250","source":"Crossref","is-referenced-by-count":8,"title":["Theorem Proving and Proof Verification in the System SAD"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Lyaletski","sequence":"first","affiliation":[]},{"given":"Andrey","family":"Paskevich","sequence":"additional","affiliation":[]},{"given":"Konstantin","family":"Verchinine","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"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: Proc. 3rd International Workshop on the Implementation of Logics, Tbilisi, Georgia, pp. 21\u201324 (2002)","key":"17_CR1"},{"unstructured":"Bakhvalov, N.I., Zhidkov, N.P., Kobelkon, G.M.: Computational Methods (in Russian). BINOM Publisher (2003)","key":"17_CR2"},{"unstructured":"Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J., Gim\u00e9nez, E., Herbelin, H., Huet, G., Mu\u00f1oz, C., Murthy, C., Parent, C., Paulin, C., Sa\u00efbi, A., Werner, B.: The Coq proof assistant reference manual \u2013 version v6.1. Technical Report 0203, INRIA (1997)","key":"17_CR3"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-63104-6_23","volume-title":"Automated Deduction - CADE-14","author":"C. Benzm\u00fcller","year":"1997","unstructured":"Benzm\u00fcller, C., Cheikhrouhou, L., Fehrer, D., Fiedler, A., Huang, X., Kerber, M., Kohlhase, M., Konrad, K., Meier, A., Melis, E., Schaarschmidt, W., Siekmann, J.H., Sorge, V.: Omega: Towards a mathematical assistant. In: McCune, W. (ed.) CADE 1997. LNCS, vol.\u00a01249, pp. 252\u2013255. Springer, Heidelberg (1997)"},{"key":"17_CR5","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":"17_CR6","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1145\/258726.258853","volume-title":"ISSAC 1997 \u2013 Proc. International Symposium on Symbolic and Algebraic Computation","author":"B. Buchberger","year":"1997","unstructured":"Buchberger, B., Jebelean, T., Kriftner, F., Marin, M., Tomuta, E., Vasaru, D.: A survey of the Theorema project. In: K\u00fcchlin, W. (ed.) ISSAC 1997 \u2013 Proc. International Symposium on Symbolic and Algebraic Computation, Maui, Hawaii, USA, pp. 384\u2013391. ACM Press, New York (1997)"},{"key":"17_CR7","volume-title":"Electronic Notes in Theoretical Computer Science","author":"O. Caprotti","year":"2001","unstructured":"Caprotti, O., Cohen, A.M.: Integrating computational and deduction systems using OpenMath. In: Armando, A., Jebelean, T. (eds.) Electronic Notes in Theoretical Computer Science, vol.\u00a023. Elsevier, Amsterdam (2001)"},{"key":"17_CR8","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)"},{"key":"17_CR9","first-page":"126","volume-title":"Symbolic Computation and Automated Reasoning: The CALCULEMUS 2000 Symposium","author":"A. Degtyarev","year":"2001","unstructured":"Degtyarev, A., Lyaletski, A., Morokhovets, M.: On the EA-style integrated processing of self-contained mathematical texts. In: Kerber, M., Kohlhase, M. (eds.) Symbolic Computation and Automated Reasoning: The CALCULEMUS 2000 Symposium, pp. 126\u2013141. A.K. Peters Ltd., USA (2001)"},{"key":"17_CR10","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen uber das Logische Schliessen. Math. Zeit.\u00a039, 176\u2013210 (1934)","journal-title":"Math. Zeit."},{"key":"17_CR11","first-page":"3","volume":"2","author":"V.M. Glushkov","year":"1970","unstructured":"Glushkov, V.M.: Some problems of automata theory and artificial intelligence (in Russian). Kibernetika\u00a02, 3\u201313 (1970)","journal-title":"Kibernetika"},{"doi-asserted-by":"crossref","unstructured":"Graham, R.L.: Rudiments of Ramsey Theory. AMS (1981)","key":"17_CR12","DOI":"10.1090\/cbms\/045"},{"key":"17_CR13","first-page":"2017","volume-title":"Handbook for Automated Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Model elimination and connection tableau procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook for Automated Reasoning, vol.\u00a0II, pp. 2017\u20132116. Elsevier Science, Amsterdam (2001)"},{"unstructured":"Lyaletski, A., Morokhovets, M.: Evidential paradigm: a current state. In: Program of International Conference Mathematical Challenges of the 21st Century, University of California, Los Angeles, p. 48 (2000)","key":"17_CR14"},{"key":"17_CR15","series-title":"Advances in Soft Computing","first-page":"413","volume-title":"Proc. IIS 2002 Symposium on Intelligent Information Systems 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.) Proc. IIS 2002 Symposium on Intelligent Information Systems 2002, Sopot, Poland, June 3-6, 2002. Advances in Soft Computing, pp. 413\u2013422. Physica-Verlag, Heidelberg (2002)"},{"unstructured":"Lyaletski, A., Verchinine, K., Paskevich, A.: On verification tools implemented in the System for Automated Deduction. In: Proc. 2nd CoLogNet Workshop on Implementation Technology for Computational Logic Systems (ITCLS 2003), Pisa, Italy, pp. 3\u201314 (2003)","key":"17_CR16"},{"doi-asserted-by":"crossref","unstructured":"McCune, W.: Otter 3.0 reference manual and guide. Tech. Report ANL-94\/6, Argonne National Laboratory, Argonne, USA (1994)","key":"17_CR17","DOI":"10.2172\/10129052"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","author":"T. Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle\/HOL. LNCS, vol.\u00a02283. Springer, Heidelberg (2002)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"key":"17_CR20","first-page":"91","volume":"15","author":"A. Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Communications\u00a015, 91\u2013110 (2002)","journal-title":"AI Communications"},{"key":"17_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/3-540-58156-1_18","volume-title":"Automated Deduction - CADE-12","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C.B., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 252\u2013266. Springer, Heidelberg (1994), See also: http:\/\/tptp.org"},{"unstructured":"Trybulec, A., Blair, H.: Computer assisted reasoning with Mizar. In: Proc. 9th International Joint Conference on Artificial Intelligence, pp. 26\u201328 (1985)","key":"17_CR22"},{"key":"17_CR23","volume-title":"Proc. Workshop on 35 Years of AUTOMATH","author":"K. Verchinine","year":"2002","unstructured":"Verchinine, K., Degtyarev, A., Lyaleyski, A., Paskevich, A.: SAD, a System for Automated Deduction: a current state. In: Kamareddine, F. (ed.) Proc. Workshop on 35 Years of AUTOMATH. Heriot-Watt University, Edinburgh (2002)"},{"issue":"3","key":"17_CR24","first-page":"120","volume":"7","author":"K. Vershinin","year":"2000","unstructured":"Vershinin, K., Paskevich, A.: ForTheL \u2013 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":"17_CR25","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/3-540-48660-7_34","volume-title":"Automated Deduction - CADE-16","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: System description: Spass version 1.0.0. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 378\u2013382. Springer, Heidelberg (1999)"},{"key":"17_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/3-540-45620-1_11","volume-title":"Automated Deduction - CADE-18","author":"J. Zimmer","year":"2002","unstructured":"Zimmer, J., Kohlhase, M.: System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning. In: Voronkov, A. (ed.) CADE 2002. LNCS, vol.\u00a02392, pp. 139\u2013143. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Mathematical Knowledge Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-27818-4_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T07:49:35Z","timestamp":1558856975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-27818-4_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540230298","9783540278184"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-27818-4_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}