This publication has gone through many revisions, with the more recent ones using slightly less insightful notation. I found this early copy over at REMath

http://65.99.230.10:81/collect/computer/index/assoc/HASH0183.dir/doc.pdf

In short, we model problems as a system of "reverse" implication constraints inductively defined on the base order logic; to model computation, we attempt to disprove assertions that are known satisfiable in order to construct a counterexample.

For example, we can encode numerals as n \triangleq s^n(0) (here, 0 is some symbol and not the concrete number itself, this is very reminiscent of church encodings) so in order to calculate fib(n), we define a 2-ary predicate

fib(n,m)

to mean that m is the n-th fibonacci number. I.e, the following are true:
fib(0,0) <- fib(0) = 0
fib(1,1) <- fib(1) = 1
fib(1,2)
fib(2,3)
fib(3,4)
fib(5,5)

We can define the constraints that the fib predicate must follow as an inductive set

fib(0,0) <=
fib(1,1) <=

where P(x,...) <= means that P(x,...) holds vacuously, so here, we assert that there exists a symbol 0 such that 0 = fib(0); furthermore, 1 = s(0) = fib(1) as well.

Next, we have

fib(s(s(n)),u) <= fib(n,v), fib(s(n),w), add(v, w, u)

this says that if there exists some symbol v = fib(n) and some other symbol w = fib(n+1) (remember, n+1 is shorthand for s(n)) and if add(v,w,u) also holds, then there must exist some symbol u = fib(s(s(n))) (this just asserts that fib(s(s(n))) exists). Now, add(v,w,u) is a 3-ary rule stating that there exists some u such that u = v+w.

Now, to calculate fib(10), we would assert that

<= fib(10, u)

which says that if there exists u = fib(10), then nothing can be true, meaning that we're asserting that there does not exist u such that u = fib(10). We then work through our base order logic system either applying our rules or strengthening/weakening the system with "guesses" until we come across a counter-example