eyeprolog

A dog licence rule

Who has so many dogs that they need a licence?

A municipal rule says that anyone with more than four dogs needs a dog licence. Applying it means counting, which is an aggregate over all of a person’s dogs, not a property of any single dog. This tiny example shows the counting pattern and how a proof treats a count.

Run it in the playground · Source

The question

Alice has five registered dogs and Bob has two. Who must hold a dog licence?

The facts

hasDog(alice, dog1).
hasDog(alice, dog2).
hasDog(alice, dog3).
hasDog(alice, dog4).
hasDog(alice, dog5).
hasDog(bob, dog6).
hasDog(bob, dog7).

One fact per dog. Nothing records how many dogs a person has; that has to be computed.

The rules

dogCount(Subject, Count) :-
  hasDog(Subject, _any),
  countall(hasDog(Subject, _dog), Count).

mustHave(Subject, dogLicense) :-
  dogCount(Subject, Count),
  (Count > 4).

The first goal of dogCount/2 picks a dog owner, so the count is taken per person. countall/2 counts every solution of hasDog(Subject, _dog). The licence rule compares the count with the threshold.

The answer

eyeprolog examples/dog.pl

mustHave(alice, dogLicense).

Alice has five dogs, which is more than four. Bob, with two, does not need a licence.

The reason

eyeprolog --proof examples/dog.pl

step(dogCount(alice, 5),
     rule(8),
     ['Subject' = alice, 'Count' = 5],
     [hasDog(alice, dog1), countall(hasDog(alice, _dog), 5)]).
step(countall(hasDog(alice, _dog), 5), builtin, [], []).
step(5 > 4, builtin, [], []).

Alice’s count of 5 rests on one of her dogs (to select her) and on the built-in count. Then 5 > 4 gives the licence obligation.

The check

eyeprolog --proof examples/dog.pl > dog.why.pl
eyeprolog --check-proof dog.why.pl examples/dog.pl

condition('C1', resolution, ok, 3).
condition('C4', coverage, ok, 5).
condition('C7', relevance, ok, 6).
obligation(builtin, theory_scoped, countall(hasDog(alice, A), 5)).
verdict(checked_with_obligations).

The rule steps replay and 5 > 4 is recomputed. The count itself is an obligation: it depends on the program’s own hasDog/2 facts, so the checker cannot recompute it in isolation and lists it as an assumption instead.

Try it

Give Bob three more dogs. Who needs a licence now?
Change the threshold so that owners of exactly four dogs also need one.
Remove the first goal, hasDog(Subject, _any), from dogCount/2 and ask --goal 'mustHave(Who, L)'. What goes wrong when Subject is unbound?

Learn more in The Art of EyeProlog, Chapter 8 (collecting and choosing answers).

This site is open source. Improve this page.