Exercise 12. A return counts as timely

An exercise for the presumptions and rebuttal page. The archive issue journal is kept by hand, and the archive rules establish: a handover record in the journal means a timely return, unless the record itself implies otherwise.

Setup. Write a presumption with three outcomes. A 20 March handover record with a term to 31 March yields TRUE_ONLY on the timely-return question. A 5 April record with the same term yields FALSE_ONLY: the record itself proves the delay. A 20 March record disputed by the reader yields NEITHER: the presumption is removed, but delay is not proven.

Hint. Rebuttal on the merits and blocking are different unless clauses, and the first must bind every variable it reads.

Below is the solution. Try it yourself first.

Solution

Arxo Law

language "law.core" version "0.2";
package tutorial.archive version "0.10.1";
namespace "urn:law:tutorial:archive";

entity Person;

relation document_lent(p: Person, issued: Date, due: Date) kind empirical { key(p); }
relation journal_return_entry(p: Person, on: Date) kind empirical { key(p); }
relation journal_entry_disputed(p: Person) kind empirical;
relation returned_in_time(p: Person) kind institutional;

The presumption. The first unless rebuts on the merits and says what is established instead; the second only blocks:

Arxo Law

presumption TimelyReturnByJournal {
    for p: Person;
    for issued, due, on: Date;
    when document_lent(p, issued, due) and journal_return_entry(p, on);
    presume returned_in_time(p);
    unless document_lent(p, issued, due) and journal_return_entry(p, on) and on > due
        then not returned_in_time(p);
    unless journal_entry_disputed(p);
}

The document_lent and journal_return_entry repetition in the first unless is no accident: the clause reads due and on, and the compiler requires it to bind them itself. Remove the repetition and you get LDC-E4101.

Check

Facts	Answer on returned_in_time(ivanova)
term to 31 March, handover record 20 March	TRUE_ONLY
term to 31 March, handover record 5 April	FALSE_ONLY
term to 31 March, 20 March record, record disputed	NEITHER
term exists, no handover record	NEITHER

What the exercise teaches. A presumption’s three outcomes are three different claims about the world: “counts”, “the opposite proven”, “does not count, but not refuted either”. A disputed record does not make the return untimely; it merely strips the reader of the presumption, and the question is then settled by evidence.