×

zbMATH — the first resource for mathematics

Evidence algorithm and inference search in first-order logics. (English) Zbl 1356.03055
Summary: In the early 1970s, in Kiev, research on automated theorem proving started in the framework of the so-called Evidence Algorithm (EA) programme, having some general features with the Mizar project and, in particular, being oriented to the development of such a technique for inference search in various first-order logics that satisfies the following requirements: the syntactic form of a problem under consideration should be preserved, logical transformations should be performed in the signature of the original theory, equality handling should be separated from deduction. For these reasons, the main efforts of the EA developers were concentrated on modifying the sequent formalism to obtain sufficient efficiency in sequent proof search, although some attention was paid to the construction of resolution-type methods. This paper contains a brief summary of the author’s results in this field. It is shown that the proposed approach enables to construct (sound and complete) quantifier-rule-free sequent calculi for classical and non-classical logics, including the intuitionistic and modal cases. Besides, two sound and complete resolution-type methods based on a certain generalization of the notion of a clause are described. One of them gives the possibility to interpret Maslov’s inverse method in resolution terms.

MSC:
03B35 Mechanization of proofs and logical operations
03F07 Structure of proofs
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
ForTheL; Mizar; SAD
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Glushkov, VM, Some problems in the theories of automata and artificial intelligence, Cybern. Syst. Anal., 6, 17-27, (1970) · Zbl 0242.68056
[2] Lyaletski, A., Morokhovets, M., Paskevich, A.: Kyiv school of automated theorem proving: a historical chronicle. In: Logic in Central and Eastern Europe: History, Science, and Discourse, pp. 431-439. University Press of America, New York (2012) · Zbl 0139.12303
[3] Glushkov, VM, “intelligent” machines and the mental activity of a human, Sov. School, 2, 87-91, (1962)
[4] Matulis, VA, The first all-union symposium on the problem of machine searching the logical deduction, UMN, 19, 239-241, (1964)
[5] Anufriyev, F.V.: An algorithm of search of theorem proofs in logical calculi. In: Theory of Automata, pp. 3-26. GIC AS UkrSSR, Kiev (1969). (in Russian)
[6] Malashonok, A.I.: Obviousness of theorem proving and complexity of proof search in the auxiliary goal search method. In: Computer-Aided Theorem Proving in Mathematics, pp. 100-108. GIC AS UkrSSR, Kiev (1974). (in Russian) · Zbl 0881.68109
[7] Kanger, S.: Simplified proof method for elementary logic. In: Comp. Program. and Form. Systems. Stud. in Logic, pp. 87-93, North-Holland Publ. Co., Amsterdam (1963) · Zbl 0217.00902
[8] Anufriyev, FV; Kostiakov, VM; Malashonok, AI, Algorithm and computer experiments for searching theorem proofs in the predicate calculus, Cybern. Syst. Anal., 8, 777-783, (1972)
[9] Robinson, JA, A machine-oriented logic based on the resolution principle, ACM, 12, 23-41, (1965) · Zbl 0139.12303
[10] Lifschitz, V, What is the inverse method?, J. Autom. Reason., 5, 1-23, (1989) · Zbl 0694.03010
[11] Maslov, SYu, The inverse method for establishing the deducibility in the classical predicate calculus, DAN SSSR, 159, 17-20, (1964)
[12] Degtyarev, A.I.: On the usage of functional reflexivity axioms in the P&R refutation procedure. Preprint 75-28, GIC AS UkrSSR, Kiev (1975). (in Russian)
[13] Degtyarev, A.I.: A monotonic paramodulation strategy. In: Abstracts of V All-union Conference on Mathematical Logic, vol. 39, Novosibirsk, USSR (1979). (in Russian) · Zbl 0694.03010
[14] Degtyarev, A.I.: A strict paramodulation strategy. Volume 12 of Semiotics and Informatics, pp. 20-22. All-union Institute of Scientific and Technical Information, Moscow (1979). (in Russian)
[15] Morokhovets, M.K.: On proof editing. In: Computer-Aided Processing of Mathematical Texts, pp. 53-61. GIC AS UkrSSR, Kiev (1980). (in Russian)
[16] Kapitonova, YV; Vershinin, KP; Degtyarev, AI; Zhezherun, AP; Lyaletski, AV, System for processing mathematical texts, Cybern. Syst. Anal., 15, 209-210, (1979)
[17] Degtyarev, A.I., Lyaletski, A.V.: Logical inference in the system of automated proving, SAD. In: Mathematical Foundations of Artificial Intelligence Systems, pp. 3-11. GIC AS UkrSSR, Kiev (1981). (in Russian)
[18] Lyaletski, A.V.: Generating sufficient statements in the SAD system. In: Abstracts of III All-Union Conference “Application of the Methods of Mathematical Logic”, pp. 65-66. Tallinn, USSR (1983). (in Russian)
[19] Atayan, VV; Morokhovets, MK, Combining formal derivation search procedures and natural theorem proving techniques in an automated theorem proving system, Cybern. Syst. Anal., 32, 442-465, (1996) · Zbl 0881.68109
[20] Vershinin, K; Paskevich, A, Forthel—the language of formal theories, Int. J. Inf. Theor. Appl., 7, 120-126, (2000)
[21] Lyaletski, A., Verchinine, K., Degtyarev, A., Paskevich, A.: SAD, a system for automated deduction: a current state. In: Proceedings of the Workshop on 35 Years of Automath, Edinburgh, Scotland (2002) · Zbl 1088.68773
[22] Lyaletski, A., Verchinine, K., Degtyarev, A., Paskevich, A.: System for automated deduction (SAD): linguistic and deductive peculiarities. In: Intelligent Information Systems (IIS 2002). Advances in Soft Computing, pp. 413-422. Physica-Verlag (2002) · Zbl 1088.68773
[23] Lyaletski, A., Degtyarev, A., Morokhovets, M.: Evidence Algorithm and sequent logical inference search. In: Logic for Programming and Automated Reasoning (LPAR’99). Lecture Notes in Computer Science, vol. 1705, pp. 44-61 (1999) · Zbl 0938.03018
[24] Robinson, J.A.: An overview of mechanical theorem proving. In: Lecture Notes in Operations Research and Mathematical Systems, vol. 28, pp. 2-20 (1970) · Zbl 0694.03010
[25] Lyaletski, A.V.: On a calculus of c-disjuncts. In: Mathematical Issues of Intelligent Machines Theory, pp. 34-48. GIC AS UkrSSR, Kiev (1975). (in Russian)
[26] Lyaletski, A.V., Malashonok, A.I.: A calculus of c-disjuncts based on the clash-resolution rule. In: Mathematical Issues of Intelligent Machine Theory, pp. 3-33. GIC AS UkrSSR, Kiev (1975). (in Russian)
[27] Lyaletski, A.V.: On minimal inferences in the calculi of c-disjuncts. In: Issues of the Theory of Robots and Artificial Intelligence, pp. 34-48, GIC AS UkrSSR, Kiev (1975). (in Russian)
[28] Lee, Ch., Chang, RCh.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, New York (1973) · Zbl 0263.68046
[29] Maslov, SYu, Proof-search strategies for methods of resolution type, Mach. Intell., 6, 77-90, (1971) · Zbl 0281.68042
[30] Kuechner, D, On the relation between resolution and maslov’s inverse method, Mach. Intell., 6, 73-76, (1971) · Zbl 0263.68049
[31] 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, 3rd International Workshop (WIL 2002), pp. 21-24, Tbilisi, Georgia (2002)
[32] Lyaletski, A, Evidential paradigm: the logical aspect, Cybern. Syst. Anal., 39, 659-667, (2003) · Zbl 1097.68631
[33] Lyaletski, A., Verchinine, K., Paskevich, A.: Theorem proving and proof verification in the system SAD. In: Mathematical Knowledge Management: Third International Conference (MKM 2004). Lecture Notes in Computer Science, vol. 3119, pp. 236-250 (2004) · Zbl 1108.68573
[34] 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, pp. 39-46, Timisoara, Romania (2008)
[35] Gentzen, G.: Untersuchungenuber das logische schliessen. Math. Z. 39(2), 176-210 (1934); 39(3), 405-431 (1935). (in German) · Zbl 0010.14501
[36] 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 the Issues of Robots Construction, pp. 28-35. GIC AS UkrSSR, Kiev (1979). (in Russian)
[37] Lyaletski, AV, A variant of herbrand’s theorem for formulas in prenex form, Cybern. Syst. Anal., 17, 125-129, (1981) · Zbl 0462.68074
[38] Wallen, L.: Automated Proof Search in Non-classical Logics. Oxford University Press, Oxford (1990) · Zbl 0782.03003
[39] Hiroakira, O.: Proof-theoretic methods in non-classical logic—an introduction. In: Theories of Types and Proofs, pp. 207-254. Mathematical Society of Japan, Tokyo (1998) · Zbl 0947.03073
[40] Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Wiley, New York (1988) · Zbl 0605.03004
[41] Mints, G.: Herbrand theorem. In: Mathematical Theory of Logical Inference, pp. 311-350, Nauka, Moscow (1967). (in Russian)
[42] Waaler, A., Antonsen, R.: A free variable sequent calculus with uniform variable splitting. In: Lecture Notes in Computer Science, vol. 2796, pp. 214-229 (2003) · Zbl 1274.03026
[43] Lyaletski, A.V.: A note on the cut rule. In: Abstracts on the International Conference “Mal’tsev meeting”, vol. 137, Novosibirsk (2011)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.