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作业君