Brief description: The machine proves that the use of computer certification theorem, also known as the agencical certificate or automatic proof of theorem. As an important topic of computer science, its research and development has been about 50 years of history. In this article, it will try to show you the basic ideas and methods of the machine proven.
Keywords: machine certificate, interpretation of the form of system P, Temporatory method, judgment, computer-aided proof, proof algorithm
In the science of each door, there is reasonable and argument; especially in mathematics, it is necessary to establish theorem through reasoning and prove to establish a proof to introduce other propositions through the rules of logic reasoning. Propositions from them are called premise, and the propositions launched are called conclusions. Let's take a look at an example. When the mathematical analysis of the continuity of the study function, it proves the following premise
1) Function f (x) continuous in closed interval [A, B], 2) f (a) and f (b) hemaphys. Can introduce conclusions
3) There is C, so that the closed interval [A, B] in 1) in 1) is changed to the opening section (A, B), then the changed 1) and 2) The premise cannot be launched 3) this conclusion.
This work (reasoning and proof) has always been made by mathematicians; this is their livelihood. However, is there any other possibility? For example, will you prove the machine to demonstrate and reasonine mathematics? This is a meaningful and difficult job; reasoning and prove is an embodiment of intelligence, and artificial intelligence is one of the dreams of humanity. This requires several conditions.
First, we have to make reasoning and certificates as a research object, and study more. In the past, any mathematical branch has its own research object, but does not study the logical reasoning rules they work together; the proactive logic is such a condition, which puts reasoning and prove as a mathematical object. Only human thinking activities such as reasoning and certification have sufficient understanding, we may hand over this work to the machine. Second, the computer must have considerable development. This is no doubt, but it is often facilitating each other, but it is not perfect, the other can develop. With these conditions, the machine proven will become possible if needed, and the fact that this needs will be produced. Below we will try to show the mystery of machine certificates. However, this paper is informal academic papers, so you will see that it is not strictly description and formal tool alternate. But the introduction of machine proves is the purpose of this article.
Of course, you need to briefly quote the knowledge of the progeny logic. Mathematical logic is studied as a mathematical object in reasoning and proven, starting from Leibniz tries to work on thinking symbolization. It is now fruitful and has a rich knowledge system. Generally, the undergraduate phase can be exposed to proposition logic and predicate logic, and the graduate phase will study other high-aller logic content (computer professional teaching programs). We use the simplest proposition logic "Interpretation of the System P" as an example to let you first understand the characteristics of the logic.
The main feature of mathematical logic is "formal", specifically, is the formation of "mathematical reasoning". And the popularity is the premise and conclusions, and the premise is "symbolized" as a system, form system. The form system has a strict definition, where you can temporarily think that the form system consists of four collections: alphabet or symbol library, word set or formula set, axiom set, rule set; axiom set is a subset of formulas The rule set is the comparative composition of the formula set.
Such as the definition of the system P in the form of reasoning:
The alphabet of the P: (1) Propositional variables: P1, P2, ..., PN, ...; (2) coupled words: ┐, →; (3) auxiliary symbol: (,); p The formula is defined as follows: (1) The proposition variable element is formula; (2) If α is formula, (┐α) is a formula; (3) If α, β is formula, (α → → β) is formula; 4) All formulas are limited only (1) - (3) obtained. P'm The axioms of the Africa: (1) α → (β → α) (A1) (2) (α → β) → (α α → r)) (A2) ( 3) ((┐β) → (┐α)) → (α → → →) (3 β) (α β) (A3) P forms: Isolation rules: α → β, α┣β (m) This system will compete for the logic of life . However, I have emphasized you such a concept, formula in the form system, just satisfying a certain number of symbol strings, "Form reasoning" is a symbol string conversion before giving them semantics. For example, for rules (M): α → β, α┣β you don't want to come in your heart: If α is true, α → β is true, then β is true! This is the transformation rule of the symbol string, there is no real concept. You may wish to see this, such as a string (formula:) α, can be introduced to β → α:
(1) α → (β → α) (A1) (2) α (3) β → α (m) (1) (2) such a sequence, that is, in the form of reasoning.
Of course, as a technician, I think I don't see its semantic part, everyone will not be assured, this form system P, what is it? But if it is disclosed, this article has become a presented manager logic. In this way, interested readers can refer to Note 1.
Let's take a look at the example of the reasoning process of human beings:
Proof proves in the deductive inference form system P: ┣ (α → β) → (α → α)
This is an interesting logical thinking exercise, which is derived from the axiom set and rule set; I think you can think of this sequence: (1) α → (β → α) (A1) (2) (α → (β → α)) → ((α → β) → (α)) (A2) (3) (α → β) → (α → α) (m) (1) (2) in fact, we The idea can be like this: from (α → β) → (α → → α), the characteristics of three types of axioms are seen, you don't think it is bright: Formula (α → β) → (α → α) Can correspond to the right end of (A2), let al alpha replace R; there is no doubt by rule (m), we hope α → (β → α) is established, and this is (A1)! We can write this proof sequence. For complex problems, this "looks in front", which is not a relaxed work for humans. What's more, we hope that our computer can also "bright in front of you"! The machine proves is difficult, but it is still not perfect. I hope you are not bored by theoretical science. Next time we will launch the mystery of the machine certificate.
Note 1: Good Mathematical Logic Textbook, I read, there is
[Lu Zhong Wan]. Mathematical Logic for Computer Science. Science Press, 1998
[王 捍 贫]. Mathematical Logic. Peking University Press, 1997
This article reference materials:
[Lu Zhong Wan]. Mathematical Logic and Machine Proof. Scientific Press, 1983 [Wang Xi ". Matal Logic. Peking University Press, 1997
