Exercise 3. Two ways to say "not accredited"

An exercise for the negation page. The page’s background-check norm uses not_known: a check is required while nothing is known about accreditation.

Setup. Add a second check norm, with not accredited(p) in the body instead of not_known, and pick cases on which the two norms answer differently. The answers to reach:

Facts	norm with not_known	norm with not
registry	TRUE_ONLY	NEITHER
registry, case record “not accredited”	TRUE_ONLY	TRUE_ONLY
registry, accreditation	NEITHER	NEITHER

Hint. not has no denial source of its own. Who in the package or the case can establish not accredited?

Below is an interactive stub. Fix the second norm and check it on three cases. If JavaScript is off, the solution is shown instead of the editor.

Practicum and solution

Arxo Law

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

entity Person;

relation in_researcher_registry(p: Person) kind institutional;
relation accredited(p: Person) kind institutional;
relation reference_check_required(p: Person) kind institutional;
relation reference_check_on_refusal(p: Person) kind institutional;

rule ReferenceCheck strict {
    for p: Person;
    when in_researcher_registry(p) and not_known(accredited(p));
    then reference_check_required(p);
}

rule ReferenceCheckOnRefusal strict {
    for p: Person;
    when in_researcher_registry(p) and not accredited(p);
    then reference_check_on_refusal(p);
}

The table’s first row is the whole point. With one registry fact the not_known norm fires: indeed nothing is known about accreditation. The not norm stays silent: not accredited must be established, and there is nobody to establish it. The package holds neither a norm with a negative head nor a closure, and the case holds no negative record.

Second row: the negative record is fed by the case, and both norms fire. For not_known, a “not accredited” record is also “no positive record”. Third: accreditation exists, both stay silent.

Check

The table’s three rows execute for each of the two norms on this package.

What the exercise teaches. not P without a denial source never fires, and the compiler will not warn about it: the package is clean, the answer NEITHER. Before writing not in a body, name who produces the denial: a norm with a negative head, a closure from the coming pages, or a case record.