On page 36 is the definition for satisfied
A rule is satisfied by a relation if, for each instance of the rule, either the conclusion is in the relation or one of the premises is not.
On page 36 is the definition for instance
An instance of an inference rule is obtained by consistently replacing each metavariable by the same term in the rule's conclusion and all its premises (if any).
if true then true else (if false then false else false) -> true
is an instance of E-IFTRUE, where both occurrences of $t_2$ have been replaced by
trueand $t_3$ has been replaced by
if false then false else false.
On page 15 is the definition for relataion
An n-place relation on a collection of sets $S_1, S_2,..., S_n$ is a set $R\subseteq S_1\times\;S_2\;\times\;...\;\times\;S_n$ of tuples of elements from $S_1$ through $S_n$. We say that the elements $s_1\in > S_1$ thorugh $s_n\in S_n$ are related by $R$ if $(s_1,...,s_n)$ is an element or $R$.
On page 36 is the definition for one-step evaluation relation ($\rightarrow $)
The one-step evaluation relation $\rightarrow $ is the smallest binary relation on terms satisfying the three rules of Figure 3-1. When the pair $(t,t')$ is in the evaluation relation, we say that "the evaluation statement (or judgment) $t \rightarrow t'$ is derivable."
On page 34 are the three rules from Figure 3-1
Can someone explain this definition and give an example for parts of the defintion.
1. The conclusion is in the relation.
2. One of the premises is not.
Note: I am aware that there is a forum dedicated to questions for the book here.
Note: You can use Google Scholar to see more of the details to this question in context.
To connect some of the dots about my comment regarding unification and term rewriting.
When I saw
$$(A\rightarrow B)\equiv (\neg A \vee B)$$
it reminded me of Horn claues from Prolog, that along with the example then connected with my understanding of term rewriting. Having the book "Term Rewriting and All That" (WorldCat) by Franz Baader and Tobias Nipkow, I quickly looked up satisfiability and found satisfiable on page 58. This is actually the start of whole chapter on Equational Problems; but it also covers unification. At that point I realized that the definition was dealing with Satisfiability and from there is was a topic I was already familiar. What threw me was the way Benjamin defined it. He used a very precise definition right up front in a manner I didn't associate with my knowledge.
If you work through the code as I am and understand logic programming, then the definition makes perfect sense.