Davis, Putnam, Logaman, Loveland Procedure.

It's a long name for a very simple thing actually.

That's it.

Tiny little program.

This is a program that takes a clause set, so that's the first thing to notice.

Like resolution, we're talking clause sets here.

Why?

Because clause sets are so nice.

If you think about it, to implement in a programming language a logical formula,

propositional logic formula, it's quite a lot of work.

You kind of have to have a tree, data structure, and so on.

A clause is very simple.

If you have something of the form p true or q false or r true,

then one of the things you know about this junction is that it is commutative and associative.

You can reorder this.

That's not what I wanted to do.

Nothing changes.

The wonderful thing now is that you can actually say,

this here is essentially letters, three names, decorated by one of two different states.

I can actually make this into a list, p, r, q, and maybe make a pair out of it.

That has the same information.

The pair actually has the true literals from that list first,

and the false literals, that is a very non-beautiful q, last.

They're not losing any information.

Formula are very icky, heavyweight data structures.

Lists is something that are very, very simple data structures.

Pairs are even cheaper.

Think about it and see that you have a couple of pointers, and that's all there is.

We have a pair of two lists.

That's a clause.

That's a clause list.

It's very, very simple to do.

What is resolution?

Take two elements of the list.

See whether the first element of the pair of one and the second element of the other

actually are non-disjoint.

If they are non-disjoint, resolves, which actually makes you another clause,

which is a pair of two lists of names.

If both of these lists are empty, hooray.

Clauses are nice for implementing, which is why implementers use clause normal form.

Of course, there are standard clause normalization algorithms, so you're not losing anything.

That's what we're doing.

We have a procedure.

We have a clause set, which actually is a list of pairs of lists.

We give it as an accumulator argument.

Since this is a recursive thing, we give it a partial interpretation, which is just

how you represent that, a list of a pair, name, true or false, or 0 or 1,

or whatever you want to do here, or just a bit.

Another very, very simple data structure if you want to ever really implement it.

Then if you look at it, this only recursively does one of two things.