Đã hoàn thành

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.


— {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


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


while the clause ¬C will be represented by the pair of lists


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.

Kĩ năng: Lập trình C, Lập trình C++, Python, Phát triển phần mềm

Xem nhiều hơn: Project.I need a logo desgined, introduction to algorithms data structures & formal languages, https m freelancer com post project i need some graphic design, i need a project manager in maryland, i need a project manager for startup brasil, i need a project manager for retail, i need a high speed 5 or more data entry operator for our offline project that is only filling the form of 44 fields, i need a graphic designer for one project, i need a crestron engineer for small project, i need a consulting project, i need a consultant to do a project, i need a computer graphics designer for a project, i need a business development manager for web development project, i have 300 pdf page that need to retype in text or word formatt i will allow you to work next 6 months in my project i will pay , hi i need to configure freepbx and asterisk upon a project we have really quick and easy stuff thanks, hello my data httptarekahmedlancerinfosamplesintroductionindexhtml i am ready to do the project you need samples of what i did b, statistics report project introduction, handbag project introduction, making project introduction conclusion, formal letter project

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

ID dự án: #17073831

Được trao cho:


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á)

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


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)

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)
€155 EUR trong 3 ngày
(9 Nhận xét)
€250 EUR trong 3 ngày
(19 Nhận xét)
€155 EUR trong 3 ngày
(4 Nhận xét)

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)
€155 EUR trong 3 ngày
(0 Nhận xét)