A3 – [II.3518] Formal Approaches Project Olivier Hermant and Matthieu Manceny The goal is to implement a proof-search algorithm in propositional logic and to run it on small examples. The algorithm is quite different from natural deduction or sequent calculus, and it is called resolution. It has been introduced by Alan Robinson in 1965 [3] and has been extended in many ways. Nowadays most powerful first-order theorem pro- vers are still based on resolution and refinments (such as superposition), see for example E [4] or Vampire [2]. Note that the resolution method is a proof-search in classical logic, or boolean logic that is to say, a logic where we accept the excluded-middle law : A∨¬A is valid/provable. 1 Description of the method 1.1 Clauses Resolution works on fomulæ that have the following form : A1 ∨ · · · ∨An ∨ ¬B1 ∨ · · · ∨ ¬Bm where : — A1, · · · , An and B1, · · · , Bm are atomic formulæ — n, as well as m are potentially equal to 0 This form is called a clausal form, or a disjunctive normal form. A formula in clausal form is called a clause. In the case where n = 0 and m = 0, the clause is called the empty clause, or absurd clause, and it is sometimes denoted by . Here are six examples of clauses : A ¬A A ∨ ¬B A ∨ ¬A A ∨B ∨ C ∨ ¬B B ∨B ∨ ¬C The informal meaning of a clause A1 ∨ · · · ∨An ∨ ¬B1 ∨ · · · ∨ ¬Bm is : At least one of A1, · · · , An,¬B1, · · · ,¬Bm is true or, said otherwise : At least one of A1, · · · , An is true, or at least one of B1, · · · , Bm is false 1.2 Transforming a formula into a set of clause It is known that any formula F (even a first-order formula with quantifiers) can be trans- formed into an equivalent set of clauses, which have to be though as a conjunctive normal form of F in propositional logic. See for instance http://en.wikipedia.org/wiki/Conjunctive_normal_form Here is an example of transformation in clausal form of various formulæ of propositio- nal logic : 1 A ∧B ↪→ {A,B} (two clauses) ((A ∧ ¬A) ∨B) ↪→ {A ∨B,B ∨ ¬A} (two clauses) ((A ∧ ¬A) ∨B) ∧ ¬B ↪→ {A ∨B,B ∨ ¬A,¬B} (three clauses) A ∨ ¬C ↪→ {A ∨ ¬C} (one clause) 1.3 Resolution The resolution method is a refutation method : it tries to derive a contradiction starting from a set of clauses as hypothesis. In this regard, it is a forward proof-search method. The resolution rule is shown in Figure 1. A ∨A1 ∨ · · · ∨An ∨ ¬B1 ∨ · · · ¬Bm C1 ∨ · · · ∨ Cp ∨ ¬D1 ∨ · · · ¬Dl ∨ ¬A A1 ∨ · · · ∨An ∨ C1 ∨ · · · ∨ Cp ∨ ¬B1 ∨ · · · ¬Bm ∨ ¬D1 ∨ · · · ¬Dl FIGURE 1 – The resolution rule This rule has to be understood top-down : — we start with the two premises A ∨ A1 ∨ · · · ∨ An ∨ ¬B1 ∨ · · · ¬Bm and C1 ∨ · · · ∨ Cp ∨ ¬D1 ∨ · · · ¬Dl ∨ ¬A. — we eliminate the occurrence of A in the first clause and ¬A in the second clause, and we conclude with a new clause, A1∨ · · ·∨An∨C1∨ · · ·∨Cp∨¬B1∨ · · · ¬Bm∨ ¬D1 ∨ · · · ¬Dl — note that some n,m, p, l can be equal to 0. As we can see, we have formed the new clause by eliminating the inconsistent atomic formula A, that cannot be, at the same time true in the first clause and false in the second clause. So, one of the remaining atomic fromula must make the clause true. We start with a given set of clauses, that are supposed to be all true at the same time, and generate new clauses with the resolution rule. In this way, we try to see which assignment of truth value to atoms must be made. This is, in essence, a similar problem that the very-well known SAT problem [1]. If we generate to the empty clause, this means that we have found an inconsistency : all the clauses cannot be true at the same time, they are inconsistent. This is called a proof (by contradiction). Here is an example of proof, starting from the set of clauses {A ∨B,B ∨ ¬A,¬B} : A ∨B B ∨ ¬A ¬B ¬A B ¬B We see that we have generated the empty clause , by using twice the clause ¬B and once the two clauses A ∨ B and B ∨ ¬A. This proof is as well a proof of the contra- diction of the formula ((A ∧ ¬A) ∨B) ∧ ¬B. To prove a formula F we must then : negate it (¬F ), transform ¬F into its clausal form and then run the resolution method until we generate the empty clause, in which case the proof is done. 1.4 Improvements : simplification of a clause The sole resolution rule, as expressed in Figure 1, is not complete. Let us consider the set of clauses {A ∨ A,¬A ∨ ¬A}, that is trivially inconsistent. By applying the resolution rule, we can generate the clause A ∨ ¬A. But once we have the new set of clause {A ∨ 2 A ∨A ∨A1 ∨ · · · ∨An ∨ ¬B1 ∨ · · · ∨ ¬Bm Simpl1A ∨A1 ∨ · · · ∨An ∨ ¬B1 ∨ · · · ∨ ¬Bm A1 ∨ · · · ∨An ∨ ¬B1 ∨ · · · ∨ ¬Bm ∨ ¬B ∨ ¬B Simpl2A1 ∨ · · · ∨An ∨ ¬B1 ∨ · · · ∨ ¬Bm ∨ ¬B FIGURE 2 – The two simplification rules A,¬A∨¬A,A∨¬A}, we are stuck, since we can generate only already known clauses 1. To break this circle, we must use the simplification rules, shown in Figure 1.4 : The simplification rules just amount to simplify redundant atomic formulæ in clauses, those that appear more than once. Equiped with those two additional rule, we can now construct the following proof : A ∨Asimpl A ¬A ∨ ¬Asimpl ¬Aresolution 2 Exercises Prove “by hand” that the following set of clauses is unsatisfiable : — {A,¬A} — {¬A,¬B,A ∨B} — {¬A ∨ ¬B,A,B ∨ ¬C,C} — {C ∨ ¬A ∨ ¬B,B ∨ ¬A,A,¬C} — {A ∨A ∨B,¬A ∨ ¬A,¬B ∨ ¬B,C ∨ ¬C} This is also part of the project. 3 The Project 3.1 Work expected The goal of this project is to implement a resolution kernel in the language of your choice, and to prove automatically the exercises of Section 2. You must implement the three rules : resolution and the two simplification rules, and finally, a complete strategy to systematically search for a proof, that will succeed if the current set of clauses is unsatisfiable. 3.2 Structure For this, we will use the following structures : — atomic formulæ are represented by strings. — a clause C is represented by two lists : one list for the non-negated atomic formulæ of the clause C (the positive atoms) and another list for the negated atomic formulæ of the clause C (the negative axioms). For instance, the clause {A,¬B} will be represented by the pair of lists (["A"],["B"]) while the clause ¬C will be represented by the pair of lists ([],["C"]) 1. From A ∨ A,¬A ∨ ¬A we generate A ∨ ¬A. From A ∨ A,A ∨ ¬A we generate A ∨ A. And from A ∨ ¬A,¬A ∨ ¬A we generate ¬A ∨ ¬A. 3 Here [] stands for the empty list. So the empty clause will be represented by athe follo- wing pair of lists ([],[]) 3.3 Testing your work First, you shall test your program on the exercises of Section 2. Then, check that your program is correct, by verifying that your program is not able to find a proof for consistent sets of clauses, among which : — {A ∨ ¬A} — {A ∨ ¬A,A} — {A ∨ ¬A,¬A} — {A,¬B} — {A ∨B,A ∨ ¬B} — {C ∨ ¬A ∨ ¬B,C ∨ ¬A,A,B} — {C ∨ ¬A ∨ ¬B,C ∨ ¬A,A,¬B} Your program may loop forever if there is no proof, this is not a problem, and even may be a desired behavior 2. 3.4 Optional work As an optional work, you can implement the algorithms that takes a formula in pro- positional logic (so, without quantifiers) and constructs is clausal form. Then, you can for instance use your program to prove any of the formulæ of propositional logic that we have seen during the lectures 3. For instance : — {(A⇒ (B ⇒ C))⇒ ((A⇒ B)⇒ A)} ⇒ C — A ∨ ¬A — A⇒ B ⇒ A ∧B — A⇒ A ∨B — (A ∨B)⇒ ((A⇒ C)⇒ ((B ⇒ C)⇒ C)) — and so on ... Keep in mind, please, that you must negate your theorem before proving it (so for instance, instead of proving A ∨ ¬A, we must prove that ¬(A ∨ ¬A) is inconsistent). You can also develop an interactive proof mode, with a parser for formulæ for instance. Références [1] S. A. Cook. The complexity of theorem-proving procedures. In M. A. Harrison, R. B. Banerji, and J. D. Ullman, editors, STOC, pages 151–158. ACM, 1971. [2] L. Kovács and A. Voronkov. First-order theorem proving and vampire. In N. Sharygina and H. Veith, editors, CAV, volume 8044 of Lecture Notes in Computer Science, pages 1–35. Springer, 2013. [3] J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1) :23–41, 1965. [4] S. Schulz. System Description : E 1.8. In K. McMillan, A. Middeldorp, and A. Voronkov, editors, Proc. of the 19th LPAR, Stellenbosch, volume 8312 of LNCS, pages 735–743. Springer, 2013. 2. especially in first-order logic, that is only semi-decidable 3. after having negated them, of course 4
欢迎咨询51作业君