Resolution (logic)

The resolution is a method of formal logic , a logical formula to test for validity.

The resolution procedure, also called resolution calculus , is a refutation procedure : Instead of directly showing the general validity of a formula, it derives a logical contradiction from its negation.

This derivation takes place by means of an algorithm in a purely formal way and can therefore be carried out by a computer program. Resolution is one of the most well-known machine-aided proofing techniques .

The resolution method in propositional logic

Resolvent (also: resolvent)

Be , clauses of a propositional formula that is in conjunctive normal form. If there is a literal that occurs in positive and negative, the union of both clauses without the positive and negative literal is a resolvent (also: the resolvent) . In particular, this means: If there is no complementary literal, there are also no resolvents. ${\displaystyle C_{1}}$ ${\displaystyle C_{2}}$ ${\displaystyle L}$ ${\displaystyle C_{1}}$ ${\displaystyle C_{2}}$ ${\displaystyle L}$ ${\displaystyle C_{R}}$

${\displaystyle L\in C_{1}}$

${\displaystyle {\overline {L}}\in C_{2}}$

${\displaystyle C_{R}=(C_{1}\setminus \{L\})\cup (C_{2}\setminus \{{\overline {L}}\})}$

Only one literal can be resolved at a time. Depending on the initial clauses, the formation of different resolvents is possible.

Notated differently: Off

${\displaystyle (A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})}$

will be on the resolvent

${\displaystyle A_{2}\vee \dots \vee A_{n}\vee B_{1}\vee \dots \vee B_{m}}$

closed.

The resolvent is not equivalent to the exit clauses. Rather, the significance of the resolvent lies in the fact that the exit clauses can only both be fulfilled at the same time if the resolvent can also be fulfilled ( necessary condition ). If we succeed in resolving the empty clause, which is always unsatisfiable, the unsatisfiability of the entire formula is shown.

proof

Since the resolvent is a necessary condition for the exit clauses and , applies ${\displaystyle C_{R}}$ ${\displaystyle C_{1}}$ ${\displaystyle C_{2}}$

${\displaystyle (C_{1}\wedge C_{2})\rightarrow C_{R}}$.

One says follows from and . From this follows the proof of the correctness of the resolution: ${\displaystyle C_{R}}$ ${\displaystyle C_{1}}$ ${\displaystyle C_{2}}$

