http://www.cs.cmu.edu/~fp/courses/lp/
15+26 → (1+2+1)1 → (3+1)1 → 41
computation — a limited form of deduction, establishes theorems
So computation is mechanical and requires no ingenuity, while deduction is a creative process. For example,
a^n + b^n ̸= c^n for n > 2, ... 357 years of hard work ..., QED.
deduction — form of computation if we fix a strategy for proof search, removing the guesswork
George Boole succeeded in reducing a certain class of logical reasoning to computation in so-called Boolean algebras… undecidability results of the 20th centuries we know that not everything we can reason about is in fact mechanically computable….
The most basic notion is that of a judgment, which is an object of knowledge. We know a judgment because we have evidence for it. The kind of evidence we are most interested in is a proof, which we display as a deduction using inference rules.
If J1 and ··· and Jn then we can conclude J by virtue of rule R.
(judgment) A true, ... omit the trailing "true"
To make the transition from inference rules to logic programming we need to impose a particular strategy.
To make the transition from inference rules to logic programming we need to impose a particular strategy…negation does not have first-class status in logic programming.
consider a goal of the form plus(s(z), s(z), R) where R is an
unknown … Search not only constructs a proof, but also a term t
for R such that plus(s(z), s(z), t) is true.
the original goal is called the query, its unknowns are logic variables, and the result of the computation is an answer substitution for the logic variables, suppressing the proof.