Which temperature evidence drives a quarantine?

Keep the message boundary, the evidence policy and the resulting task visible.

program · output · proof · check · playground

The question

A distributor of chilled food receives a temperature reading each time one of its batches changes hands. At the handover of batch A, two sensors disagree: a handheld thermometer reports 7.2°C and a calibrated logger reports 9.4°C. The limit, chosen for illustration, is 8°C. Batch B was handed over at 7.5°C.

Messages arrive numbered in sequence. The distributor has already processed everything up to message 42 (its checkpoint), so only later messages count.

Which reading should drive the decision, which batch must be quarantined, and which destinations need notice?

What we tell eyemind: the data

fact(checkpoint(42), temperature_limit(80))                                    // clauses 1, 2
fact(sensor_priority('handheld', 1), sensor_priority('calibrated_logger', 2))  // 3, 4
// observation(Id, Sample, Batch, Sequence, Sensor, TemperatureTenthC)
fact(observation('old_b', 'old_handover', 'batch_b', 41, 'calibrated_logger', 120))  // 5
fact(observation('handheld_a', 'handover_a', 'batch_a', 43, 'handheld', 72))         // 6
fact(observation('logger_a', 'handover_a', 'batch_a', 44, 'calibrated_logger', 94))  // 7
fact(observation('logger_b', 'handover_b', 'batch_b', 45, 'calibrated_logger', 75))  // 8
fact(destination('batch_a', 'north_depot'), destination('batch_a', 'station_shop'))  // 9, 10
fact(destination('batch_b', 'south_depot'))                                          // 11

Each fact states something true outright, and each item is a numbered clause of the program. Temperatures are whole numbers in tenths of a degree, so 80 means 8.0°C and 94 means 9.4°C. Each observation has an identifier, the sample it measured, the batch, its message number, the sensor and the temperature. The calibrated logger has the higher priority. Message 41 (an old 12°C reading of batch B) falls before the checkpoint.

What we tell eyemind: the rules

implies([observation(Id, Sample, Batch, Sequence, Sensor, Temperature), checkpoint(Committed), gt(Sequence, Committed)],
  current_reading(Id, Sample, Batch, Sensor, Temperature))                                                                   // 12
implies([
  current_reading(_, Sample, Batch, _, Low), current_reading(_, Sample, Batch, _, High),
  temperature_limit(Limit), le(Low, Limit), gt(High, Limit),
], conflicting_sample(Sample, Batch))                                                                                        // 13
implies([
  current_reading(Id, Sample, Batch, Sensor, _), current_reading(_, Sample, Batch, OtherSensor, _),
  sensor_priority(Sensor, Priority), sensor_priority(OtherSensor, OtherPriority), gt(OtherPriority, Priority),
], superseded(Id))                                                                                                           // 14
implies([current_reading(Id, _, Batch, _, Temperature), not(superseded(Id))], selected_reading(Id, Batch, Temperature))      // 15
implies([selected_reading(Id, Batch, Temperature), temperature_limit(Limit), gt(Temperature, Limit)], quarantine(Batch, Id)) // 16
implies([quarantine(Batch, _), destination(Batch, Site)], notify(Site, Batch))                                               // 17
implies(quarantine(Batch, Evidence), inspection_task(Batch, Evidence, Task))                                                 // 18

implies(premise, conclusion) is a forward rule: whenever everything in the premise list holds, eyemind adds the conclusion.
Capitalized names are variables: they stand for whatever value makes the rule fit. _ is a variable we do not care about.
gt(A, B) (A greater than B) and le(A, B) (A less than or equal to B) are built-in comparisons: eyemind calculates them itself instead of looking them up in facts.
not(...) means “it cannot be found”. eyemind decides it by searching: if the goal inside cannot be shown, not succeeds.

In words: rule 12 keeps only messages after the checkpoint. Rule 13 flags a sample with one reading within the limit and another above it. Rule 14 sets a reading aside when a higher-priority sensor read the same sample. Rule 15 selects every current reading that is not set aside. Rule 16 quarantines a batch whose selected reading is above the limit, rule 17 notifies each of its destinations, and rule 18 opens an inspection task for each quarantine.

