Here are four different logic programs, each one designed to
find proofs of formulas (A imp B), where A is a conjunction of
several formulas and B is a different conjunction of (some subset)
of the same formulas.
These programs can be loaded using the "as5" logic.
Linear-time algorithm using dynamic clauses,
with a semantic model that proves soundness of the clauses.
Now, we generalize to a logic program that proves that (subset A B)
where A is an intersection of several sets and B is a different
intersection of the same sets.
