## Paramodulation vs. Resolution

### February 2, 2013

Equations are ubiquitous in mathematics, physics, and computer science. In database field an optimizer rewriting a query to standard *restrict-project-join* leverages relational algebra identities. The craft of those reasoning abilities is culminated in Automated Theorem Proving systems.

Modern systems, such as Prover9, employs many sophisticated techniques, but as far as equality is concerned, paramodulation rules them all. In a seminal paper Robinson & Wos give an example of a problem which solution takes 47 steps with paramodulation vs. 136 steps with resolution.

The difference can be even more dramatic. Consider lattice idempotence law derived from the two absorption axioms:

`formulas(assumptions).`

x ^ (x v y) = x.

x v (x ^ y) = x.

end_of_list.

```
```

`formulas(goals).`

x ^ x = x.

end_of_list.

It takes Prover9 just a single paramodulation step and 0.00 (+ 0.03) seconds. To compare it with resolution, we have to explicitly write down equality identities fit to the two lattice operations:

`x = x.`

x != y | y = x.

x != y | y != z | x = z.

x != y | x ^ z = y ^ z.

x != y | z ^ x = z ^ y.

x != y | x v z = y v z.

x != y | z v x = z v y.

This explosion of axioms alone hints that the proof length must increase. It is the magnitude of the increase that caught me by surprise: 98 steps and 101 sec.