CS 4365语言程序讲解、辅导C/C++编程 调试Matlab程序|讲解留学生Prolog
- 首页 >> Java编程 CS 4365 Artificial Intelligence
Spring 2021
Assignment 3: Knowledge Representation & Reasoning
Part I: Due electronically by Wednesday, April 7, 11:59 p.m.
Part II: Due electronically by Wednesday, April 14, 11:59 p.m.
Part I: Programming (100 points)
In this problem you will be implementing a theorem prover for a clause logic using the resolution
principle. Well-formed sentences in this logic are clauses. As mentioned in class, instead of using
the implicative form, we will be using the disjunctive form, since this form is more suitable for
automatic manipulation. The syntax of sentences in the clause logic is thus:
Clause → Literal ∨ . . . ∨ Literal
Literal → ¬Atom | Atom
Atom → True | False | P | Q | . . .
We will regard two clauses as identical if they have the same literals. For example, q ∨ ¬p ∨ q,
q ∨ ¬p, and ¬p ∨ q are equivalent for our purposes. For this reason, we adopt a standardized
representation of clauses, with duplicated literals always eliminated.
When modeling real domains, clauses are often written in the form:
Literal ∧ . . . ∧ Literal ⇒ Literal
In this case, we need to transform the clauses such that they conform to the syntax of the clause
logic. This can always be done using the following simple rules:
1. (p ⇒ q) is equivalent to (¬p ∨ q)
2. (¬(p ∨ q)) is equivalent to (¬p ∧ ¬q)
3. (¬(p ∧ q)) is equivalent to (¬p ∨ ¬q)
4. ((p ∧ q) ∧ . . .) is equivalent to (p ∧ q ∧ . . .)
5. ((p ∨ q) ∨ . . .) is equivalent to (p ∨ q ∨ . . .)
6. (¬(¬p)) is equivalent to p
The proof theory of the clause logic contains only the resolution rule:
¬a ∨ l1 ∨ . . . ∨ ln,
a ∨ L1 ∨ . . . ∨ Lm
l1 ∨ . . . ∨ ln ∨ L1 ∨ . . . ∨ Lm
If there are no literals l1, . . . ln and L1, . . . , Lm, the resolution rule has the form:
1
¬a, a
False
Remember that inference rules are used to generate new valid sentences, given that a set of old
sentences are valid. For the clause logic this means that we can use the resolution rule to generate
new valid clauses given a set of valid clauses. Consider a simple example where p ⇒ q, z ⇒ y and
p are valid clauses. To prove that q is a valid clause we first need to rewrite the rules to disjunctive
form: ¬p ∨ q, ¬z ∨ y and p. Resolution is then applied to the first and last clause, and we get:
¬p ∨ q, p
q
If False can be deduced by resolution, the original set of clauses is inconsistent. When making
proofs by contradiction this is exactly what we want to do. The approach is illustrated by the
resolution principle explained below.
The Resolution Principle
To prove that a clause is valid using the resolution method, we attempt to show that the negation
of the clause is unsatisfiable, meaning it cannot be true under any truth assignment. This is done
using the following algorithm:
1. Negate the clause and add each literal in the resulting conjunction of literals to the set of
clauses already known to be valid.
2. Find two clauses for which the resolution rule can be applied. Change the form of the
produced clause to the standard form and add it to the set of valid clauses.
3. Repeat 2 until False is produced, or until no new clauses can be produced. If no new clauses
can be produced, report failure; the original clause is not valid. If False is produced, report
success; the original clause is valid.
Consider again our example. Assume we now want to prove that ¬z ∨ y is valid. First, we
negate the clause and get z ∧ ¬y. Then each literal is added to the set of valid clauses (see 4. and
5.). The resulting set of clauses is:
1. ¬p ∨ q
2. ¬z ∨ y
3. p
4. z
5. ¬y
Resolution on 2. and 5. gives:
1. ¬p ∨ q
2
2. ¬z ∨ y
3. p
4. z
5. ¬y
6. ¬z
Finally, we apply the resolution rule on 4. and 6. which produces False. Thus, the original
clause ¬z ∨ y is valid.
(A) The Program
Files and Task Description
Your program should take exactly one argument from the command line:
1. A .kb file that contains the initial KB and the clause whose validity we want to test. The
input file contains n lines organized as follows: the first n − 1 lines describe the initial KB,
while line n contains the (original) clause to test. Note that the KB is written in CNF, so
each clause represents a disjunction of literals. The literals of each clause are separated by a
blank space, while negated variables are prefixed by ∼.
Your program should adhere to the following policy:
• If the negated version of the clause to validate has ANDs, your program should split it into
separate clauses. These clauses should be added to the KB from left to right order.
• Resolution should proceed as follows: For each clause i[1,n] (where n is the last clause in
the KB), attempt to resolve clause i with every previous clause j[1,i) (in order). If a new
clause is generated, it is added to the end of the KB (therefore the value of n changes). Your
system should continue trying to resolve the next clause (i+1) with all previous clauses until
1) a contradiction is found (in which case ’Contradiction’ should be added to the KB) or 2)
all possible resolutions have been performed.
• Redundant generated clauses should not be added to the KB. A clause is redundant if the KB
contains another clause which is logically equivalent to it.
• Clauses that evaluate to True should not be added to the KB.
• Generated clauses should not have redundant (repeated) literals.
3
Requirements: Output
Your program should implement the resolution algorithm as explained in the previous section.
Your program should output a line for every clause in the final KB (in the order they were added),
each line should be single-space-separated and contain: 1) the clause number followed by a period
(starting from 1), 2) the clause in DNF, and 3) the parent clauses (if this clause was generated
through resolution) written as {i, j}. Finally, your program should print a final line containing the
word Valid or Fail depending on whether the proof by contradiction succeeded or not.
Let us consider a correct solution for testing the validity of ¬z ∨ y, given the input:
∼p q
∼z y
p
∼z y
Your program’s output should be:
1. ∼p q {}
2. ∼z y {}
3. p {}
4. z {}
5. ∼y {}
6. q {3, 1}
7. y {4, 2}
8. ∼z {5, 2}
6. Contradiction {7, 5}
Valid
(B) Power Plant Diagnosis
In the last part of this assignment you will be using your resolution prover to verify the safety
requirements of a reactor unit in a nuclear power plant. The reactor unit is shown in the figure on
the next page and consists of a reactor R, two heat exchangers H1 and H2, two steam valves V 1
and V 2, and a control stick l for changing the level of energy production. The state of the reactor
unit is given by 5 propositional variables l, okH1, okH2, V 1 and V 2. If l has the value True
the production level is 2 energy units. Otherwise, the production level is 1 energy unit. At least
one working heat exchanger is necessary for each energy unit produced to keep the reactor from
overheating. Unfortunately a heat exchanger i can start leaking reactive water from the internal
cooling system to the surroundings. okHi is False if heat exchanger Hi is leaking. Otherwise,
okHi is True. When a heat exchanger i is leaking, it must be shut off by closing its valve V i. The
state variable V i indicates whether the valve V i is closed (False) or open (True). Formally, the
safety requirements are described by the following clauses:
4
NoLeak ∧ LowT emp ⇒ ReactorUnitSafe
NoLeakH1 ∧ NoLeakH2 ⇒ NoLeak
okH1 ⇒ NoLeakH1
¬okH1 ∧ ¬V 1 ⇒ NoLeakH1
okH2 ⇒ NoLeakH2
¬okH2 ∧ ¬V 2 ⇒ NoLeakH2
l ∧ V 1 ∧ V 2 ⇒ LowT emp
¬l ∧ V 1 ⇒ LowT emp
¬l ∧ V 2 ⇒ LowT emp
Assume that the current state of the reactor unit is given by the clauses:
¬l
¬okH2
okH1
V 1
¬V 2
1. Rewrite the safely rules from their implicative form to the disjunctive form used by your
resolution prover. The initial set of valid clauses is the union of the rule clauses and the
clauses defining the current state. Write the clauses in a file called facts.txt.
2. Use your resolution prover to test whether LowT emp is a valid clause:
(a) Save the input in a file called task1.in.
(b) Test the result of your prover.
3. Now test the validity of ReactorUnitSafe in a similar way:
(a) Save the input in a file called task2.in.
(b) Test the result of your prover.
4. Consider a simpler set of safety rules:
5
NoLeakH1 ∧ NoLeakH2 ⇒ NoLeak
okH1 ⇒ NoLeakH1
¬okH1 ∧ ¬V 1 ⇒ NoLeakH1
okH2 ⇒ NoLeakH2
¬okH2 ∧ ¬V 2 ⇒ NoLeakH2
and a reduced current state description:
¬okH2
okH1
¬V 2
Test the validity of ¬NoLeak:
(a) Save the input in a file task3.in.
(b) Test the result of your prover.
Implementation and Submission Requirements
The program must be written in C/C++, Java (JDK 8), or Python, and needs to be run/compile
on the UTD Linux boxes without installing extra software.
You may submit as many source files as needed, but you must make sure your provide a
main code entry that follows the following naming convention:
• Java: Main.java
• Python: main.py
• C: main.c
• C++: main.cpp
Your code should not use any external libraries.
Submission
You must directly submit all your source files, task 1, 2, and 3 .in files, and the facts.txt file
to eLearning (do not put them in a folder or zip file). Any program that does not conform to
this specification will receive no credit.
Grading
Make sure you follow the formatting from the example test files: be careful not to insert
extra lines, tabs instead of spaces, etc ... When you submit, your code will be graded using
hidden test cases, so we encourage you to test your code thoroughly.
6
Important: Be mindful of the efficiency of your implementation; as the test cases we will
use are quite long, poorly written code might time out (and receive no credit!). We will
provide you with example input files and approximate timings for each, so you can get an
idea of how fast your code is.
Part II: Written Problems (100 points)
1. Representing Sentences in First-Order Logic (32 points)
Assume that you are given the following predicates, where the universe of discourse consists
of all the students in your class.
I(x): x has an Internet connection
C(x, y): x and y have chatted over the Internet
Write the following statements using these predicates and any needed quantifiers.
(a) Exactly one student in your class has an Internet connection.
(b) Everyone except one student in your class has an Internet connection.
(c) Everyone in your class with an Internet connection has chatted over the Internet with
at least one other student in your class.
(d) Someone in your class has an Internet connection but has not chatted with anyone else
in your class.
(e) There are two students in your class who have not chatted with each other over the
Internet.
(f) There is a student in your class who has chatted with everyone in your class over the
Internet.
(g) There are at least two students in your class who have not chatted with the same person
in your class.
(h) There are two students in the class who between them have chatted with everyone else
in the class.
2. Validity and Satisfiability (8 points)
For each of the sentences below, decide whether it is valid, satisfiable, or neither. Verify your
decisions using truth tables or the Boolean equivalence rules.
(a) Big ∨ Dumb ∨ (Big ⇒ Dumb)
(b) (Smoke ⇒ F ire) ⇒ ((Smoke ∧ Heat) ⇒ F ire)
3. Models (12 points)
Consider a world in which there are only four proposition, A, B, C, and D. How many
models are there for the following sentences? Justify your answer.
7
(a) (A ∧ B) ∨ (B ∧ C)
(b) A ∨ B
(c) A ⇔ B ⇔ C
4. Unification (12 points)
Compute the most general unifier (mgu) for each of the following pairs of atomic sentences,
or explain why no mgu exists. (Recall that lowercase letters denote variables, and uppercase
letters denote constants.)
(a) Q(y, Gee(A, B)), Q(Gee(x, x), y).
(b) Older(F ather(y), y), Older(F ather(x), John).
(c) Knows(F ather(y), y), Knows(x, x).
5. Inference in First-Order Logic (36 points)
Consider the following statements in English.
1. Every child loves every candy.
2. Anyone who loves some candy is not a nutrition fanatic.
3. Anyone who eats any pumpkin is a nutrition fanatic.
4. Anyone who buys any pumpkin either carves it or eats it.
5. John buys a pumpkin.
6. Lifesavers is a candy.
Assume that you are given the following predicates:
• Child(x) — x is a child.
• F anatic(x) — x is a nutrition fanatic.
• Candy(y) — y is a candy.
• P umpkin(y) — y is a pumpkin.
• Carves(x, y) — x carves y.
• Eats(x, y) — x eats y.
• Buys(x, y) — x buys y.
• Loves(x, y) — x loves y.
(a) (12 pts) Translate the six statements above into first-order logic using these predicates.
(b) (12 pts) Convert the six sentences in part (a) into clausal form.
(c) (12 pts) Prove using resolution by refutation that If John is a child, then John carves
some pumpkin. Show any unifiers required for the resolution. Be sure to provide a
clear numbering of the sentences in the knowledge base and indicate which sentences
are involved in each step of the proof.
8
Spring 2021
Assignment 3: Knowledge Representation & Reasoning
Part I: Due electronically by Wednesday, April 7, 11:59 p.m.
Part II: Due electronically by Wednesday, April 14, 11:59 p.m.
Part I: Programming (100 points)
In this problem you will be implementing a theorem prover for a clause logic using the resolution
principle. Well-formed sentences in this logic are clauses. As mentioned in class, instead of using
the implicative form, we will be using the disjunctive form, since this form is more suitable for
automatic manipulation. The syntax of sentences in the clause logic is thus:
Clause → Literal ∨ . . . ∨ Literal
Literal → ¬Atom | Atom
Atom → True | False | P | Q | . . .
We will regard two clauses as identical if they have the same literals. For example, q ∨ ¬p ∨ q,
q ∨ ¬p, and ¬p ∨ q are equivalent for our purposes. For this reason, we adopt a standardized
representation of clauses, with duplicated literals always eliminated.
When modeling real domains, clauses are often written in the form:
Literal ∧ . . . ∧ Literal ⇒ Literal
In this case, we need to transform the clauses such that they conform to the syntax of the clause
logic. This can always be done using the following simple rules:
1. (p ⇒ q) is equivalent to (¬p ∨ q)
2. (¬(p ∨ q)) is equivalent to (¬p ∧ ¬q)
3. (¬(p ∧ q)) is equivalent to (¬p ∨ ¬q)
4. ((p ∧ q) ∧ . . .) is equivalent to (p ∧ q ∧ . . .)
5. ((p ∨ q) ∨ . . .) is equivalent to (p ∨ q ∨ . . .)
6. (¬(¬p)) is equivalent to p
The proof theory of the clause logic contains only the resolution rule:
¬a ∨ l1 ∨ . . . ∨ ln,
a ∨ L1 ∨ . . . ∨ Lm
l1 ∨ . . . ∨ ln ∨ L1 ∨ . . . ∨ Lm
If there are no literals l1, . . . ln and L1, . . . , Lm, the resolution rule has the form:
1
¬a, a
False
Remember that inference rules are used to generate new valid sentences, given that a set of old
sentences are valid. For the clause logic this means that we can use the resolution rule to generate
new valid clauses given a set of valid clauses. Consider a simple example where p ⇒ q, z ⇒ y and
p are valid clauses. To prove that q is a valid clause we first need to rewrite the rules to disjunctive
form: ¬p ∨ q, ¬z ∨ y and p. Resolution is then applied to the first and last clause, and we get:
¬p ∨ q, p
q
If False can be deduced by resolution, the original set of clauses is inconsistent. When making
proofs by contradiction this is exactly what we want to do. The approach is illustrated by the
resolution principle explained below.
The Resolution Principle
To prove that a clause is valid using the resolution method, we attempt to show that the negation
of the clause is unsatisfiable, meaning it cannot be true under any truth assignment. This is done
using the following algorithm:
1. Negate the clause and add each literal in the resulting conjunction of literals to the set of
clauses already known to be valid.
2. Find two clauses for which the resolution rule can be applied. Change the form of the
produced clause to the standard form and add it to the set of valid clauses.
3. Repeat 2 until False is produced, or until no new clauses can be produced. If no new clauses
can be produced, report failure; the original clause is not valid. If False is produced, report
success; the original clause is valid.
Consider again our example. Assume we now want to prove that ¬z ∨ y is valid. First, we
negate the clause and get z ∧ ¬y. Then each literal is added to the set of valid clauses (see 4. and
5.). The resulting set of clauses is:
1. ¬p ∨ q
2. ¬z ∨ y
3. p
4. z
5. ¬y
Resolution on 2. and 5. gives:
1. ¬p ∨ q
2
2. ¬z ∨ y
3. p
4. z
5. ¬y
6. ¬z
Finally, we apply the resolution rule on 4. and 6. which produces False. Thus, the original
clause ¬z ∨ y is valid.
(A) The Program
Files and Task Description
Your program should take exactly one argument from the command line:
1. A .kb file that contains the initial KB and the clause whose validity we want to test. The
input file contains n lines organized as follows: the first n − 1 lines describe the initial KB,
while line n contains the (original) clause to test. Note that the KB is written in CNF, so
each clause represents a disjunction of literals. The literals of each clause are separated by a
blank space, while negated variables are prefixed by ∼.
Your program should adhere to the following policy:
• If the negated version of the clause to validate has ANDs, your program should split it into
separate clauses. These clauses should be added to the KB from left to right order.
• Resolution should proceed as follows: For each clause i[1,n] (where n is the last clause in
the KB), attempt to resolve clause i with every previous clause j[1,i) (in order). If a new
clause is generated, it is added to the end of the KB (therefore the value of n changes). Your
system should continue trying to resolve the next clause (i+1) with all previous clauses until
1) a contradiction is found (in which case ’Contradiction’ should be added to the KB) or 2)
all possible resolutions have been performed.
• Redundant generated clauses should not be added to the KB. A clause is redundant if the KB
contains another clause which is logically equivalent to it.
• Clauses that evaluate to True should not be added to the KB.
• Generated clauses should not have redundant (repeated) literals.
3
Requirements: Output
Your program should implement the resolution algorithm as explained in the previous section.
Your program should output a line for every clause in the final KB (in the order they were added),
each line should be single-space-separated and contain: 1) the clause number followed by a period
(starting from 1), 2) the clause in DNF, and 3) the parent clauses (if this clause was generated
through resolution) written as {i, j}. Finally, your program should print a final line containing the
word Valid or Fail depending on whether the proof by contradiction succeeded or not.
Let us consider a correct solution for testing the validity of ¬z ∨ y, given the input:
∼p q
∼z y
p
∼z y
Your program’s output should be:
1. ∼p q {}
2. ∼z y {}
3. p {}
4. z {}
5. ∼y {}
6. q {3, 1}
7. y {4, 2}
8. ∼z {5, 2}
6. Contradiction {7, 5}
Valid
(B) Power Plant Diagnosis
In the last part of this assignment you will be using your resolution prover to verify the safety
requirements of a reactor unit in a nuclear power plant. The reactor unit is shown in the figure on
the next page and consists of a reactor R, two heat exchangers H1 and H2, two steam valves V 1
and V 2, and a control stick l for changing the level of energy production. The state of the reactor
unit is given by 5 propositional variables l, okH1, okH2, V 1 and V 2. If l has the value True
the production level is 2 energy units. Otherwise, the production level is 1 energy unit. At least
one working heat exchanger is necessary for each energy unit produced to keep the reactor from
overheating. Unfortunately a heat exchanger i can start leaking reactive water from the internal
cooling system to the surroundings. okHi is False if heat exchanger Hi is leaking. Otherwise,
okHi is True. When a heat exchanger i is leaking, it must be shut off by closing its valve V i. The
state variable V i indicates whether the valve V i is closed (False) or open (True). Formally, the
safety requirements are described by the following clauses:
4
NoLeak ∧ LowT emp ⇒ ReactorUnitSafe
NoLeakH1 ∧ NoLeakH2 ⇒ NoLeak
okH1 ⇒ NoLeakH1
¬okH1 ∧ ¬V 1 ⇒ NoLeakH1
okH2 ⇒ NoLeakH2
¬okH2 ∧ ¬V 2 ⇒ NoLeakH2
l ∧ V 1 ∧ V 2 ⇒ LowT emp
¬l ∧ V 1 ⇒ LowT emp
¬l ∧ V 2 ⇒ LowT emp
Assume that the current state of the reactor unit is given by the clauses:
¬l
¬okH2
okH1
V 1
¬V 2
1. Rewrite the safely rules from their implicative form to the disjunctive form used by your
resolution prover. The initial set of valid clauses is the union of the rule clauses and the
clauses defining the current state. Write the clauses in a file called facts.txt.
2. Use your resolution prover to test whether LowT emp is a valid clause:
(a) Save the input in a file called task1.in.
(b) Test the result of your prover.
3. Now test the validity of ReactorUnitSafe in a similar way:
(a) Save the input in a file called task2.in.
(b) Test the result of your prover.
4. Consider a simpler set of safety rules:
5
NoLeakH1 ∧ NoLeakH2 ⇒ NoLeak
okH1 ⇒ NoLeakH1
¬okH1 ∧ ¬V 1 ⇒ NoLeakH1
okH2 ⇒ NoLeakH2
¬okH2 ∧ ¬V 2 ⇒ NoLeakH2
and a reduced current state description:
¬okH2
okH1
¬V 2
Test the validity of ¬NoLeak:
(a) Save the input in a file task3.in.
(b) Test the result of your prover.
Implementation and Submission Requirements
The program must be written in C/C++, Java (JDK 8), or Python, and needs to be run/compile
on the UTD Linux boxes without installing extra software.
You may submit as many source files as needed, but you must make sure your provide a
main code entry that follows the following naming convention:
• Java: Main.java
• Python: main.py
• C: main.c
• C++: main.cpp
Your code should not use any external libraries.
Submission
You must directly submit all your source files, task 1, 2, and 3 .in files, and the facts.txt file
to eLearning (do not put them in a folder or zip file). Any program that does not conform to
this specification will receive no credit.
Grading
Make sure you follow the formatting from the example test files: be careful not to insert
extra lines, tabs instead of spaces, etc ... When you submit, your code will be graded using
hidden test cases, so we encourage you to test your code thoroughly.
6
Important: Be mindful of the efficiency of your implementation; as the test cases we will
use are quite long, poorly written code might time out (and receive no credit!). We will
provide you with example input files and approximate timings for each, so you can get an
idea of how fast your code is.
Part II: Written Problems (100 points)
1. Representing Sentences in First-Order Logic (32 points)
Assume that you are given the following predicates, where the universe of discourse consists
of all the students in your class.
I(x): x has an Internet connection
C(x, y): x and y have chatted over the Internet
Write the following statements using these predicates and any needed quantifiers.
(a) Exactly one student in your class has an Internet connection.
(b) Everyone except one student in your class has an Internet connection.
(c) Everyone in your class with an Internet connection has chatted over the Internet with
at least one other student in your class.
(d) Someone in your class has an Internet connection but has not chatted with anyone else
in your class.
(e) There are two students in your class who have not chatted with each other over the
Internet.
(f) There is a student in your class who has chatted with everyone in your class over the
Internet.
(g) There are at least two students in your class who have not chatted with the same person
in your class.
(h) There are two students in the class who between them have chatted with everyone else
in the class.
2. Validity and Satisfiability (8 points)
For each of the sentences below, decide whether it is valid, satisfiable, or neither. Verify your
decisions using truth tables or the Boolean equivalence rules.
(a) Big ∨ Dumb ∨ (Big ⇒ Dumb)
(b) (Smoke ⇒ F ire) ⇒ ((Smoke ∧ Heat) ⇒ F ire)
3. Models (12 points)
Consider a world in which there are only four proposition, A, B, C, and D. How many
models are there for the following sentences? Justify your answer.
7
(a) (A ∧ B) ∨ (B ∧ C)
(b) A ∨ B
(c) A ⇔ B ⇔ C
4. Unification (12 points)
Compute the most general unifier (mgu) for each of the following pairs of atomic sentences,
or explain why no mgu exists. (Recall that lowercase letters denote variables, and uppercase
letters denote constants.)
(a) Q(y, Gee(A, B)), Q(Gee(x, x), y).
(b) Older(F ather(y), y), Older(F ather(x), John).
(c) Knows(F ather(y), y), Knows(x, x).
5. Inference in First-Order Logic (36 points)
Consider the following statements in English.
1. Every child loves every candy.
2. Anyone who loves some candy is not a nutrition fanatic.
3. Anyone who eats any pumpkin is a nutrition fanatic.
4. Anyone who buys any pumpkin either carves it or eats it.
5. John buys a pumpkin.
6. Lifesavers is a candy.
Assume that you are given the following predicates:
• Child(x) — x is a child.
• F anatic(x) — x is a nutrition fanatic.
• Candy(y) — y is a candy.
• P umpkin(y) — y is a pumpkin.
• Carves(x, y) — x carves y.
• Eats(x, y) — x eats y.
• Buys(x, y) — x buys y.
• Loves(x, y) — x loves y.
(a) (12 pts) Translate the six statements above into first-order logic using these predicates.
(b) (12 pts) Convert the six sentences in part (a) into clausal form.
(c) (12 pts) Prove using resolution by refutation that If John is a child, then John carves
some pumpkin. Show any unifiers required for the resolution. Be sure to provide a
clear numbering of the sentences in the knowledge base and indicate which sentences
are involved in each step of the proof.
8