From four dots on an X-ray to an alarm — with the reason it fired, and every calculation rechecked.
lldm.pl · output · proof · check · try it in the playground
When one leg is noticeably longer than the other, doctors want to know by how much. One way is to mark points — landmarks — on an X-ray image (a radiograph) and measure between them.
This example takes one measurement, meas47, with four landmarks, and asks:
How long is each leg, how big is the difference, and is it over the 1.25 cm threshold? If an alarm goes off, it should say why.
(An illustration of reasoning, adapted from the Eyeling example
lldm.n3 — not a clinical tool.)
The measured coordinates, in centimetres, and the threshold:
val(meas47, p1xCm, 10.1).
val(meas47, p1yCm, 7.8).
% … landmarks 2, 3 and 4 the same way
threshold(meas47, lld_alarm_threshold_cm, 1.25).
Then one rule per intermediate value — 37 in all — such as the final leg length and the difference:
val(M, d53Cm, Z) :- measurement(M), val(M, ssd53Cm2, X), (Z is X ** 0.5).
val(M, dCm, Z) :- measurement(M), val(M, d53Cm, X), val(M, d64Cm, Y), (Z is X - Y).
alarm(M, 'discrepancy below negative threshold') :- measurement(M), val(M, dCm, D), threshold(M, lld_alarm_threshold_cm, T), (Negt is 0 - T), (D < Negt).
alarm(M, 'discrepancy above threshold') :- measurement(M), val(M, dCm, D), threshold(M, lld_alarm_threshold_cm, T), (D > T).
Two rules, one per side. Each carries its own reason, so the output says which side of the threshold was crossed. (The version this was adapted from gave the same reason for both.)
type(meas47, lld_alarm).
lld_left_length_cm(meas47, 21.548900464617255).
lld_right_length_cm(meas47, 23.45713444515475).
lld_discrepancy_cm(meas47, -1.9082339805374957).
lld_threshold_cm(meas47, 1.25).
lld_reason(meas47, 'discrepancy below negative threshold').
The left leg measures about 21.55 cm, the right about 23.46 cm. The left is 1.91 cm shorter — past the 1.25 cm limit — so the alarm is raised, with its reason.
The proof walks from the raw dots to the alarm:
Every intermediate number is its own named value, so each one is visible.
A separate checker read the proof’s 93 steps against the program:
Verdict: checked. Nothing taken on trust.
node bin/eyedia.js examples/lldm.pl # the alarm and its reason
node bin/eyedia.js --proof examples/lldm.pl # with every calculation
Or open it in the playground.
Change the threshold from 1.25 to 2.0 and run again: the output is
empty. A 1.91 cm difference is within that limit, so no alarm — and nothing
to report.
An alarm you cannot question is hard to act on. Here the alarm arrives with its numbers and its reason, and behind them a proof in which every step of geometry has been recomputed by an independent checker.