O'Reilly logo

Introduction to Logic, 2nd Edition by Eric Kao, Michael Genesereth

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

CHAPTER 5

Propositional Resolution

5.1 INTRODUCTION

Propositional Resolution is a powerful rule of inference for Propositional Logic. Using Propositional Resolution (without axiom schemas or other rules of inference), it is possible to build a theorem prover that is sound and complete for all of Propositional Logic. What’s more, the search space using Propositional Resolution is much smaller than for standard Propositional Logic proof systems.

This chapter is devoted entirely to Propositional Resolution. We start with a look at clausal form, a variation of the language of Propositional Logic. We then examine Propositional Resolution. We close with some examples.

5.2 CLAUSAL FORM

Propositional Resolution works only on expressions in clausal form ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required