Changes

|}

|}

This means that the propositional program itself is nothing more or less than a single proposition or boolean function <math>p : \mathbb{B}^{57} \to \mathbb{B}.</math>

This means that the propositional program itself is nothing but a single proposition or boolean function of the form <math>p : \mathbb{B}^{57} \to \mathbb{B}.</math>

An assignment of boolean values to the above set of boolean variables is called an ''interpretation'' of the proposition <math>p,\!</math> and any interpretation of <math>p\!</math> that makes the proposition <math>p : \mathbb{B}^{57} \to \mathbb{B}</math> evaluate to <math>1\!</math> is referred to as a ''satisfying interpretation'' of the proposition <math>p.\!</math> Another way to specify interpretations, instead of giving them as bit vectors in <math>\mathbb{B}^{57}</math> and trying to remember some arbitrary ordering of variables, is to give them in the form of ''singular propositions'', that is, a conjunction of the form <math>e_1 \cdot \ldots \cdot e_{57}</math> where each <math>e_j\!</math> is either <math>v_j\!</math> or <math>\texttt{(} v_j \texttt{)},</math> that is, either the assertion or the negation of the boolean variable <math>v_j,\!</math> as <math>j\!</math> runs from 1 to 57. Even more briefly, the same information can be communicated simply by giving the conjunction of the asserted variables, with the understanding that each of the others is negated.

An assignment of boolean values to the above set of boolean variables

is called an "interpretation" of P, and any interpretation of P that

makes the proposition P : B^57 -> B evaluate to 1 is referred to as

a "satisfying interpretation" of the proposition P.  Another way to

specify interpretations, instead of giving them as bit vectors in

B^57 and trying to remember some arbitrary ordering of variables,

is to give them in the form of "singular propositions", that is,

a conjunction of the form "e_1 & ... & e_57" where each e_j is

either "v_j" or "(v_j)", that is, either the assertion or the

negation of the boolean variable v_j, as j runs from 1 to 57.

Even more briefly, the same information can be communicated

simply by giving the conjunction of the asserted variables,

with the understanding that each of the others is negated.

A satisfying interpretation of the proposition P supplies us

A satisfying interpretation of the proposition <math>p\!</math> supplies us with all the information of a complete execution history for the corresponding program, and so all we have to do in order to get the output of the program <math>p\!</math> is to read off the proper part of the data from the expression of this interpretation.

with all the information of a complete execution history for

the corresponding program, and so all we have to do in order

to get the output of the program P is to read off the proper

part of the data from the expression of this interpretation.

===Output===

===Output===