## COMP4418, 2019–Assignment 1

Prolog代写 This assignment consists of four questions. The first two questions and the fourth question require written answers only.

Due: 23:59:59pm Sunday 13 October (End of Week 4)

Late penalty: 10 marks per day.

Worth: 15%.

This assignment consists of four questions. The fifirst two questions and the fourth question require written answers only. The third question requires some programming and a written report.

### 1.[**20 Marks**] (Logical Inference) Prolog代写

For each of the following inferences:

(a) prove whether or not the following inferences hold using a suitable semantic method (*|*=); and,

(b) prove whether or not the following inferences hold syntactically using resolution (*`*).

In each case you must provide a proof and clearly state whether the inference holds or whether the inference does not hold.

(i) *p **∧ *(*q **∨ **r*)[*|*= */ **`*](*p **∧ **q*) *∨ *(*p **∧ **r*)

(ii) [*|*= */ **`*]*p **→ *(*q **→ **p*)

(iii) *∃**x.**∀**y.Likes*(*x, y*)[*|*= */ **`*]*∀**x.**∃**y.Likes*(*x, y*)

(iv) *¬**p **→ ¬**q, p **→ **q*[*|*= */ **`*]*p **↔ **q *

(v) *∀**x.P*(*x*) *→ **Q*(*x*)*, **∀**x.Q*(*x*) *→ **R*(*x*)*, **¬**R*(*a*)[*|*= */ **`*]*¬**P*(*a*)

### 2.[**20 Marks**] (Logic Puzzle) Prolog代写

Flatmates, from Logic Problems, Issue 10, page 35. The following logic puzzle appears in the lecture notes and is 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 flflats laid out as in the plan.

(i) Represent these facts as sentences in fifirst-order logic.Prolog代写

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

(iii) 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 flflat.

### 3.[**50 Marks**] (Automated Theorem Proving)

In 1958 the logician Hao Wang implemented one of the fifirst automated theorem provers. He succeeded in writing several programs capable of automatically proving a majority of theorems from the fifirst fifive chapters of Whitehead and Russell’s *Principia Mathematica *(in fact, his program managed to prove over 200 of these theorems “within about 37 minutes, and 12/13 of the time is used for read-in and print-out”). This was an impressive achievement at the time; previous attempts had only succeeded in proving a handful of the theorems in *Principia Mathematica*.

**Background **

Wang’s idea is based around the notion of a *sequent *(this idea had been introduced years earlier by Gentzen) and the manipulation of sequents. A sequent is essentially a list of formulae on either side of a sequent (or provability) symbol *`*. The sequent *π **` **ρ*, where *π *and *ρ *are strings (i.e., lists) of formulae, can be read as “the formulae in the string *ρ **follow *from the formulae in thestring *π*” (or, equivalently, “the formulae in string *π **prove *the formulae in string *ρ*”).Prolog代写

To prove whether a given sequent is true all you need to do is start from some basic sequents and successively apply a series of rules that transform sequents until you end up with the sequent you desire. This process is detailed below.

Additionally, determining whether a formula *φ *is a theorem, is equivalent to determining whether the sequent *∅ ` **φ *is true (e.g., *` ¬**φ **∨ **φ*).

**Formulae Prolog代写**

**Connectives **

We allow the following connectives in decreasing order of precedence:

*¬ *— negation

*∧ *— conjunction; *∨ *— disjunction (both same precedence)

*→ *— implication; *↔ *— biconditional (both same precedence).

**Formula **

*p, q, . . .*) is an*atomic*formula (and thus a formula).*φ, ψ*are formulae, then*¬**φ, φ**∧**ψ, φ**∨**ψ, φ**→**ψ, φ**↔**ψ*are formulae.

**Sequent **

If *π *and *ρ *are strings of formulae (possibly empty strings) and *φ *is a formula, then *π, φ, ρ *is a string and *π **` **ρ *is a sequent.Prolog代写

**Rules **

The logic consists of the following sequent rules. The fifirst rule (P1) gives a characterisation of simple theorems. The remaining rules are simply ways of transforming sequents into new sequents.

The manner in which you can construct a proof for a sequent to determine whether it holds or not is given below.

**P1 **Initial Rule: If *λ, ζ *are strings of atomic formulae, then *λ **` **ζ *is a theorem if some atomic formula occurs on both side of the sequent *`*.Prolog代写

##### In the following ten rules *λ *and *ζ *are always strings (possibly empty) of formulae.

**P2a **Rule *` ¬*: If *φ, ζ **` **λ, ρ*, then *ζ **` **λ, **¬**φ, *

**P2b **Rule *¬ `*: If *λ, ρ **` **π, φ*, then *λ, **¬**φ, ρ **` **π *

**P3a **Rule *` ∧*: If *ζ **` **λ, φ, ρ *and *ζ **` **λ, ψ, ρ*, then *ζ **` **λ, φ **∧ **ψ, ρ *

**P3b **Rule *∧ `*: If *λ, φ, ψ, ρ **` **π*, then *λ, φ **∧ **ψ, ρ **` **π *

**P4a **Rule *` ∨*: If *ζ **` **λ, φ, ψ, ρ*, then *ζ **` **λ, φ **∨ **ψ, ρ *

**P4b **Rule *∨ `*: If *λ, φ, ρ **` **π *and *λ, ψ, ρ **` **π*, then *λ, φ **∨ **ψ, ρ **` **π *

**P5a **Rule *`→*: If *ζ, φ **` **λ, ψ, ρ*, then *ζ **` **λ, φ **→ **ψ, ρ *

**P5b **Rule *→`*: If *λ, ψ, ρ **` **π *and *λ, ρ **` **π, φ*, then *λ, φ **→ **ψ, ρ **` **π *

