Resolution (logic)
The resolution is a method of formal logic to test a logical formula to be valid.
The resolution method, also called resolution calculus, is a Widerlegungsverfahren: Instead of directly to show the universality of a formula, it derives a logical contradiction from its negation.
This derivation is done by means of an algorithm on a purely formal way and can therefore be carried out by a computer program. The resolution is one of the most well-known techniques of machine -aided proving.
- 2.1 Problem
- 2.2 normalization
- 2.3 Substitution and Unification
- 2.4 Resolution predicate logic clauses
- 3.1 A logical riddle
- 3.2 The puzzles in clause form
- 3.3 The resolution
The resolution method in propositional logic
Resolvent (also: resolvent )
Be, clauses of a propositional formula, which is in conjunctive normal form. Is there a literal that occurs in positive and in negative, the union of the two clauses is without the positive and negative literal a resolvent (also: the resolvent ). This means in particular: If there is no complementary literal, so there is no resolvent ().
It may not always exactly one literal resolved upon. Depending on the initial formation of various clauses of the resolvent is possible.
Other notes: From
Is the resolvent
Closed.
The resolvent is not equivalent to the output clauses. The importance of the resolvent lies rather in the fact that the output clauses on both simultaneously satisfiable, if the resolvent is satisfiable ( necessary condition ). If it is possible to resolvieren the empty clause, which is always unsatisfiable, hence the impossibility of the entire formula is shown.
Evidence
Since the resolvent is a necessary condition for the output clauses and applies
It is said follows from and. It follows from the proof for the correctness of resolution:
Res - operator
Running a single resolution step is listed with the Res operator:
With refers to the union of all possible resolution steps.
Thus, the following conclusions are possible:
Resolution and predicate logic
Problem
For more interesting problems the tools of propositional logic is not sufficient. The principle of the resolution should be able to be extended from the simple propositional logic to first-order logic. In addition to logical literals are taken into account:
- Variables (eg, number of variables ), usually denoted by symbols such as and
- Quantifiers ( the existential ) and ( the universal quantifier ),
- Constants, such as
- Mono-and multivalent functions, usually with symbols or as indicated.
A quite typical example of a predicate logic statement is:
( Note: we set and so provides us with the above formula, the formal- logical definition of continuity of the function at the point. )
Thus, the resolution can be applied to such statements, they must be formed and the process described above are expanded.
Normalization
The first steps are to bring the irrefutable evidence in a form that is similar to the conjunctive normal form of propositional logic.
For example, is the clausal form of the formula 1) from the previous section:
Substitution and unification
The formulas
Not seem to be resolvierbar, because they differ in and on first glance. However, since the free variable is implicitly a representative of everyone, may ( among other things) be used for.
One thus gets the two terms
Which obviously can resolvieren together.
The following substitutions are possible:
The substitution of variables in a literal must be performed in a consistent manner: If a variable at one point replaced by a term, this must be achieved within the literal everywhere:
Be a lot of variables. Let be a set of terms that can be composed of functions, variables or constants.
- A system of substitutions is called a substitution.
Be literals over the same predicate, which in turn, are terms.
- A substitution means standardizing (or unifier ) of, when brought by the application of all the literals of the arguments match, that is, when.
Two literals over the same predicate are not necessarily a standardization. For example, let and not unify if and to the different constants.
- A unification of literals is called most general unification, if there is a substitution for any other unifying these literals so.
If a set of literals has a unification, then it has a most general unification. This can be determined with the aid of a relatively simple algorithm.
Resolution predicate logic clauses
By using this instrument, the resolution process can be extended to statements of predicate logic.
- Be two clauses of a normalized predicate logic statement. Without loss of generality may be assumed that they do not contain matching variables (since they are bound by a universal quantifier, we can rename variables of the same name in a clause, even if the universal quantifier is not explicitly written ).
- Let and be positive or negated literals occurring in or having a general unification.
Then say
- A binary resolvent of and.
- Further, let a clause with a subset of literals, which has a general unification.
Then say
- A factor of.
A resolvent of two clauses is
- Either a binary resolvent of and.
- Or a binary resolvent of a factor of and.
- Or a binary resolvent of a factor of and.
- Or a binary resolvent of a factor of and a factor of.
The resolution method for predicate logic statements is as long to produce such resolvents, until the empty clause is generated and thus provided the proof by contradiction.
Example
A logical riddle
We want to illustrate the principle using the example of a small, not to be taken literally logical puzzle:
Since ancient times it is known that all the Athenians wise (1 ), and all Spartans heroically ( 2). It is also known that a profound distrust between the two cities there, so city double citizenships are excluded (3). Our researchers posted to Greece was recently a guest at a conference. With the exception of our researcher, everyone in attendance came from one of two cities (4).
The researchers came to talk to the men Diogenes, Plato and Euclid. With their famous role models they had in common only the name. The men rose sharply above the other from the leather. Euclid said, "If Plato is Spartan, then Diogenes is a coward! " (5) - Plato claimed, " Diogenes is a coward if Euclid is Spartan! " (6) "If Diogenes, however, the Athenians, then Euclid is a sissy! "(7) - What Diogenes the beard smoothed and postulated: " If Plato Athens, then Euclid is a fool "(8)!
With all Spitzzüngigkeit the three men remained with their claims to the truth. Who comes from what city?
The puzzles in clause form
We set p for Plato, Diogenes d, e for Euclid. The predicates " is Athens ", " is Spartan ," " is heroically " and " wise ", we denote by A, S, H and K. We translate the above statements in the clause form and receive:
The resolution
We assume that Plato was Athens:
We now turn to the resolution principle and receive:
Thus, the assumption ( 9) leads to a contradiction. You should be discarded together with the clauses derived from it ( 10) to ( 18). We get instead:
Now suppose, Diogenes was Spartan, and we continue to apply the resolution principle:
Thus, the assumption ( 21) is refuted and, together with the clauses derived from it (22) - to reject (24). We get instead:
Suppose that Euclid was the Spartans. We obtain:
So (27) is false, and together with (28 ) - to reject (30). We get instead:
Plato 's Spartan (20). Diogenes is Athens (26 ), just as Euclid (32).
Termination and complexity
In the case of propositional logic terminates the process: It provides a result in finite time whether a submitted statement is satisfiable. The computing time increases in the general case, and with the methods currently known exponentially with the number of literals, because it is an NP -complete problem.
In the case of predicate logic, the process terminates, although always with the correct result if it a unsatisfiable formula is presented. In the general case, for a satisfiable formula, it happens, however, that the process never ends. With each resolution step, new clauses, but not the empty clause, which stands for the slides to show contradiction. So we speak of semi - decidability. If it were otherwise, then the resolution process would be an algorithm to predicate logic formulas generally to decide - which is impossible, since the validity problem in predicate logic is not decidable.
Other calculi in the logical use
- Tree calculus: in some ways among the calculi of the next of kin of the resolution calculus
- Axiomatic calculi
- Natural deduction systems
- Sequent calculus
- Existential Graphs