${\displaystyle {\begin{aligned}&[(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\rightarrow (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&\equiv \neg [(A_{1}\vee A_{2}\vee \dots \vee A_{n})\wedge (B_{1}\vee B_{2}\vee \dots \vee B_{m}\vee \neg A_{1})]\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&\equiv (\neg A_{1}\wedge \neg A_{2}\wedge \dots \wedge \neg A_{n})\vee (\neg B_{1}\wedge \neg B_{2}\wedge \dots \wedge \neg B_{m}\wedge A_{1})\vee (A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&\equiv (\neg A_{1}\vee A_{2}\vee A_{3}\vee \dots \vee A_{n})\vee (A_{1}\vee B_{1}\vee B_{2}\vee \dots \vee B_{m})\\&\equiv \neg A_{1}\vee A_{1}\\&\equiv 1\end{aligned}}}$

Res operator

The execution of a single resolution step is noted with the res operator:

${\displaystyle \operatorname {Res} (F)=F\cup \{R\}}$, where a resolvent of two clauses is off ${\displaystyle R}$ ${\displaystyle F}$

With one denotes the union of all possible resolution steps . ${\displaystyle \operatorname {Res} ^{\star }(F)=\bigcup _{n\in \mathbb {N} }\operatorname {Res} ^{n}(F)}$ ${\displaystyle F}$

Thus the following statements are possible:

1. is the empty clause element of , is unsatisfiable and ${\displaystyle \operatorname {Res} ^{\star }(F)}$ ${\displaystyle F}$
2. is the empty clause element of , is a tautology ${\displaystyle \operatorname {Res} ^{\star }(\neg F)}$ ${\displaystyle F}$

Resolution and predicate logic

Problem

Propositional logic is not sufficient for more interesting problems. It should be possible to extend the principle of resolution from simple propositional logic to first-level predicate logic . In addition to logical literals, the following must be taken into account:

• Variables (such as number variables), usuallylabeledwith symbols likeand ${\displaystyle x}$ ${\displaystyle y}$
• the quantifiers ( the existential quantifier ) and ( the universal quantifier ), ${\displaystyle \exists }$ ${\displaystyle \forall }$
• Constants , for example ${\displaystyle 0,1,\pi \,}$
• single and multi-valued functions , usually denoted by symbols such as or . ${\displaystyle f(x)}$ ${\displaystyle g(x,y)}$

A typical example of a predicate logic statement is:

1)	${\displaystyle \forall x\exists y\forall zK(g(a,z),y)\implies K(g(f(a),f(z)),x)}$

(Note: If we set and , the above formula gives us the formal-logical definition of the continuity of the function in the point .) ${\displaystyle g(t,u)=\vert t-u\vert \,}$ ${\displaystyle K(v,w)\equiv (v<w)\,}$ ${\displaystyle f\,}$ ${\displaystyle a\,}$

So that the resolution can be applied to such statements, they must be transformed and the procedure described above expanded.

normalization

The first steps are to bring the statement to be refuted into a form that is similar to the conjunctive normal form of propositional logic.

1. The formula to be refuted is brought into prenex form . After this transformation, the quantifiers are all at the beginning of the formula, and the rest of the formula has the form of a conjunctive normal form.
2. By using Skolem functions one eliminates all existential quantifiers from the formula and brings them into Skolem form . ${\displaystyle \exists }$
3. Now all variables in the function are bound to universal quantifiers . If one agrees to denote constants and variables differently, for example constants with and variables with , then the explicit notation of the universal quantifier can be dispensed with. You also leave it out and get the clause form of the statement. ${\displaystyle \forall }$ ${\displaystyle a,b,c,a_{1},a_{2},a_{3},\dotsc \,}$ ${\displaystyle x,y,z,x_{1},x_{2},x_{3},\dotsc \,}$

For example, the clause form of formula 1) from the previous section is:

2)	${\displaystyle \neg K(g(a,z),s(x))\vee K(g(f(a),f(z)),x)}$

Substitution and standardization

The formulas

${\displaystyle P(x)\,}$

and

${\displaystyle \neg P(a)\,}$

do not seem to be resolvable at first glance, since they differ in and . Since the free variable but implicitly a proxy for all is, must (among other things) for be used. ${\displaystyle x\,}$ ${\displaystyle a\,}$ ${\displaystyle x\,}$ ${\displaystyle x\,}$ ${\displaystyle a\,}$ ${\displaystyle x\,}$

So you get the two terms

${\displaystyle P(a)\,}$

and

${\displaystyle \neg P(a)\,}$

which can obviously be resolved together.

The following replacements are possible:

3a)	Replace variable with constant:	${\displaystyle P(x)\,}$	${\displaystyle \rightarrow }$	${\displaystyle P(a)\,}$
3b)	Replace variable with another variable:	${\displaystyle P(x)\,}$	${\displaystyle \rightarrow }$	${\displaystyle P(y)\,}$
3c)	Replace variable with function of a variable:	${\displaystyle P(x)\,}$	${\displaystyle \rightarrow }$	${\displaystyle P(f(y))\,}$

The replacement of variables in a literal must be carried out consistently: If a variable is replaced by a term at one point, this must be done everywhere within the literal:

4a)	Correct replacement:	${\displaystyle P(x,f(x))\,}$	${\displaystyle \rightarrow }$	${\displaystyle P(a,f(a))\,}$
4b)	Prohibited substitution:	${\displaystyle P(x,f(x))\,}$	${\displaystyle \nrightarrow }$	${\displaystyle P(a,f(x))\,}$

Be a set of variables. Be a set of terms that can be composed of functions, variables or constants. ${\displaystyle \lbrace x_{1},x_{2},\dotsc ,x_{n}\rbrace \,}$ ${\displaystyle \lbrace t_{1},t_{2},\dotsc ,t_{n}\rbrace \,}$

• A system of substitutions is called a substitution . ${\displaystyle S\,}$ ${\displaystyle \lbrace x_{1}\rightarrow t_{1},x_{2}\rightarrow t_{2},\dotsc ,x_{n}\rightarrow t_{n}\rbrace \,}$

Let literals be over the same predicate , which in turn are terms. ${\displaystyle L_{1}=P(t_{1},t_{2},\dotsc ,t_{n}),L_{2}=P(u_{1},u_{2},\dotsc ,u_{n}),\dotsc ,L_{m}=P(v_{1},v_{2},\dotsc ,v_{n})\,}$ ${\displaystyle P\,}$ ${\displaystyle t_{i},u_{i},\dotsc ,v_{i}\,}$

