Resolution Implementation For First Order Logic

Problem Description

We want to implement resolution inference for a given first order logic knowledge base. Following are the input forms and rules:

Format for Input.txt:

1
2
3
4
5
6
7
8
9
<NQ = NUMBER OF QUERIES>
<QUERY 1>
...
<QUERY NQ>
<NS = NUMBER OF GIVEN SENTENCES IN THE KNOWLEDGE BASE>
<SENTENCE 1>
...
<SENTENCE NS>
  • Each query will be a single literal of the form Predicate(Constant) or ~Predicate(Constant).
  • Variables are all single lowercase letters.
  • All predicates (such as Sibling) and constants (such as John) are case-sensitive alphabetical strings that begin with an uppercase letter.
  • Each predicate takes at least one argument. Predicates will take at most 100 arguments. A given predicate name will not appear with different number of arguments.
  • There will be at most 100 queries and 1000 sentences in the knowledge base.
  • You can assume that the input format is exactly as it is described. There will be no syntax errors in the given input.

e.g.

input.txt(example):

1
2
3
4
5
6
7
8
9
10
2
Ancestor(Liz,Billy)
Ancestor(Liz,Bob)
6
Mother(Liz,Charley)
Father(Charley,Billy)
~Mother(x,y) | Parent(x,y)
~Father(x,y) | Parent(x,y)
~Parent(x,y) | Ancestor(x,y)
~(Parent(x,y) & Ancestor(y,z)) | Ancestor(x,z)

output.txt:

1
2
TRUE
FALSE

In a word

You need to use the given sentences and resolution reference to determine whether the query can be derived.

Intuition

If we want to prove a query is TRUE we need to get the contradiction after negating the query and adding it into KB. But how to get contradiction?

  • We can find that in binary resolution the only way to get a contradiction(a empty clause after resolvent) is to resolve two clauses that both have only one predicate(these clause we call them unit clause). But there is a prerequest: all the clauses that cannot be simplified any more are all included in KB, that is, A(x,y)| A(x,y) | A(z, m) ‘s simplified clause—A(x,y)—should also be included in KB. Otherwise, it will be incomplete cause we only focus on unit clause to derive the contradiction(empty clause).
  • But how can we guarantee the prerequest? Factoring! Factoring in fact is to reduce the redundant predicate by applying unification on original clause. If you want to get all the derivation(subsititution) for original clause, you may need a recursive way. After factoring, you can add them all into KBs and in this way to guarantee all the most simplified clauses are included in KB.
  • Another thing we need to pay attention to is that in binary resolution if we want to reduce the number of predicates in a clause, the only way is to resolve the clause with one unit clause. Why? length(clause1) + length(clause2) - 2 < length(clause1) ===> length(clause2) < 2
  • Why we should only focus on unit clause but not any other general clause? Because we finally want to get the contradiction result which can only be derived by applying “dimension” deduction and unit clause resolvent. If a general clause can be resolved by a general clause and a unit clause at the same time, why not unit clause first? It will be more efficient and no waste on unnecessay reference.

Generally speaking, we have two targets here:

  • Use two unit clauses to derive a contradiction then return TRUE meaning that we can get such a query based on given KB
  • Use one unit clauses to reduce the “dimension” of a non-unit clause to derive new clause.

Follow-up Thoughts

How can this method make a FALSE conclusion?

Good questions! The answer is:

  • We try every unit clause with all other clauses which can be resolved with it and no new derivation clause appears, then we return FALSE

What does “new derivation clause” mean and how to recognize “new”?

  • “new derivation clause” means the clause that hasn’t been included in KB before. e.g. A(x, y) is a new clause if current KB doesn’t contain any clause like A(z, w) or A(u, p).
  • How to judge? Just stirngfy the clause, that is, no matter what the variable is, just rename the variable based on its appearance order and judge two stringfy clause are the same or not. There may be a problem here. You may say the predicate order may be different and actually they are the same like A(x, y) | B(z, w) and B(z, w) | A(x, y). You are correct in general, but in this case your code is fixed which means that if your programs generates that clause before, then this time the clause generated will be the same order definitely.

How to avoid infinite loop

  • This method has its advantage at least so far it hasn’t fell to any infinite loop in 45 random testcases. Why? Since we are always doing the right thing—clause dimension deduction. It has two natural terminations where the dimension of a clause cannot go negative and where we cannot get any more new clause by applying resolvent on a unit clause and a general clause. It’s just something like the total size of a KB has a limited upperbound.

Implemetation(Python)

  1. Read files
  2. Use lex&Yacc to convert orignal clauses and queries into Conjunctive Normal Form(CNF) and save them in KB. P.s. each time you add a clause into KB you should also:
    1. Factoring the clause (for each factoring clause do following three things as well)
    2. Stardardize the clause
    3. Establish index(dict) for each predicate in the clause
    4. If the clause is a unit clause then record its index
  3. for each unit clause find any possible resolvent based on the index you established in step 2.3. Generate clause.
  4. For each newly generated clause. Check empty, If yes, return TRUE. Check duplication and tautology. If yes, then ignore and continue step 3. Otherwise add them into tmp_kb(temporary knowledge base to be added into original KB).
  5. if tmp_kb is empty, return False. Otherwise for each clause in tmp_kb do step 2.1-step 2.4 and add it into KB then repeat step 3-step 5