自动推理代写 CS264A代写 Automated Reasoning代写 hw代写

CS264A: Automated Reasoning

Homework 1

自动推理代写 1. [8 pts] Show that the following sentences are consistent by identifying a world which satisfieseach sentence: • (¬A⇒B) ∧ (A⇒¬B).• (A ∧ B)⇒

1.[8 pts]

Show that the following sentences are consistent by identifying a world which satisfies each sentence:

• (¬A⇒B) ∧ (A⇒¬B).
• (A ∧ B)⇒(¬A ∨ ¬B).

2.[8 pts]

Show that the following sentences are valid by showing that each is true at every world:

• (A⇒B)⇒(¬B⇒¬A).
• ((A ∨ B) ∧ (A⇒C))⇒(B ∨ C).

3.[8 pts]

Prove from the definitions of Boolean quantifiers ∃ and ∀ that (a) ∃P · (∆ ∨ Γ) is equivalent to (∃P · ∆) ∨ (∃P · Γ), and (b) ∀P · (∆ ∧ Γ) is equivalent to (∀P · ∆) ∧ (∀P · Γ).

4.[8 pts]

Convert the following knowledge base into clausal form:

∆ = A⇒B, ¬A⇒(¬B ∧ C), (B ∨ C)⇒D.

5.[8 pts] 自动推理代写

Show that if we have a polynomial-time procedure for model counting, and another for clausal entailment on a knowledge base Γ, then we have a polynomial-time procedure for testing the equivalence between Γ and CNF ∆.

6.[10 pts]

Show using resolution that D ∨ E is entailed by the knowledge base:

∆ = ¬A⇒B, A⇒¬C, ¬D⇒¬B ∧ ¬C, A⇒E.

7.[12 pts]

Show the termination tree for dpll when run on the following KB, assuming that variables are tested according to the order A, B, C, D, E and true expanded before false:

Note that dpll does not use conflict-directed backtracking.

8.[12 pts]

Show a trace of dpll+ on the above KB, assuming that decisions are made according to the constraints given above. At each conflict, show the decision sequence, implication graph, conflict-driven clause, and its assertion level. Assume that conflict-driven clauses are generated using the first-UIP method of Section 3.6.2.

9.[12 pts]

Consider the following knowledge base.

∆ = A⇒B, ¬A⇒(¬B ∧ C), (B ∨ C)⇒D.

Show how you can count the number of models of ∆ using cdpll and draw the termination tree. Assume that you are expanding variables according to the order A, B, C, D and always expand true before false.

10.[14 pts] 自动推理代写

Consider the following knowledge base:

∆ = P₁ ∨ P₂ ∨ P₃, P₁⇒Q, P₂⇒Q, P₃⇒Q.

a. Convert ∆ into clausal form.

b. Apply directed resolution to the clausal form using the variable order P₁, P₂, P₃, Q.

c. Construct a decision tree for ∆ and use it to count the number of models of ∆.

更多代写：代写code  gre在家考作弊  英国商科Midterm代考  商科管理学essay代写  商业伦理学英文论文代写  反思报告代写

合作平台：essay代写 论文代写 写手招聘 英国留学生代写