One of the problems of natural deduction
systems like Fitch,
Is that we must often choose from
infinitely many possible instances.
For example, the assumption rule allows us
to assume almost any legal sentence.
And the universal elimination rule allows
us to substitute almost any legal term for
the variables in universally quantified
sentences.
Relational resolution is approved system
for relational logic that does not have
this problem.
As we shall see, relational resolution
allows us to derive conclusions from
premises without making any arbitrary
substitutions.
Like propositional resolution, relational
resolution relies on a single rule of
inference called a resolution principle.
Using the resolution principle alone,
without any axiom scheme in the, or other
rules of inference, it's possible to build
a reasoning system that is able to prove
everything that can be proved in Fitch.
Moreover, the search base using the
resolution principles much smaller than
the search base for generating fitch
proofs.
This lesson is devoted entirely to
relational resolution.
We start with a look at clausal form, a
variation of the language of relational
logic.
We then discuss unification, which is a
key to the power to, of relational
resolution.
And then, we examine the resolution rule
of inference in detail and show how it is
used in relational reasoning.
Finally, we show how the rule is used in
determining unsatisfiability in checking
logical entailment,
And extracting answers to fill in the
blank type questions.