Robotics Reference
In-Depth Information
the statement
for all
men referred to as
A
and
for all
men referred to as
B,
if
A
is the brother of
BthenB
is the brother of
A
can be expressed in a more computer-like way as
for all
(
A
,
B
) [the brother of
A
is
Bimplies
that the brother of
B
is
A
]
3
More symbolically, and using the normal shorthand symbols of logic,
where
∀
means “for all” and
⊃
means “implies”, we can express this as
∀
⊃
(
A
,
B
)[brother(
A
,
B
)
brother (
B
,
A
)]
You should be able to see that this symbolic expression represents the
original statement: “
for all
men referred to as
A
and
for all
men referred
to as
B,
if
A
is the brother of
BthenB
is the brother of
A
”. But the
symbolic form is more easily manipulated inside a computer than is the
original statement.
Logical Reasoning
One of the most important problems in Artificial Intelligence is how
to enable computers to draw logical conclusions from known facts, the
process of reasoning. We can look at the task of proving a theorem in
logic, or solving a problem that requires the use of logic, in the following
way. A proof is a sequence of expressions such that every expression in
the sequence is either one of the already accepted theorems or axioms,
or an expression that can be obtained from one or two of the already
accepted theorems or axioms by applying one of the rules of inference,
such as that described in footnote 5.
The Logic Theory Machine
The first programmed deduction system was developed by Allen Newell,
Herbert Simon and John Shaw at Carnegie Institute of Technology
4
and
described by Newell and Simon during the 1956 Dartmouth workshop.
3
Note that “
X
implies
Y
” means that “
Y
can be deduced from
X
”.
4
Later called Carnegie-Mellon University.
