Alexander Lyaletski; Alexandre Lyaletsky; Andrei Paskevich

Evidential Paradigm and SAD Systems: Features and Peculiarities

Full Text (PDF, 372KB), PP.1-11

Views: 0 Downloads: 0

Author(s)

Alexander Lyaletski ^1,* Alexandre Lyaletsky ² Andrei Paskevich ³

1. Institute of Mathematics and Computer Science, 5, Academiei street, Chisinau, MD 2028, Moldova

2. Taras Shevchenko National University of Kyiv, 60, Volodymyrska Street, Kyiv, 01033, Ukraine

3. LRI, Paris-Sud University, bât. 650 Ada Lovelace, Orsay, 91405, France

* Corresponding author.

DOI: https://doi.org/10.5815/ijmsc.2018.02.01

Received: 12 Sep. 2017 / Revised: 10 Jan. 2018 / Accepted: 13 Feb. 2018 / Published: 8 Apr. 2018

Index Terms

Automated reasoning, automated theorem proving, classical logic, intuitionistic logic, modal logic, Evidence Algorithm, formal language, formalized text, induction, number computation, symbolic transformation, deduction, paradigm, proof search, sequent calculus

Abstract

Research on automated reasoning systems based on a number of paradigms that support human activity in formalized text processing began in the late 1950s – early 1960s, when computer performance and memory space became sufficient for programming of complex intelligent processes. The so-called evidential paradigm was among them and it can be viewed as a way for integrating all reasonable paradigms oriented to the development of computer languages for representing formalized texts in the form most suitable for a user, formalization and development of the evidence of a computer-made proof step, creation of the information environment having influence on a current evidence of a machine proof step, and an active human-machine interaction. This work contains a brief description of the evidential paradigm and its implementation in the form of intelligent systems intended for the symbolic and deductive processing of mathematical texts focusing main attention on their features and peculiarities.

Cite This Paper

Alexander Lyaletski, Alexandre Lyaletsky, Andrei Paskevich,"Evidential Paradigm and SAD Systems: Features and Peculiarities", International Journal of Mathematical Sciences and Computing(IJMSC), Vol.4, No.2, pp.1-11, 2018.DOI: 10.5815/ijmsc.2018.02.01

Reference

[1]Glushkov V.M. Some problems in automata theory and artificial intelligence. Cybernetics and System Analysis. 1970:6(2):P. 17-27.

[2]Lyaletski A., Morokhovets M., Paskevich A. Kyiv School of Automated Theorem Proving: a Historical Chronicle. In book: “Logic in Central and Eastern Europe: History, Science, and Discourse”. USA:University Press of America; 2012:431-469.

[3]Letichevsky A.A., Lyaletski A.V., Morokhovets M.K. Glushkov’s Evidence Algorithm. Cybernetics and System Analysis. 2013:49(4):3-16.

[4]Lyaletski A., Morokhovets M. Evidential paradigm: a current state. Programme of the International Conference “Mathematical Challenges of the 21st Century”. USA: University of California, Los Angeles. 2000:48.

[5]Vershinin K., Paskevich A. ForTheL – the language of formal theories. International Journal of Information Theories and Applications. 2000:7(3):120-126.

[6]Kapitonova Yu.V., Vershinin K.P., Degtyarev A.I., Zhezherun A.P., Lyaletski A.V. System for processing mathematical texts. Cybernetics and System Analysis. 1979:15(2):209-210.

[7]Armando A., Bertoli P., Coglio A., Giunchiglia F., Meseguer J., Ranise S., Talcott C. Open Mechanized Reasoning Systems: A preliminary report. Proceedings of the Workshop on Integration of Deduction Systems (CADE 15). 1998.

[8]OpenMath.org: https://www.openmath.org

[9]The QED Manifesto: https://www.cs.ru.nl/~freek/qed/qed.html

[10]Mizar Home Page: http://mizar.uwb.edu.pl

[11]The Theorema system: https://www.risc.jku.at/research/theorema/software/

[12]Anufriyev F.V. An algorithm of theorem proving in logical calculi. , GIC, AS of UkrSSR, Kiev: Theory of Automata. 1969:3-26. (In Russian).

[13]Lyaletski A.V. On variant of Herbrand theorem for formulas in prefix form, Cybernetics and System Analysis (Historical Archive). 1981:17(1):125-129.

[14]Lyaletski A. Gentzen calculi and admissible substitutions. Actes Preliminaires du Symposium Franco-Sovietique “Informatika-91”, Grenoble, France: 1991:99- 111.

[15]Lyaletski A., Verchinine K., Degtyarev A., Paskevich A. System for Automated Deduction (SAD): Linguistic and deductive peculiarities. Advances in Soft Computing: Intelligent Information Systems, Proceedings of the 11th International Symposium, Sopot, Poland. 2002:413–422.

[16]Glushkov V.M., Kapitonova Yu.V., Letichevskii A.A., Vershinin K.P., Malevanyi N.P. Construction of a practical formal language for mathematical theories. Cybernetics and System Analysis. 1972:8(5):730-739.

[17]Glushkov V.M., Vershinin K.P., Kapitonova Yu.V., Letichevsky A.A., Malevanyi N.P., Kostyrko V.F. On a formal language for representation of mathematical texts. GIC, AS of UkrSSR, Kiev: Automated Proof Search in Mathematics. 1974:3-36. (In Russian).

[18]Degtyarev A.I., Lyaletski A.V. Deductive tools of the Evidence Algorithm. Abstracts of the All-union Conference “Methods of Mathematical Logic in Artificial Intelligence and Systematic Programming”, Palanga, Lithuania. 1980: I: 89-90. (In Russian).

[19]Lyaletski A.V., Degtyarev A.I. Logical inference in System for Automated Deduction, SAD. GIC, AS of UkrSSR, Kiev: Mathematical Foundations of Artificial Intelligence Systems. 1981: 3-11. (In Russian).

[20]Degtyarev A., Lyaletski A., Morokhovets M. Evidence Algorithm and sequent logical inference search. Lecture Notes in Computer Science. 1999:1705:44-61.

[21]Konev B., Lyaletski A. Tableau proof search with admissible substitutions. Proceedings of the International Workshop on First-order Theorem Proving, Koblenz, Germany. 2005:35-50.

[22]Lyaletski A. Mathematical text processing in EA-style: a sequent aspect. Journal of Formalized Reasoning (Special Issue: Twenty Years of the QED Manifesto). 2016:9(1):235-264.

[23]Verchinine K., Lyaletski A., Paskevich A. System for Automated Deduction (SAD): a tool for proof verification. Lecture Notes in Computer Science. 2007:4603:398-403.

[24]Vampire’s Home Page: http://www.vprover.org

[25]Classic SPASS Theorem Prover: https://www.mpi-inf.mpg.de/departments/automation-of-logic/software/ spass-workbench/classic-spass-theorem-prover/

[26]Otter and Mace2: https://www.cs.unm.edu/ mccune/otter/

[27]The E Theorem prover: http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html

[28]Prover9 and Mace4: https://www.cs.unm.edu/~mccune/mace4/

[29]Furstenberg H. On the infinitude of primes. American Mathematical Monthly. 1955:62(5): 353.

International Journal of Mathematical Sciences and Computing (IJMSC)