Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: THEend8_
CS262 Logic and Verification: Coursework assignment
Resolution proof system in Prolog
1 The rules
This assignment is worth 15% of the module overall. The absolute number of points that can
be achieved is 50. The assignment is stated in a quite concise way below, but you will realise
that it comprises a relatively large chunk of work. It is your responsibility to divide this work
up into reasonable steps, and to plan ahead what you will do when. To complete the assignment
successfully, you will combine many of the concepts we learned in lecture and put them together
in Prolog. Moreover, you will have to do some independent reading. Specifically, the assignment
is Exercise 3.3.3 from Fitting’s book mentioned in the literature section of the module’s Moodle
website, and the book provides a step-by-step guide to coming up with a solution, which you will
see when reading the previous sections. The book is available online via the ‘Reading list’ link
provided on the Moodle website. Some of the code for your program will be taken verbatim from
Fitting’s book (which is allowed), some other code will have to be modified, and some code will
have to be written newly.
You will have the opportunity to attend the lab sessions in weeks 8-10 of term 2, where tutors will
be present and ready to answer your questions that may come up during solving the assignment.
They will also take time to revisit and explain some of the fundamental concepts (concerning
resolution and Prolog) that you will need to solve the assignment. There will also be additional
Prolog problems provided that you may work on during the lab sessions to prepare you for this
coursework and practise your Prolog skills.
This is an individual assignment and you should therefore complete it on your own.
2 The assignment
Write a resolution theorem prover in Prolog, and test it on the ten propositional formulas given
below.
[40+10 points]
Use the tableau theorem prover specified in Fitting’s book as a starting point. Your program
should be able to handle negation (¬), and all primary (∧, ∨, →, ←, ↑, ↓, ̸→, ̸←) and secondary
(≡, ̸≡) connectives in an input formula.
3 Step-by-step guide
As a first step, write a Prolog program that transforms a given propositional formula into conjunc
tive normal form. In this, follow the example program given in Section 2.9 of Fitting’s book, which
shows a program to transform a propositional formula into disjunctive normal form.
1In your program, you need to define the unary operator neg and the binary operators and,
or, imp, revimp, uparrow, downarrow, notimp, and notrevimp, which denote the eight aforemen
tioned primary connectives (see Table 2.1 in the book). Also reuse the predicates conjunctive/1,
disjunctive/1 that recognise α- and β-formulas, and the predicates components/3 and component/2
that split formulas into their components (see Table 2.2 in the book). The interface of this part
of the program should be a predicate clauseform(X,Y), where Y is the conjunctive normal form
of the formula X. For example, for the query ?- clauseform(a imp b, Y)., the result should be
Y=[[neg a, b]], and for the query ?- clauseform(neg(a uparrow b), Y), the result should be
Y=[[a],[b]].