**P6a **Rule *`↔*: If *φ, ζ **` **λ, ψ, ρ *and *ψ, ζ **` **λ, φ, ρ*, then *ζ **` **λ, φ **↔ **ψ, ρ *

**P6b **Rule *↔`*: If *φ, ψ, λ, ρ **` **π *and *λ, ρ **` **π, φ, ψ*, then *λ, φ **↔ **ψ, ρ **` **π *

**Proofs **

The basic idea in proving a sequent *π **` **ρ *is to begin with instance(s) of Rule P1 and successively apply the remaining rules until you end up with the sequent you are hoping to prove.Prolog代写

For example, suppose you wanted to prove the sequent *¬*(*p **∨ **q*) *` ¬**p*. One possible proof would proceed as follows.

*1.p **` **p, q *

Rule 1

2.*p **` **p **∨ **q *

Rule P4a

*3.` ¬**p, p **∨ **q *

Rule P2a

*4.¬*(*p **∨ **q*) *` ¬**p *

Rule P2b

QED.

However, a simpler idea (as it will involve much less search) is to begin with the sequent(s) to be proved and apply the rules above in the “backward” direction until you end up with the sequent you desire. In the example then, you would begin at Step 4 and apply each of the rules in the backward direction until you end up at Step 1 at which point you can conclude the original sequent is a theorem.Prolog代写

**Question Specifification Prolog代写**

In this assignment you are to emulate Hao Wang’s feats and implement a propositional theorem prover. You may use any programming language to complete this question. You must providea script named assn1q3 or a Makefile that, when the command make is executed, produces an executable fifile assn1q3.

**Input **

The input will consist of a single sequent on the command line. Sequents will be written as:

[*List of Formulae*] seq [

*List of Formulae*] To construct formulae, atoms can be any string of characters (without space) and connectives as follows:

*¬*: neg*∧*: and*∨*: or*→*: imp*↔*: iff

So, for example, the sequent *p **→ **q, **¬**r **→ ¬**q **` **p **→ **r *would be written as:

Your program should be called assn1q3 and run as follows:

./assn1q3 ’*Sequent*’

For example

./assn1q3 ’[p imp q, (neg r) imp (neg q)] seq [p imp r]’

**Output **

The fifirst line of the output will be either true or false indicating whether or not the sequent on the command line holds. This output is worth 40% of the total mark for this question on given and hidden test data. The subsequent lines of output should produce a proof like the one in the *Proofs *section above.

**Marking for this Question **

**References **

[1] Hao Wang, *Toward Mechanical Mathematics*, IBM Journal for Research and Development,volume 4, 1960. (Reprinted in: Hao Wang, ”Logic, Computers, and Sets”, Sciene Press, Peking, Hao Wang, ”A Survey of Mathematical Logic”, North Holland Publishing Company, 1964.Prolog代写

Hao Wang, ”Logic, Computers, and Sets”, Chelsea Publishing Company, New York, 1970.)

[2] Alfred North Whitehead and Bertrand Russell,*Principia Mathematica*, 2nd Edition, Cambridge University Press, Cambridge, England, 1927.

**A List of 10 Propositional Theorems **

You may fifind it instructional to prove these by hand fifirst.

(i) *` ¬**p **∨ **p *

(ii) *¬*(*p **∨ **q*) *` ¬**p *

(iii) *p **` **q **→ **p *

(iv) *p **` **p **∨ **q *

(v) (*p **∧ **q*) *∧ **r **` **p **∧ *(*q **∧ **r*)Prolog代写

(vi) *p **↔ **q **` ¬*(*p **↔ ¬**q*)

(vii) *p **↔ **q **` *(*q **↔ **r*) *→ *(*p **↔ **r*)

(viii) *` *(*¬**p **∧ ¬**q*) *→ *(*p **↔ **q*)

(ix) *p **↔ **q **` *(*p **∧ **q*) *∨ *(*¬**p **∧ ¬**q*)

(x) *p **→ **q, **¬**r **→ ¬**q **` **p **→ **r *

##### 4.[**10 Marks**] (Knowledge Representation and Reasoning)

Select a method for knowledge representation and reasoning that we have not covered in lectures and provide one example that explains:

(i) how the method represents knowledge;

(ii) describes how inference works for reasoning with that knowledge representation.

In answering this question some sources you might consult include:

*Knowledge Representation and Reasoning*, Morgan Kaufmann, 2004.

*Artifificial Intelligence: A Modern Approach*, Third Edition,Prentice Hall, 2010.Prolog代写

*Principles of Knowledge Representation and Reasoning*conference series (www.kr.org).*Association for the Advancement of Artifificial Intelligence*conference series (www.ijcai.org).*International Joint Conference on Artifificial Intelligence*series (www.aaai.org).

**Assignment Submission **

You will need to submit answers to Questions 1, 2, 4 and the report for Question 3 in a PDF fifile named assn1.pdf along with any source code fifiles for Questions 3. Your report for Question 3 in assn1.pdf should describe the additional fifiles you submit for this question and how they can used to replicate/generate your results.

give cs4418 assn1 assn1.pdf assn1-q3-files

The deadline for this submission is 23:59:59am Sunday 13 October.

**Late Submissions **

In case of late submissions, 10% will be deducted from the maximum mark for each day late.

No extensions will be given for any of the assignments (except in case of illness or misadventure).Read the course outline carefully for the rules regarding plagiarism.

其他代写：考试助攻 计算机代写 java代写 function代写 paper代写 web代写 编程代写 report代写 数学代写 algorithm代写 python代写 java代写 code代写 project代写 dataset代写 analysis代写 C++代写 代写CS 金融经济统计代写 essay代写 course代写