# 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.

Về Bên Thuê:
( 3 nhận xét ) Saint-maur, France

ID dự án: #17073831

## Được trao cho:

xiaomingming1985

Hi, I'm a C++ expert and have 7 years of experience. I'll provide you quality work according to your instructions. Please award me the project so that we can discuss it more. Thanks.

€95 EUR trong 3 ngày
(3 Đánh Giá)
2.6

## 8 freelancer đang chào giá trung bình €167 cho công việc này

liangjongai

Hi! I'm interesting your project very well. I am mastering c++ and I'm a good Mathematician. And also I have many experience and good skill about algorithm development. Let's go ahead with me

€150 EUR trong 3 ngày
(72 Nhận xét)
6.0
kcbStar

Hello, I am interested in this project and so wanted to discuss more it in details. I have a lot of experience in C C++ programming. I will provide you quality work according to your instrument. Thank you.

€155 EUR trong 3 ngày
(62 Nhận xét)
5.5
€155 EUR trong 3 ngày
(9 Nhận xét)
4.4
€250 EUR trong 3 ngày
(19 Nhận xét)
4.8
€155 EUR trong 3 ngày
(4 Nhận xét)
3.2
MzHashmi

Hi... I am very curious about your project. It has raised great interest in me. I have previously implemented many algorithms. I can implement it on multiple platforms. Pay only when you are fully satisfied by my wo Thêm

€222 EUR trong 3 ngày
(3 Nhận xét)
2.2
€155 EUR trong 3 ngày
(0 Nhận xét)
0.0