• A substitution is called a unification (or also unifier) ​​of when the arguments of all literals are brought into agreement by using, that is, when . ${\displaystyle S\,}$ ${\displaystyle L_{1},L_{2},\dotsc ,L_{m}\,}$ ${\displaystyle S\,}$ ${\displaystyle S(L_{1})=S(L_{2})=\dotsb =S(L_{m})\,}$

Two literals over the same predicate do not necessarily have a unification. For example, and cannot be unified if and are different constants. ${\displaystyle P(a)\,}$ ${\displaystyle P(b)\,}$ ${\displaystyle a\,}$ ${\displaystyle b\,}$

• A standardization of literals is called the most general standardization if there is a substitution for every other standardization of these literals , so that . ${\displaystyle S\,}$ ${\displaystyle T\,}$ ${\displaystyle V\,}$ ${\displaystyle T=S\circ V\,}$

If a set of literals has a unification, then it has a most general unification. This can be determined using a relatively simple algorithm.

Resolution of predicate clauses

With this set of instruments the resolution procedure can be extended to statements of the predicate logic.

• Let be two clauses of a normalized predicate statement. Without loss of generality, it can be assumed that these do not contain any matching variables (since they are bound by a universal quantifier, we can rename variables with the same name in a clause, even if the universal quantifier is no longer explicitly written). ${\displaystyle C_{1},C_{2}\,}$
• Be and positive or negated literals occurring in or , which have the most general unification . ${\displaystyle L_{1}\,}$ ${\displaystyle L_{2}\,}$ ${\displaystyle C_{1}\,}$ ${\displaystyle C_{2}\,}$ ${\displaystyle S\,}$

Then is called

• ${\displaystyle C_{R}=S(C_{1}\cup C_{2})\setminus \{S(L_{1}),\neg S(L_{2})\}}$a binary resolvent of and . ${\displaystyle C_{1}\,}$ ${\displaystyle C_{2}\,}$
• Furthermore, let be a clause with a subset of literals that has the most general unification . ${\displaystyle C\,}$ ${\displaystyle S\,}$

Then is called

• ${\displaystyle S(C)\,}$a factor of . ${\displaystyle C\,}$

Is a resolvent of two clauses ${\displaystyle C_{1},C_{2}\,}$

• either a binary resolvent of and . ${\displaystyle C_{1}\,}$ ${\displaystyle C_{2}\,}$
• or a binary resolvent of and a factor of . ${\displaystyle C_{1}\,}$ ${\displaystyle C_{2}\,}$
• or a binary resolvent of a factor of and . ${\displaystyle C_{1}\,}$ ${\displaystyle C_{2}\,}$
• or a binary resolvent of a factor of and a factor of . ${\displaystyle C_{1}\,}$ ${\displaystyle C_{2}\,}$

The resolution procedure for statements based on predicate logic consists in generating such resolvents until the empty clause is generated and thus the contradiction proof is provided.

example

A logical puzzle

We want to illustrate the principle with the example of a small, not to be taken literally logical puzzle:

It has been known since ancient times that all Athenians are clever (1) and all Spartans are heroic (2). It is also known that there is a profound mistrust between the two cities, so that dual city citizenship is ruled out (3). Our researcher, who was sent to Greece, recently attended a conference. With the exception of our researcher, everyone present came from one of the two cities (4).

The researcher got into conversation with Messrs Diogenes, Plato and Euclid. The only thing they had in common with their famous role models was their name. The gentlemen pulled the leather vigorously over each other. Euclid said: “If Plato is a Spartan, then Diogenes is a coward!” (5) - Plato claimed: “Diogenes is a coward if Euclid is a Spartan!” (6) “If Diogenes is an Athenian, then Euclid is a washcloth! "(7) - Whereupon Diogenes smoothed his beard and postulated:" If Plato is an Athenian, then Euclid is a fool! "(8)

In spite of all their nimbleness, the three gentlemen remained true to their claims. Who is from which city?

The puzzle in clause form

We put p for Plato, d for Diogenes, e for Euclid. We denote the predicates "is Athenian", "is Spartan", "is heroic" and "is clever" with A, S, H and K. We translate the above statements into the clause form and get:

