>>
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
]
[
class /
co /
eh /
fit /
halp /
jew /
lit /
phi /
pr /
rnb /
sci /
tg /
w /
zom
]
[
a /
grim /
hi /
me /
rx /
vg /
wp /
x
]
[
be /
cake /
cd /
d /
di /
elit /
fag /
fur /
gif /
h /
men /
pco /
s /
sm /
ss /
unf /
v
]