1. (Propositional Inferences)

For each of the following inferences, prove whether they hold or do not hold in propositional logic using the truth table method.

(a) |= ¬p ∨ p

(b) p |= q → p

(c) (p ∧ q) ∧ r |= p ∧ (q ∧ r)

(d) p ↔ q |= (q ↔ r) → (p ↔ r) (e) p ↔ q |= (p ∧ q) ∨ (¬p ∧ ¬q)

For each of the following inferences, prove whether they hold or do not hold in propositional logic using resolution.

(f) ¬(p ∨ q) |- ¬p

(g) p ∀ p ∨ q

(h) p ↔ q |- ¬(p ↔ ¬q)

(i) ∀ (¬p ∧ ¬q) → (p ↔ q)

(j) p → q, ¬r → ¬q € p → r

2. (Logic Puzzle)

Flatmates, from Logic Problems, Issue 10, page 35.

The following logic puzzle was presented in lectures and solved using Prolog. Here we will determine a solution and argue using interpretations as explained in lectures.

Six people live in a three-storey block of studio flats laid out as in the plan.

- Ivor and the photographer live on the same floor.
- Edwina lives immediately above the medical student.
- Patrick, who is studying law, lives immediately above Ivor, and opposite the air hostess.
- Flat4 is the home of the store detective.
- Doris lives in Flat2.
- Rodney and Rosemary are 2 of the residents in the block of flats.
- One of the residents is a clerk.

(a) Represent these facts as sentences in first-order logic.

(b) From the clues given, work out the name and situation of the resident of each flat. Using your formalisation in part (2a), is it possible to determine the name and situation of the resident of each flat? Show semantically how you determined your answer.

(c) If your answer to part (2b) was ‘no', indicate what further sentences you would need to add to your formalisation so that name and situation of the resident of each flat.

3.

Determining whether a set of clauses is satisfiable or not is a fundamental problem in knowledge representation and reasoning (and in artificial intelligence and computer science where it was the problem considered in describing the notion of NP-complete problems). In order to better understand the computational nature of the satisfiability problem, researchers have investigated various instances of the problem. One well studied instance is 3-SAT which focusses on the satisfiability of sets of clauses

(i.e., disjunctions of literals) which have exactly three literals. For example, {p ∨ q ∨ r, p ∨ ¬s ∨ t}.

3- SAT is known to be NP-complete.

It is also known that 3-SAT exhibits an easy-hard-easy computational pattern. Determining the satisifi- ability of sets of clauses that are small in relation to the total number of distinct propositional variables in the set is usually easy because there are fewer constraints in assigning truth values to the propo- sitional variables. Determining the satisifiability of sets of clauses that are large in relation to the total number of distinct propositional variables in the set is usually easy because there are too many constraints to assign truth values to the propositional variables and the set is unsatisfiable. Somewhere in between these two extremes the satisfiability problem becomes hard.

Your task in this question is to determine empirically at what point the satisfiability problem becomes difficult. More specifically, you are to determine, approximately, a constant value C for number of propositional variables n at which C.n clauses constitutes a hard satisifiability problem.

To help you in this task, the satisfiablity solver minisat is available on the CSE machines from:
~morri/bin/minisat
You can run this program as follows:
~morri/bin/minisat file.cnf
where file.cnf is a file containing clauses in CNF in DIMACS format. DIMACS format consists of three types of lines:

- lines beginning with the letter c are comments;

- one line with the format p cnf variables clauses where variables is the number of propositional variables and clauses is the number of clauses;

- lines specifying clauses where a positive literal is specified by a number (identifying the literal) and a negative literal is specified by the corresponding negative number; each line is terminated by the number 0.

For example, the set of clauses {p ∨ q ∨ r, p ∨ ¬s ∨ t} would be represented DIMACS format as:
c example CNF file with 5 propositional variables and 2 clauses p cnf 5 2
1 2 3 0
1 -4 5 0

While you can write your own satisfiability solver and are welcome to do so, your task is to write a program to randomly generate test files containing clauses and to use these test files to empirically determine the value C explained above.

You are then to write a report explaining your empirical results and how you determined the value C. The use of tables and graphs to support your results is desirable.

For this question you must submit your report as part of the PDF file containing your answers to this assignment along with any source code files used in answering this question.

4. (Resolution)

It is possible to consider several variants to the resolution proof procedure, some of which were men- tioned in lectures. We shall consider one variant here.

- A unit resolution is one in which a resolvent is obtained using at least one parent which is a unit clause (i.e., a single literal) or a unit factor1 of a parent clause.

- A unit deduction is one in which every resolution is a unit resolution.

- A unit refutation is a unit deduction of the empty clause.

(a) While completeness is an important consideration for automated deduction, so is efficiency. At times we may be willing to forego completeness for the sake of efficiency. Show that unit resolution is incomplete. [Hint: exhibit a set of clauses and explain your answer.]

(b) Given a set of Horn clauses, show that there is a unit refutation from S if and only if S is unsatisfiable.

5. (Knowledge Representation and Reasoning)

Select a method for knowledge representation and reasoning that we have not covered in lectures and write 1-2 pages addressing the following:

(a) briefly describe how the method represents knowledge and include an example;

(b) briefly describe the inference procedure(s) adopted by the method for reasoning; and,

(c) identify some importance issues in using the method (try and assess both advantages and short- comings).