¬A (x) v K (x)		(1)
¬S (x) v H (x)		(2)
¬A (x) v ¬S (x)		(3)
A (x) v S (x)		(4)
¬S (p) v ¬H (d)		(5)
¬S (e) v ¬H (d)		(6)
¬A (d) v ¬H (e)		(7)
¬A (p) v ¬K (e)		(8th)

The resolution

We assume that Plato is an Athenian:

A (p)	{Adoption}	(9)

Now we apply the principle of resolution and get:

¬K (e)	{from resolution of (9) with (8)}	(10)
¬A (e)	{from substitution of e for x and resolution (10,1)}	(11)
S (e)	{Subs. (e: x), res. (11,4)}	(12)
¬H (d)	{Res. (12.6)}	(13)
¬S (d)	{Subs. (d: x), res. (13,2)}	(14)
A (d)	{Subs. (d: x), res. (14,4)}	(15)
¬H (e)	{Res. (15.7)}	(16)
¬S (e)	{Subs. (e: x), res. (16,2)}	(17)
empty clause	{Res. (17.12)}	(18)

Thus, assumption (9) is contradicted. It is to be rejected together with the clauses (10) to (18) derived from it. Instead we get:

¬A (p)	{since (9) is false}	(19)
S (p)	{Subs. (p: x), res. (19.4)}	(20)

Let us now assume that Diogenes is a Spartan and let us continue to apply the principle of resolution:

S (d)	{Adoption}	(21)
H (d)	{Subs. (d: x), res. (21,2)}	(22)
¬S (p)	{Res. (22.5)}	(23)
empty clause	{Res. (23.20)}	(24)

Assumption (21) is thus refuted and together with the clauses (22) - (24) derived from it must be rejected. Instead we get:

¬S (d)	{since (21) is false}	(25)
A (d)	{Subs. (d: x), res. (25,4)}	(26)

Let us assume that Euclid is a Spartan. We obtain:

S (e)	{Adoption}	(27)
H (e)	{Subs. (e: x), Res. (27, 2)}	(28)
¬A (d)	{Res. (28, 7)}	(29)
empty clause	{Res. (29.26)}	(30)

So (27) is false and all (28) - (30) must be rejected. Instead we get:

¬S (e)	{since (27) is false}	(31)
A (e)	{Subs. (e: x), Res. (31,4)}	(32)

Plato is a Spartan (20). Diogenes is an Athenian (26), as is Euclid (32).

Scheduling and Complexity

In the case of propositional logic, the procedure terminates : It provides a result in a finite time as to whether a given statement can be fulfilled. The computation time increases in the general case and with the currently known methods exponentially with the number of literals. The problem is NP-complete .

In the case of predicate logic, the method always terminates with the correct result if it is applied to an unsatisfiable formula. In the case of a formula that can be fulfilled, however, the process never ends. One speaks of semi-decidability . If it were different, then the resolution method would be an algorithm to decide predicate logic formulas in general - which is impossible, since the validity problem in the predicate logic cannot be decided .

Other calculations in logical use

• Tree calculus : in a certain way the closest relative of the calculus of resolution among the calculi
• axiomatic calculi
• Systems of natural reasoning
• Sequence calculus
• Existential graphs

swell

1. ^ Davis, Martin: Eliminating the Irrelevant from Mechanical Proofs. in: Journal of Symbolic Logic , ISSN  0022-4812 , Vol. 32, No. 1 (Mar., 1967), pp. 118-119
2. ↑ Chang, Chin-Liang; Lee, Richard Char-Tung: Symbolic Logic and Mechanical Theorem Proving , Academic Press, 1973, ISBN 0-12-170350-9 , pp. 77ff
3. ↑ Chang, Chin-Liang; Lee, Richard Char-Tung: S ymbolic Logic and Mechanical Theorem Proving , Academic Press, 1973, ISBN 0-12-170350-9 , pp. 80-81
4. ↑ Haken, A. "The Intractability of Resolution", Theoretical Computer Science 39 (1985), pp. 297-308.

literature

• Chang, Chin-Liang; Lee, Richard Char-Tung: Symbolic Logic and Mechanical Theorem Proving , Academic Press, 1973, ISBN 0-12-170350-9

Web links

• Lecture script by Habel and Eschenbach , 2009, Department of Computer Science, University of Hamburg, with clear graphic representations (PDF file; 410 kB)
• Lecture notes by Bernhard Beckert , 2006, University of Koblenz-Landau (PDF file; 197 kB)
• Logic for Computer Scientists , by Ulrich Furbach , University of Koblenz-Landau