How does the resolution algorithm work for sentence logic?

Question

I could not understand what is the rule of permission in the logic of statements. Does permission just allow the rules by which a sentence can be expanded and written in another form?
Below is a simple algorithm for resolving propositional logic. The function returns a set of all possible sentences obtained by resolving this 2 entries. I can not understand the operation of the algorithm, can someone explain this to me?

function PL-RESOLUTION(KB,α) returns true or false inputs: KB, the knowledge base, a sentence α in propositional logic, the query, a sentence in propositional logic clauses <--- the set of clauses in the CNF representation of KB ∧ ¬α new <--- {} loop do for each Ci, Cj in clauses do resolvents <----- PL-RESOLVE(Ci, Cj) if resolvents contains the empty clause then return true new <--- new ∪ resolvents if new ⊆ clauses then return false clauses <---- clauses ∪ new 

Answer 1

This is a whole topic of discussion, but I will try to explain one simple example to you.

Entering your KB algorithm is a set of rules for resolving. It is easy to understand that in the form of many facts such as:

• Apple red
• If smth is red then this smth is sweet

We introduce two predicates R(x) - ( x red), and S(x) - ( x sweet). How can we write our facts in the official language:

• R('apple')
• R(X) -> S(X)

We can replace the 2nd fact as ¬R v S to be eligible for the permission rule.

The calculating step of the resolvent in your programs removes two opposite facts:

Examples: 1) a & ¬a -> empty . 2) a('b') & ¬a(x) vs(x) -> S('b')

Note that in the second example, the variable x replaced with the actual value of 'b' .

The goal of our program is to determine if the offer is really sweet . We also write this sentence in the official language as S('apple') and set it in an inverted state. Then the formal definition of the problem:

• CLAUSE1 = R('apple')
• CLAUSE2 = ¬R(X) v S(X)
• Purpose? = ¬S('apple')

The algorithm works as follows:

• Take item c1 and c2
• calculate resolvents for c1 and c2 gives a new sentence c3 = S('apple')
• calculates the resolvents for c3, and the goal gives us an empty set.

This means that our proposal is true. If you cannot get an empty set with such permissions, which means that the sentence is false (but for most cases in practical applications this is the absence of KB facts).

Answer 2

Consider the sentences X and Y, where X = {a, x1, x2, ..., xm} and Y = {~ a, y1, y2, ..., yn}, where a is a variable, ~ a is its negation , and xi and yi are literals (i.e., possibly negative variables).

Interpretation of X is a sentence (a \ / x1 \ / x2 \ / ... \ / xm) - that is, at least one of a or one of xi must be true if we assume that X is true, Similarly for Y.

Suppose that X and Y are true.

We also know that (a \ / ~ a) is always true, regardless of the value of a.

If ~ a is true, then a is false, therefore ~ ​​a / \ X => {x1, x2, ..., xm}.

If a is true, then ~ a is false. In this case, a / \ Y => {y1, y2, ..., yn}.

Therefore, we know that {x1, x2, ..., xm, y1, y2, ..., yn} must be true, assuming that X and Y are true. Note that the new sentence does not apply to variable a.

This type of deduction is known as permission.

How does this work in the proof of a resolution-based theorem? Simple: we use evidence from the contrary. That is, we start by turning our "facts" into reservations and add suggestions corresponding to the denial of our "goal." Then, if we can eventually resolve the empty sentence {}, we will reach a contradiction, since an empty sentence is equivalent to false. Since the data is given, this means that our negative goal must be wrong, therefore, the goal (unnecessarily) must be true.

Answer 3

resolution is a procedure used to prove that an argument expressed in predicate logic is correct
resolution leads to a method of proving the refutation theorem for sentences in propositional logic.
permission provides evidence by rebuttal . those. in order to show that it is valid, permission tries to show that the negation of the operator contradicts the well-known statement
Algorithm:
one). convert all axiom offers into a proposal form
2). deny offers and convert the result to a proposal form
3) allow them
4) if the resolvent is an empty sentence, then a contradiction is found