Formal methods project

Introduction : The goal is to implement a proof-search algorithm in propositional logic and to run it on small examples, The algorithm used is called Resolution. It has been introduced by Alan Robinson in 1965. Note that the resolution method is a proof-search in classical logic, or boolean logic that is to say, a logic where we accept the excluded-middle law : A ∨ ¬A is valid/provable. 1. — {A, ¬A} — {¬A, ¬B, A ∨ B} — {¬A ∨ ¬B, A, B ∨ ¬C, C} — {C ∨ ¬A ∨ ¬B, B ∨ ¬A, A, ¬C} — {A ∨ A ∨ B, ¬A ∨ ¬A, ¬B ∨ ¬B, C ∨ ¬C} 2.1 Project expected The goal of this project is to implement a resolution kernel in the language of your choice, and to prove automatically the exercises above. You must implement the three rules : resolution and the two simplification rules, and finally, a complete strategy to systematically search for a proof, that will succeed if the current set of clauses is unsatisfiable. 2.2 Structure For this, we will use the following structures : — atomic formulæ are represented by strings. — a clause C is represented by two lists : one list for the non-negated atomic formulæ of the clause C (the positive atoms) and another list for the negated atomic formulæ of the clause C (the negative axioms). For instance, the clause {A, ¬B} will be represented by the pair of lists (["A"],["B"]) while the clause ¬C will be represented by the pair of lists ([],["C"]) Here [] stands for the empty list. So the empty clause will be represented by athe following pair of lists ([],[]) 2.3 Testing the work Check that your program is correct, by verifying that your program is not able to find a proof for consistent sets of clauses, among which : — {A ∨ ¬A} — {A ∨ ¬A, A} — {A ∨ ¬A, ¬A} — {A, ¬B} — {A ∨ B, A ∨ ¬B} — {C ∨ ¬A ∨ ¬B, C ∨ ¬A, A, B} — {C ∨ ¬A ∨ ¬B, C ∨ ¬A, A, ¬B} Your program may loop forever if there is no proof, this is not a problem, and even may be a desired behavior.