Tip:
Highlight text to annotate it
X
[sound]. One of the problems of using axiom schemata is that there are many
possible instances to consider. In some cases, we have to try many alternatives
before we hit upon an instance that leads to a proof. The same is true in making
assumptions in structured proofs. There are many things we can assume. And it's
challenging to figure out which is going to be useful. In this lesson, we look at a
proof method that does not require that we make arbitrary choices from among
infinitely many possible instances of schemata or assumptions. The method is
based on a rule of inference called propositional resolution. Using
propositional resolution without axiom schemata, without other rules of
inference, and without subproofs, it's possible to create a proof method that is
sound and complete for all of propositional logic. What's more, the
search space using propositional resolution is much smaller than for other
methods. This lesson is devoted entirely too propositional resolution. We start
with a look at clausal form, a variation of the language of propositional logic. We
then examine the rule of resolution in detail. Then we show how the rule is used
in a proof procedure that is sound and complete for all of propositional logic.
Finally, we close with a look at box logic. An interesting logic inspired