Booleans as a data type

A recap example: modelling propositional logic

File booleans-facts.pl. The modelling idea is that this is a simple data type:

• we have two booleans, modelled as atomic terms b_true and b_false (functors with arity 0);
• a unary function is modelled as a binary predicate p(I, O);
• a binary function is modelled as a ternary predicate p(I1, I2, O);
• use universal facts to somewhat address DRY (don't repeat yourself).

Can we derive a general approach for data types?

The last two goals are the interesting ones. b_or(b_true, B2, B) has two answers: whatever B2 is, the result is b_true, because the first argument is true. And b_or(B1, B2, B) is the whole truth table of or in two clauses: either B2 is false and the result is just B1, or B2 is true and the result is true.

Improving booleans with rules

File booleans-rules.pl. The same booleans, with b_or and b_implies as rules, defined by composing the other functions:

The resolution of b_implies(b_true, b_false, O), one resolvent per line:

b_implies(b_true, b_false, O)
b_not(b_true, NB1'), b_or(NB1', b_false, O)
b_or(b_false, b_false, O)
b_not(b_false, NB1'), b_not(b_false, NB2'), b_and(NB1', NB2', NB'), b_not(NB', O)
b_not(b_false, NB2'), b_and(b_true, NB2', NB'), b_not(NB', O)
b_and(b_true, b_true, NB'), b_not(NB', O)
b_not(b_true, O)

{O/b_false}

This is the procedural interpretation at work: each goal of a body is replaced, in turn, by the body of a matching clause, until the resolvent is empty, and the substitution is the result.