DonNTU   Masters' portal

Abstract

Content

Introduction

Automatic theorem proving goes back to the fundamental works of Herbrand, who in the 30s of XX century. suggested that the mechanical process of deductive inference. In the 60 years the efforts of Newell and Simon created a general solver of problems, proving theorems of formal logic developed by Russell and Whitehead[1], who believed that mathematics is enough to have a formal derivation of theorems from basic axioms.

However, the results of the Church[2 and Turing[3] on the undecidability of first-order predicate logic to some extent pushed the Herbrand work in the background. Interest in them has increased only in the 60th, when Gilmour sold Erbranov’s procedure output to the computer. Indeed, if there is no procedure for checking inconsistency (validity) of formulas of predicate logic of first order, the most that can do - is to check the inconsistency of (validity) of the formula, if it really is. Gilmore was able to prove with the help of some simple procedures Herbrand theorems of propositional logic and first-order predicate logic, but the program is faced with insurmountable difficulties in proving more difficult theorems of predicate logic.

Slightly better was the method of Davis and Putnam[4-7], with which were proved some theorems of first-order predicate logic, is not proven Gilmour. In 1964-1965 independently came inverse method of establishing deducibility Maslow and Robinson's resolution principle [8] . In those same years, Shanin[9]and his colleagues developed several versions of the algorithm search engine natural inference in the propositional calculus (ALPEV). Development versions of ALPEV algorithms and computer output based on the inverse method and the principle of the resolution showed the fundamental possibility of machine proofs of theorems.

1. Relevance of topic

Now it is assumed that automated reasoning based on formal logic are weak theorem proving techniques, and purely syntactic methods to control the search are not able to handle the huge search space in solving problems of practical complexity. Therefore, alternative search methods are informal, ad hoc strategies, heuristics and common sense reasoning that people use when solving problems.

However, the methods of proving theorems, based on formal logic, such as first-order predicate logic, are still a powerful weapon in the manipulation of knowledge and cannot be ignored. The continuing interest in automatic theorem proving is the symbiosis of man and machine in solving complex problems, when the proportion of people are the problem of decomposition of complex problems in a number of sub problems, finding the right heuristics to reduce the search space, and brought the automatic solver to perform the formal manipulation of the knowledge-based techniques withdrawal. A striking example of this symbiosis are the expert system based on rules that have found wide application in medicine, geology, production management, transport, thermal and nuclear power plants, etc.

Of course, dominant in automatic theorem proving method of resolution is not a panacea for all ills that accompany the procedure, proofs, and we may hope for the emergence of more sophisticated procedures of deductive inference.

Master's research is devoted to the development of relevant scientific inference problem on a graph connections, which would reduce the execution time and amount of resources required to implement the algorithm.

2. The purpose and objectives of research

The aims of this research are an analysis of existing methods and developing new method of the resolution.

The main objectives of research:

  1. Analysis of existing methods of resolution and heuristic functions.
  2. Finding ways to reduce the resource intensity of the problem by developing their own representation of the graph relations.
  3. Develop your own heuristic function which allows to minimize the expansion of the graph when the method of resolution.

Object of research: logical conclusion of the graph relations.

Subject of research: heuristic function of method resolution.

3. Scope of applications

After the appearance of the first modern computers began to develop engine technology with fantastic speed. Today, we see that the machines are used not only for solving difficult computational problems, such as the implementation of the fast Fourier transform or matrix inversion, a high order. They are required to perform such tasks, and that would be called intelligent if they were done by people. Examples of such problems are programming, the creation of systems that respond to the questions, and theorem proving. Artificial intelligence - is the area of computational mathematics that deals with such problems.

There are many tasks that can be transformed into proofs of the problem. Here are some of them:

  1. In the question-response systems, the approval may be represented by logical formulas. Then, to answer the question, using these facts, we prove that the formula corresponding to the answer is deducible from the formulas representing these facts.
  2. In the problem analysis program, we can describe the execution of the program by A, and the condition that the program is finished, the other by B. Then check that the program is finished, is equivalent to proving that the formula B follows from A.
  3. In the graph isomorphism problem we want to know whether the graph is isomorphic to a sub graph of another graph. This problem is not only of mathematical interest, this problem is practical. For example, the structure of organic compounds can be described by a graph. Therefore, checking whether a substructure of a structure of an organic compound structure of another organic compound, there is the isomorphism problem. To solve it, we can describe the graphs of the formulas. Thus, the problem can be formulated as a problem of proof that the formula that represents the graph follows from the formula that represents the other graph.
  4. In the problem of converting the state has a set of states and a set of operators over the states. When one of the operators is applied to the state, we obtain a new state. Based on the initial state, will try to find a sequence of operators that transforms the initial state to some desired. In this case, we can describe the state transition rules and logical formulas. Consequently, the conversion to the desired initial state can be considered as verification that the formula that represents the desired state, follows from the formula, which represents both state and transition rules.

Since many problems can be formulated as a theorem proving problem, the problem of automating proofs is an important area in artificial intelligence.

4. Review of research and development

The method of resolution is an important part of automatic theorem proving. This method is widely studied by scientists from all over the world. The research method resolution continues today.

4.1 Review of international sources

Man has long sought to find a common procedure for the resolution theorem proving. This desire is clearly seen in Leibniz[10] works (1646—1716); it was resurrected by Peano[11] at the beginning of this century, and the school of Gilbert in the 20's. A very important theorem was proved by Erbran in 1930, he proposed an automatic method for proving theorems. Unfortunately, his method was very difficult to implement because it was very labor intensive with manual analysis. With the invention of the computer logic again expressed an interest in automatic theorem proving. In 1960, Mr. Herbrand's Theorem years has been implemented on a computer Gilmour, and was soon followed by a more efficient procedure, proposed by Davis and Putnam.

Important progress in automatic theorem proving was made by J.A. Robinson in 1965 he developed the only inference rule - the principle of the resolution, which proved to be extremely effective and readily available for implementation on a computer. Since then, many improvements have been invited to the principle of the resolution. Automatic proof of the theory is applied in many areas such as program analysis, deductive system of answers to the questions of problem solving and technology of robots. The number of applications continues to grow.

Separate programs, and study the search for solutions to logical problems in 1945 - 1964. Creates a program that automatically proving theorems (ALPEV LOMI) in Leningrad (LOMI - Leningrad Department of Steklov Institute. Of Mathematics). It is based on the original return S.Yu. Maslov's output similar to the method of Robinson's resolutions.

In the approach based on natural deduction (natural deduction), which was introduced by Gerhard Gentzen[12] and Stanislav Yaskovskiy, the focus was not on the axiomatic systems, and the rules of inference. Natural deduction is called the "natural" because it does not require conversion to normal form (inconvenient for human perception), and also due to the fact that it applies these rules of inference that seem natural to people. Pravitts devoted to the description of natural deduction, an entire book. Gale used Gentzen's approach to explain the theoretical foundations of automated deduction.

It is an important milestone in the development of a deep mathematical analysis of first-order logic was the invention of forms of representation in the form of implicational expressions (clausal form). Whitehead and Russell described the passage of the so-called rules (rules of passage) (in fact, this term belongs Erbran), which are used to move the quantifiers to the front of the formulas. Toralfom Skolem[13] was fairly promptly offered Skolem’s constants and Skolem’s functions. General procedure scolemization, along with the important concept of the universe Herbrand.

It is extremely important role in the development of automated methods of generating discussion, both before and after introduction of the resolution rule Robinson, played by Herbrand's theorem, named in honor of French logic of Jacques Herbrand. This is reflected in the applicable term our Herbrand’s universe rather than the universe of Skolem despite the fact that this concept actually opened by Skolem. In addition, Herbrand may be regarded as the inventor of the unification operation. Godel[14], based on the idea of Skolem and Herbrand, was able to show that for first-order logic, there is full evidence of the procedure. Alan Turing and Alonzo Church showed almost simultaneously, using a different proof that the problem of determining the validity of first-order logic has no solution. In the excellent Enderton’s book[15] all these results are described in a rigorous but difficult to understand manner.

By modern sources include A. Averin[16] and V. Vagin[17]are actively engaged in research of the parallel output connections on the graph. We should also mention the interesting work of Commandantsky V.E.[18] on the resolution method in many-valued logics. It should also be noted Aseev's I.[24] research.

4.2 Review of national sources.

In the Kiev National University. Shevchenko A. Lyaletsky and A. Paskevich[19] investigated using of Automated Deduction System for verification of mathematical texts and linguistic problem of automating proofs of theorems in formalized theories.

In the National Technical University of Ukraine KPI Aselderov Z.M. and Molchanovsky A. presented the work of organizing the knowledge base in the system of automatic theorem proving SAD.

4.3 Review of local sources

The Institute of Artificial Intelligence and Computer Science at DonNTU scientific work in the field of automatic theorem proving involved Grunsky I.S., Kozlovsky V.A., Barashko A.S.[20-22], Volchenko M.V.[23], etc.

Conclusion

Since many problems can be formulated as a theorem proving problem, the problem of automating proofs is an important area in artificial intelligence. Thanks to the tireless efforts of many researchers has been made great progress in the use of machines in order to prove theorems.

Master's research devoted to actual scientific problem of the development of the inference algorithm on the graph relations. In the trials carried out:

  1. Highlights the key features of the method of resolution of the graph relations.
  2. The possibility of creating an optimal heuristics.
  3. A number of experiments to improve the representation of the graph relations to reduce the resource intensity of the algorithm.

Further studies focused on such aspects:

  1. Creating an optimal heuristic function for the method of resolution of the graph relations.
  2. Partitioning a graph into sub graphs ties to reduce the execution time of the algorithm.
  3. Development of a demonstration system that implements the proposed algorithm in the master's work method resolution.

Writing this master's work is not yet complete. Final completion: December 2012. The full text of the work and materials on the topic can be obtained from the author or his leader after that date.

References

  1. Уайтхед А.Н. Основания математики: в 3 т. / Альфред Н. Уайтхед, Бертран Рассел; пер. с англ. Ю.Н. Радаева, И.С. Фролова; под ред. Г.П. Ярового, Ю.Н. Радаева. – Самара: Книга, 2005–2006. – 234 c.
  2. Alonzo Church, A Bibliography of Symbolic Logic, 1666–1935. – 164 pp.
  3. Alan M. Turing – Collected works of A. M. Turing. Mathematical logic. Elsevier, Amsterdam, The Netherlands, 2001. – 745 pp.
  4. Патнэм Х. Философия сознания / Пер. с англ. Л. Б. Макеевой, О. А. Назаровой, А. Л. Никифорова; предисл. Л. Б. Макеевой. М.: Дом интеллектуальной книги, 1999. 240 с.
  5. Патнэм Х. Разум, истина и история / Пер. с англ. Т.А. Дмитриева, М.В. Лебедева. – М.: Праксис, 2002. – 296 с.
  6. Патнэм Х. Как нельзя говорить о значении (комментарий к статье Дж. Дж. Смарта) // Структура и развитие науки. М., 1978. С. 396–418
  7. Патнэм Х. Значение и референция // Новое в зарубежной лингвистике. Вып. 13. М., 1982. С. 377–390.
  8. Робинсон А. Введение в теорию моделей и мета–математику алгебры. // Серия «Математическая логика и основания математики». М.: Наука, 1967, 378 с.
  9. Шанин Н.А. Алгорифм машинного поиска естественного логического вывода в исчислении высказываний // М.: Наука, 1965, 38 с.
  10. Лейбниц Г. В. Математические работы в переводе А. П. Юшкевича // Успехи Мат. Наук, – М.: Наука, 2003. – 235 с.
  11. Peano G. "The principles of arithmetic, presented by a new method" in Jean van Heijenoort, 1967. A Source Book in Mathematical Logic, 1879–1931. Harvard Univ. pp. 83–97.
  12. Генцен Г. Непротиворечивость чистой теории чисел. // Математическая теория логического вывода. М.: Наука, 1967, C. 77–153.
  13. Skolem, Th. (1934) Uber die Nicht–charakterisierbarkeit der Zahlenreihe mittels endlich oder abzahlbar unendlich vieler Aussagen mit ausschliesslich Zahlenvariablen. Fundam. Math. 23, pp. 150–161.
  14. John W. Dawson, Jr. Logical Dilemmas: The Life and Work of Kurt Godel. AK Peters, Ltd., 1996. – 247 pp.
  15. Enderton H.B. A Mathematical Introduction to Logic // 2nd ed., Academic Press, 2001. 326 pp.
  16. Аверин А.И., Вагин В.Н. Параллелизм в дедуктивном выводе на графовых структурах,Автомат. и телемех., 2001, № 10. C. 54–64.
  17. Вагин В.Н., Головина Е.Ю., Загорянская А.А., Фомина М.В. Достоверный и правдоподобный вывод в интеллектуальных системах Монография. Под ред. В.Н. Вагина и Д.А.Поспелова. М.: Изд. 2–ое исправл. и дополн. Физматлит, 2008, 714 с.
  18. Комендантский В.Е. Метод резолюций в смешанной логике Поста // Труды XVI научно–исследовательского семинара логического центраИФРАН. М.: ИФРАН, 2002. С. 64–74.
  19. Анисимов А.В., Вершинин К.П., Лялецкий А.В., Паскевич А.Ю. //Система автоматизации дедукции (САД) как средство обработки формальных компьютерных заданий . The Fourth International Conference Theoretical and Applied Aspects of Program Systems Development (TAAPSD’2007). Abstracts (4–9 September, 2007, Berdyansk, Ukraine), Київ, Р. 9–14.
  20. Богомолов А.М., Барашко А.С., Грунский И.С. Эксперименты с автоматами. – Киев: Наукова думка, 1973. – 144 с.
  21. Богомолов А.М., Грунский И.С., Сперанский Д.В. Контроль и преобразование дискретных автоматов. – Киев: Наукова думка, 1975. – 176 с.
  22. Грунский И.С., Козловский В.А. Синтез и идентификация автоматов. – Киев: Наукова думка, 2004. – 246 с.
  23. Волченко М.В. Представление термов для алгоритма резолюции логики высказываний. Информатики и компьютерные технологии / Материалы V международной конференции. – Донецк: Изд–во ДГТУ, 2009.
  24. Асеев И.И. – Алгебра степенных операторов [Электронный ресурс]. – Режим доступа: http://sceptic-ratio.narod.ru/ma.htm