What eyemind concludes

// Answers: each instance of a query() that holds.
conflicting_sample('handover_a', 'batch_a')
selected_reading('logger_a', 'batch_a', 94)
selected_reading('logger_b', 'batch_b', 75)
quarantine('batch_a', 'logger_a')
notify('north_depot', 'batch_a')
notify('station_shop', 'batch_a')
inspection_task('batch_a', 'logger_a', skolem(18, 'Task', ['batch_a', 'logger_a']))

The handover of batch A is a conflict: 7.2°C is within the limit and 9.4°C is above it. The logger’s 9.4°C is selected, since it outranks the handheld, so batch A is quarantined and its two destinations are notified. Batch B’s selected reading is 7.5°C, so it passes; its older 12°C observation is outside the uncommitted tail of messages.

A task that has an identity

Rule 18 concludes inspection_task(Batch, Evidence, Task). Its last variable, Task, appears nowhere in the premise: the rule says only that some task exists. eyemind gives such an unknown a made-up name, a Skolem term, written skolem(Rule, Variable, Values): skolem(18, 'Task', ['batch_a', 'logger_a']) reads the Task of rule 18 for batch A and evidence logger_a. Repeating the same firing (the same rule with the same values) names the same task, and the name can never be mistaken for anything else. Such an invented name is also called a witness.

The proof, line by line

eyemind --proof writes down how it reached each answer. This is the complete proof:

// Answers: each instance of a query() that holds.
conflicting_sample('handover_a', 'batch_a')
selected_reading('logger_a', 'batch_a', 94)
selected_reading('logger_b', 'batch_b', 75)
quarantine('batch_a', 'logger_a')
notify('north_depot', 'batch_a')
notify('station_shop', 'batch_a')
inspection_task('batch_a', 'logger_a', skolem(18, 'Task', ['batch_a', 'logger_a']))

// Clauses: the program clauses the steps cite, by clause number.
clause(1, fact(checkpoint(42)))
clause(2, fact(temperature_limit(80)))
clause(3, fact(sensor_priority('handheld', 1)))
clause(4, fact(sensor_priority('calibrated_logger', 2)))
clause(6, fact(observation('handheld_a', 'handover_a', 'batch_a', 43, 'handheld', 72)))
clause(7, fact(observation('logger_a', 'handover_a', 'batch_a', 44, 'calibrated_logger', 94)))
clause(8, fact(observation('logger_b', 'handover_b', 'batch_b', 45, 'calibrated_logger', 75)))
clause(9, fact(destination('batch_a', 'north_depot')))
clause(10, fact(destination('batch_a', 'station_shop')))
clause(12, implies([observation(Id, Sample, Batch, Sequence, Sensor, Temperature), checkpoint(Committed), gt(Sequence, Committed)], current_reading(Id, Sample, Batch, Sensor, Temperature)))
clause(13, implies([current_reading(_0, Sample, Batch, _1, Low), current_reading(_2, Sample, Batch, _3, High), temperature_limit(Limit), le(Low, Limit), gt(High, Limit)], conflicting_sample(Sample, Batch)))
clause(14, implies([current_reading(Id, Sample, Batch, Sensor, _0), current_reading(_1, Sample, Batch, OtherSensor, _2), sensor_priority(Sensor, Priority), sensor_priority(OtherSensor, OtherPriority), gt(OtherPriority, Priority)], superseded(Id)))
clause(15, implies([current_reading(Id, _0, Batch, _1, Temperature), not(superseded(Id))], selected_reading(Id, Batch, Temperature)))
clause(16, implies([selected_reading(Id, Batch, Temperature), temperature_limit(Limit), gt(Temperature, Limit)], quarantine(Batch, Id)))
clause(17, implies([quarantine(Batch, _0), destination(Batch, Site)], notify(Site, Batch)))
clause(18, implies(quarantine(Batch, Evidence), inspection_task(Batch, Evidence, Task)))

