CSharp  Java  Python  Swift  GO  WPF  Ruby  Scala  F#  JavaScript  SQL  PHP  Angular  HTML
Resolution in FOLResolutionResolution is a theorem proving technique that proceeds by building refutation proofs, i.e., proofs by contradictions. It was invented by a Mathematician John Alan Robinson in the year 1965. Resolution is used, if there are various statements are given, and we need to prove a conclusion of those statements. Unification is a key concept in proofs by resolutions. Resolution is a single inference rule which can efficiently operate on the conjunctive normal form or clausal form. Clause: Disjunction of literals (an atomic sentence) is called a clause. It is also known as a unit clause. Conjunctive Normal Form: A sentence represented as a conjunction of clauses is said to be conjunctive normal form or CNF. Note: To better understand this topic, firstly learns the FOL in AI.The resolution inference rule:The resolution rule for firstorder logic is simply a lifted version of the propositional rule. Resolution can resolve two clauses if they contain complementary literals, which are assumed to be standardized apart so that they share no variables. Where l_{i} and m_{j} are complementary literals. This rule is also called the binary resolution rule because it only resolves exactly two literals. Example:We can resolve two clauses which are given below: [Animal (g(x) V Loves (f(x), x)] and [￢ Loves(a, b) V ￢Kills(a, b)] Where two complimentary literals are: Loves (f(x), x) and ￢ Loves (a, b) These literals can be unified with unifier θ= [a/f(x), and b/x] , and it will generate a resolvent clause: [Animal (g(x) V ￢ Kills(f(x), x)]. Steps for Resolution:
To better understand all the above steps, we will take an example in which we will apply resolution. Example:
Step1: Conversion of Facts into FOL In the first step we will convert all the given statements into its first order logic. Step2: Conversion of FOL into CNF In First order logic resolution, it is required to convert the FOL into CNF as CNF form makes easier for resolution proofs.
Note: Statements "food(Apple) Λ food(vegetables)" and "eats (Anil, Peanuts) Λ alive(Anil)" can be written in two separate statements.
Step3: Negate the statement to be proved In this statement, we will apply negation to the conclusion statements, which will be written as ¬likes(John, Peanuts) Step4: Draw Resolution graph: Now in this step, we will solve the problem by resolution tree using substitution. For the above problem, it will be given as follows: Hence the negation of the conclusion has been proved as a complete contradiction with the given set of statements. Explanation of Resolution graph:
