1
00:00:00,000 --> 00:00:05,218
One of the problems of natural deduction
systems like Fitch,

2
00:00:05,218 --> 00:00:11,393
Is that we must often choose from
infinitely many possible instances.

3
00:00:11,393 --> 00:00:18,178
For example, the assumption rule allows us
to assume almost any legal sentence.

4
00:00:18,178 --> 00:00:25,571
And the universal elimination rule allows
us to substitute almost any legal term for

5
00:00:25,571 --> 00:00:29,920
the variables in universally quantified
sentences.

6
00:00:30,260 --> 00:00:35,022
Relational resolution is approved system
for relational logic that does not have

7
00:00:35,022 --> 00:00:38,020
this problem.
As we shall see, relational resolution

8
00:00:38,020 --> 00:00:42,430
allows us to derive conclusions from
premises without making any arbitrary

9
00:00:42,430 --> 00:00:45,664
substitutions.
Like propositional resolution, relational

10
00:00:45,664 --> 00:00:50,250
resolution relies on a single rule of
inference called a resolution principle.

11
00:00:50,250 --> 00:00:54,530
Using the resolution principle alone,
without any axiom scheme in the, or other

12
00:00:54,530 --> 00:00:59,029
rules of inference, it's possible to build
a reasoning system that is able to prove

13
00:00:59,029 --> 00:01:03,090
everything that can be proved in Fitch.
Moreover, the search base using the

14
00:01:03,090 --> 00:01:07,315
resolution principles much smaller than
the search base for generating fitch

15
00:01:07,315 --> 00:01:11,127
proofs.
This lesson is devoted entirely to

16
00:01:11,127 --> 00:01:15,122
relational resolution.
We start with a look at clausal form, a

17
00:01:15,122 --> 00:01:18,135
variation of the language of relational
logic.

18
00:01:18,135 --> 00:01:22,917
We then discuss unification, which is a
key to the power to, of relational

19
00:01:22,917 --> 00:01:26,258
resolution.
And then, we examine the resolution rule

20
00:01:26,258 --> 00:01:30,908
of inference in detail and show how it is
used in relational reasoning.

21
00:01:31,105 --> 00:01:36,410
Finally, we show how the rule is used in
determining unsatisfiability in checking

22
00:01:36,410 --> 00:01:40,144
logical entailment,
And extracting answers to fill in the

23
00:01:40,144 --> 00:01:41,520
blank type questions.