// Steps: each goal, what justifies it (a clause, a builtin, a control, an
// absence or a collection), the bindings and the goals it uses.
step(conflicting_sample('handover_a', 'batch_a'), clause(13), {_0: 'handheld_a', Sample: 'handover_a', Batch: 'batch_a', _1: 'handheld', Low: 72, _2: 'logger_a', _3: 'calibrated_logger', High: 94, Limit: 80}, [current_reading('handheld_a', 'handover_a', 'batch_a', 'handheld', 72), current_reading('logger_a', 'handover_a', 'batch_a', 'calibrated_logger', 94), temperature_limit(80), le(72, 80), gt(94, 80)])
step(current_reading('handheld_a', 'handover_a', 'batch_a', 'handheld', 72), clause(12), {Id: 'handheld_a', Sample: 'handover_a', Batch: 'batch_a', Sequence: 43, Sensor: 'handheld', Temperature: 72, Committed: 42}, [observation('handheld_a', 'handover_a', 'batch_a', 43, 'handheld', 72), checkpoint(42), gt(43, 42)])
step(observation('handheld_a', 'handover_a', 'batch_a', 43, 'handheld', 72), clause(6), {}, [])
step(checkpoint(42), clause(1), {}, [])
step(gt(43, 42), 'builtin', {}, [])
step(current_reading('logger_a', 'handover_a', 'batch_a', 'calibrated_logger', 94), clause(12), {Id: 'logger_a', Sample: 'handover_a', Batch: 'batch_a', Sequence: 44, Sensor: 'calibrated_logger', Temperature: 94, Committed: 42}, [observation('logger_a', 'handover_a', 'batch_a', 44, 'calibrated_logger', 94), checkpoint(42), gt(44, 42)])
step(observation('logger_a', 'handover_a', 'batch_a', 44, 'calibrated_logger', 94), clause(7), {}, [])
step(gt(44, 42), 'builtin', {}, [])
step(temperature_limit(80), clause(2), {}, [])
step(le(72, 80), 'builtin', {}, [])
step(gt(94, 80), 'builtin', {}, [])
step(selected_reading('logger_a', 'batch_a', 94), clause(15), {Id: 'logger_a', _0: 'handover_a', Batch: 'batch_a', _1: 'calibrated_logger', Temperature: 94}, [current_reading('logger_a', 'handover_a', 'batch_a', 'calibrated_logger', 94), not(superseded('logger_a'))])
step(not(superseded('logger_a')), 'absent', {}, [])
step(selected_reading('logger_b', 'batch_b', 75), clause(15), {Id: 'logger_b', _0: 'handover_b', Batch: 'batch_b', _1: 'calibrated_logger', Temperature: 75}, [current_reading('logger_b', 'handover_b', 'batch_b', 'calibrated_logger', 75), not(superseded('logger_b'))])
step(current_reading('logger_b', 'handover_b', 'batch_b', 'calibrated_logger', 75), clause(12), {Id: 'logger_b', Sample: 'handover_b', Batch: 'batch_b', Sequence: 45, Sensor: 'calibrated_logger', Temperature: 75, Committed: 42}, [observation('logger_b', 'handover_b', 'batch_b', 45, 'calibrated_logger', 75), checkpoint(42), gt(45, 42)])
step(observation('logger_b', 'handover_b', 'batch_b', 45, 'calibrated_logger', 75), clause(8), {}, [])
step(gt(45, 42), 'builtin', {}, [])
step(not(superseded('logger_b')), 'absent', {}, [])
step(quarantine('batch_a', 'logger_a'), clause(16), {Id: 'logger_a', Batch: 'batch_a', Temperature: 94, Limit: 80}, [selected_reading('logger_a', 'batch_a', 94), temperature_limit(80), gt(94, 80)])
step(notify('north_depot', 'batch_a'), clause(17), {Batch: 'batch_a', _0: 'logger_a', Site: 'north_depot'}, [quarantine('batch_a', 'logger_a'), destination('batch_a', 'north_depot')])
step(destination('batch_a', 'north_depot'), clause(9), {}, [])
step(notify('station_shop', 'batch_a'), clause(17), {Batch: 'batch_a', _0: 'logger_a', Site: 'station_shop'}, [quarantine('batch_a', 'logger_a'), destination('batch_a', 'station_shop')])
step(destination('batch_a', 'station_shop'), clause(10), {}, [])
step(inspection_task('batch_a', 'logger_a', skolem(18, 'Task', ['batch_a', 'logger_a'])), clause(18), {Batch: 'batch_a', Evidence: 'logger_a', Task: skolem(18, 'Task', ['batch_a', 'logger_a'])}, [quarantine('batch_a', 'logger_a')])
step(superseded('handheld_a'), clause(14), {Id: 'handheld_a', Sample: 'handover_a', Batch: 'batch_a', Sensor: 'handheld', _0: 72, _1: 'logger_a', OtherSensor: 'calibrated_logger', _2: 94, Priority: 1, OtherPriority: 2}, [current_reading('handheld_a', 'handover_a', 'batch_a', 'handheld', 72), current_reading('logger_a', 'handover_a', 'batch_a', 'calibrated_logger', 94), sensor_priority('handheld', 1), sensor_priority('calibrated_logger', 2), gt(2, 1)])
step(sensor_priority('handheld', 1), clause(3), {}, [])
step(sensor_priority('calibrated_logger', 2), clause(4), {}, [])
step(gt(2, 1), 'builtin', {}, [])

// Search certificate: derived facts and complete answers used to check
// negations, collections and the original questions.
derived(superseded(A), [superseded('handheld_a')])
derived(current_reading(A, B, C, D, E), [current_reading('handheld_a', 'handover_a', 'batch_a', 'handheld', 72), current_reading('logger_a', 'handover_a', 'batch_a', 'calibrated_logger', 94), current_reading('logger_b', 'handover_b', 'batch_b', 'calibrated_logger', 75)])
searched(superseded('logger_a'), [])
searched(current_reading(F, G, H, I, J), [current_reading('handheld_a', 'handover_a', 'batch_a', 'handheld', 72), current_reading('logger_a', 'handover_a', 'batch_a', 'calibrated_logger', 94), current_reading('logger_b', 'handover_b', 'batch_b', 'calibrated_logger', 75)])
searched(current_reading(K, 'handover_a', 'batch_a', L, M), [current_reading('handheld_a', 'handover_a', 'batch_a', 'handheld', 72), current_reading('logger_a', 'handover_a', 'batch_a', 'calibrated_logger', 94)])
searched(current_reading(K, 'handover_b', 'batch_b', L, M), [current_reading('logger_b', 'handover_b', 'batch_b', 'calibrated_logger', 75)])
searched(superseded('logger_b'), [])

It has four parts:

The claims: the seven answers the proof is about.
The clauses: the program clauses the proof relies on, by number. Each don’t-care _ gets a name (_0, _1, …) so a step can say what it stood for.
The steps: one per thing established. A step reads step(what, by what, with which values, using what).
The search certificate: what eyemind found when it checked that the two selected readings are not superseded, so the checker can verify it.

Three kinds of justification occur:

clause(N): the step is an instance of program clause N, with the variables standing for the values shown.
'builtin': a built-in comparison such as gt(43, 42). It cites no clause and uses nothing; the checker simply calculates it again.
'absent': the step holds because something could not be found. A proof cannot point at a missing thing, so this step leans on the search certificate instead.

Read the steps as sentences:

The handover of batch A is a conflicting sample: by rule 13, with Low = 72, High = 94 and Limit = 80, because of the two current readings below, the limit, and 72 ≤ 80 and 94 > 80.
The handheld reading (7.2°C) is current: by rule 12, because of observation 6, the checkpoint 42 and 43 > 42.
The handheld observation: fact 6.
The checkpoint is 42: fact 1.
43 > 42: a built-in comparison.
The logger reading (9.4°C) is current: by rule 12, because of observation 7, the checkpoint and 44 > 42.
The logger observation: fact 7.
44 > 42: a built-in comparison.
The limit is 80: fact 2.
72 ≤ 80: a built-in comparison.
94 > 80: a built-in comparison.
The logger reading of batch A is selected: by rule 15, because it is current (step 6) and not superseded.
The logger reading of batch A is not superseded: 'absent'; no higher-priority sensor read that sample.
The logger reading of batch B (7.5°C) is selected: by rule 15, because it is current and not superseded.
The logger reading of batch B is current: by rule 12, because of observation 8, the checkpoint and 45 > 42.
The batch B observation: fact 8.
45 > 42: a built-in comparison.
The logger reading of batch B is not superseded: 'absent'.
Batch A is quarantined on the evidence of logger_a: by rule 16, because that reading is selected (step 12), the limit is 80 and 94 > 80 (steps 9 and 11).
North depot is notified about batch A: by rule 17, because batch A is quarantined and goes to north depot.
Batch A goes to north depot: fact 9.
Station shop is notified about batch A: by rule 17, likewise.
Batch A goes to station shop: fact 10.
Batch A has the inspection task skolem(18, 'Task', ['batch_a', 'logger_a']): by rule 18, because batch A is quarantined. Task is bound to the invented name.
The handheld reading is superseded: by rule 14, because the logger read the same sample and the logger’s priority, 2, is higher than the handheld’s, 1.
The handheld has priority 1: fact 3.
The calibrated logger has priority 2: fact 4.
2 > 1: a built-in comparison.

Steps that were already established are reused rather than repeated: the checkpoint (step 4), the limit (step 9) and 94 > 80 (step 11) each appear once. No answer needs steps 25 to 28; they are there because the certificate lists every reading the rules found superseded, and each listed fact must have steps of its own.

The certificate reads:

derived(superseded(A), [superseded('handheld_a')]): the only reading the rules set aside is the handheld one.
derived(current_reading(...), [...]): the three current readings.
searched(superseded('logger_a'), []) and searched(superseded('logger_b'), []): neither logger reading is superseded. The other searched lines record the calls those two searches made: which current readings there are, and which of them belong to the same sample.

Checked: what the report says

A proof is only worth something if someone else can check it. eyemind -c generates the proof and checks it against the program; --check-proof checks a saved proof. The checker never reasons by itself: it only confirms each step against the program. This is the complete report:

// Answers checked subject to the obligations below.
conflicting_sample('handover_a', 'batch_a')
selected_reading('logger_a', 'batch_a', 94)
selected_reading('logger_b', 'batch_b', 75)
quarantine('batch_a', 'logger_a')
notify('north_depot', 'batch_a')
notify('station_shop', 'batch_a')
inspection_task('batch_a', 'logger_a', skolem(18, 'Task', ['batch_a', 'logger_a']))

// C1-C10: resolution, acyclicity, justification, coverage, re-decision,
// boundary consistency, relevance, witness integrity, search closure and call fidelity.
condition('C1', 'resolution', 'ok', 20)
condition('C2', 'well_founded', 'ok', 28)
condition('C3', 'justification', 'ok', 28)
condition('C4', 'coverage', 'ok', 38)
condition('C5', 're_decision', 'ok', 6)
condition('C6', 'boundary_consistency', 'ok', 0)
condition('C7', 'relevance', 'ok', 35)
condition('C8', 'witness_integrity', 'ok', 1)
condition('C9', 'search_closure', 'ok', 2)
condition('C10', 'call_fidelity', 'ok', 0)

