40 Firearm Purchase Example

A person may purchase a firearm only if they hold a valid licence. This example shows how Predica expresses such legality conditions directly as constraints on the FirearmPurchase entity. The constraints are declarative: they state what must be true in any world where a firearm purchase is legally permitted.

entity Person
{
    String name;
    Integer age;
}

entity FirearmLicence
{
    Person holder;
    Boolean valid;
}

entity FirearmPurchase
{
    Person buyer;
    FirearmLicence licence where licence.holder = buyer;

    constraints
    {
        buyer.age ≥ 18;
        licence.valid;
    }
}

When mapped into logic, these constraints become:

// buyer.age ≥ 18
∀B:Person ∀A:Integer
    (this.buyer(B) ∧ B.age(A)) → (A ≥ 18)

// licence.valid
∀L:FirearmLicence ∀V:Boolean
    (this.licence(L) ∧ L.valid(V)) → V

// licence.holder = buyer (from the where constraint)
∀L:FirearmLicence ∀H:Person ∀B:Person
    (this.licence(L) ∧ L.holder(H) ∧ this.buyer(B)) → (H=B)