// Obligations: absence, collection or original-call evidence remains unproved.
obligation('call_fidelity', 'original_call', conflicting_sample('handover_a', 'batch_a'))
obligation('call_fidelity', 'original_call', selected_reading('logger_a', 'batch_a', 94))
obligation('call_fidelity', 'original_call', selected_reading('logger_b', 'batch_b', 75))
obligation('call_fidelity', 'original_call', quarantine('batch_a', 'logger_a'))
obligation('call_fidelity', 'original_call', notify('north_depot', 'batch_a'))
obligation('call_fidelity', 'original_call', notify('station_shop', 'batch_a'))
obligation('call_fidelity', 'original_call', inspection_task('batch_a', 'logger_a', skolem(18, 'Task', ['batch_a', 'logger_a'])))

// Proof statistics: recorded steps and how they were checked.
steps(28)
verified(20)
recomputed(6)
composed(0)
trusted(7)
claims(7)

// This verdict applies to the claims above; it does not establish completeness.
verdict('checked_with_obligations')

Each condition line names a check, says 'ok', and counts what it looked at:

C1 resolution (20): the 20 clause steps really are instances of the clauses they cite, with the values shown.
C2 well-founded (28): none of the 28 steps depends on itself, even indirectly.
C3 justification (28): all 28 steps say how they were justified, in a form the checker understands.
C4 coverage (38): the 7 claims and the 31 things the steps use are each backed by a step: nothing is taken for granted.
C5 re-decision (6): the 6 comparisons (43 > 42, 44 > 42, 72 ≤ 80, 94 > 80, 45 > 42 and 2 > 1) were calculated again by the checker, and they hold.
C6 boundary consistency (0): no boundary was left to the evidence: C9 settled both absences.
C7 relevance (35): the 7 claims answer the queries, and all 28 steps serve them. There is no padding.
C8 witness integrity (1): the 1 step that invents a name (step 24) was checked: the checker recomputes the Skolem term from rule 18, the variable Task and the values batch A and logger_a, and confirms that the step uses exactly that name.
C9 search closure (2): the 2 absences, “logger_a is not superseded” and “logger_b is not superseded”, were settled by the search certificate, as explained below.

Neither absence is taken on trust. The checker expands superseded('logger_a') one level against the program, as a search would, without searching itself: superseded readings come from forward rule 14, so the call is matched against the derived listing, whose only superseded reading is the handheld one, and that is not the logger. The listing is accepted because its fact has steps of its own and because it is closed: rule 14, run over the listed current readings and the priority facts, supersedes a reading only when a sensor with a higher priority read the same sample, and for handover A it supersedes just the handheld reading, since the logger’s priority, 2, is above the handheld’s, 1. Batch B’s sample has no other reading at all. So the logger readings of batch A and of batch B are not superseded: no higher-priority sensor read the same samples. The claim is about what this program says, not about the world.

The statistics: 28 steps, 20 verified against the program, 6 recomputed and the 2 absences settled by the certificate, no boundary steps trusted. The verdict is checked with obligations: the answers follow from the program. It does not establish that eyemind found every answer.

The supplied priorities express an evidence policy; they do not establish sensor calibration in the real world. Equal priorities can leave multiple readings selected. The program reports actions without executing them.

C10 leaves 7 original-call claims unproved by the available evidence. The verdict is checked with obligations: the recorded derivations are conditional on these call-fidelity obligations. --strict-proof rejects them. The report does not establish answer completeness.

Try it

eyemind examples/cold-chain-recall.js
eyemind --proof examples/cold-chain-recall.js
eyemind -c examples/cold-chain-recall.js

Advance the checkpoint to 44. Only the batch B reading remains in the new tail, so this run derives no quarantine or inspection task. It does not reconstruct decisions from earlier runs.

Give the handheld priority 2, the same as the logger: neither reading supersedes the other, so both selected_reading('handheld_a', 'batch_a', 72) and the logger’s reading are selected. Batch A is still quarantined, on the logger’s evidence. Or lower the logger’s reading from 94 to 79: no reading is above the limit, so there is no conflict, no quarantine and no task.

Takeaway

A recall decision is only as good as the reading it rests on. Writing down which reading counts, and why, makes the decision one you can trace from the thermometer to the notice, and check.