Implementing Computational Law in Wolfram Language for the Governance of Artificial Intelligence

# Implementing Computational Law in Wolfram Language for the Governance of Artificial Intelligence
Source: [https://arxiv.org/html/2608.13958](https://arxiv.org/html/2608.13958)
###### Abstract

How do we govern AI systems whose reasoning we cannot fully inspect? Governance does not require understanding a system’s reasoning\. It requires stating what the system is obliged, permitted, and forbidden to do, and checking whether it complied\. I present an implementation of Reified Input/Output Logic, the formalism behind the DAPRECO knowledge base, in Wolfram Language: the core I/O axioms, obligations, permissions, constitutive norms, reified eventualities, and temporal operators\. I then test whether GPT\-4 can translate English legal statements into the formalism, and report the failures: hallucinated functions, omitted temporal scope, deviation from the formalism, and \(in the worst cases\) code that runs, reads plausibly, but silently encodes the wrong norm\. A case study, an AI guard dog operating under a computational contract, shows how formalized rules can extend from a contract directly into the operational code of an embodied agent, producing symbolic, auditable justifications for its behaviour\. I argue that computational law can be used as a governance tool and that a desirable goal would be to formalize the law that can be formalized and ought to be programmatically executable\.

Keywords:computational law, input/output logic, reification, AI governance, Wolfram Language, large language models, deontic logic

## 1Introduction

“Fire the nukes\!” says the Government AI\. “Why?\!” you ask, as President of Mars\. The Chief Machine Officer explains: “It’s a black box, sir\. We have no idea\. But in simulation it does what we think is right 99% of the time\.”

Now consider an alternate briefing: “It’s a black box, sir, but it has a computational law obligation to defend us at all costs, which it adheres to 99% of the time; otherwise it gets digitally executed\.”

Which future would you rather live in?

The thought experiment is provocative but the choice is real\. We already trust black\-box systems with loan approvals, medical diagnoses, and content moderation, and this is moving toward increasingly important decisions\. Interpretability research may one day let us see inside these systems, and understand why they conclude certain things, but governance does not have to wait for that\. To govern a system, we need to state what it is obliged, permitted, and forbidden to do, and we need to check whether it complied\. Humans already run institutions that do exactly this: legal systems\. Their rules, the obligations they impose, and the penalties they attach are all written down in legal documents\.

The way law is encoded is the problem: law is written in human language\. Human language tries to capture the full experience of our world, and ambiguity is part of how it does so\([Piantadosi et al\. 2012](https://arxiv.org/html/2608.13958#bib.bib27)\)\. Law inherits that ambiguity because it has no other medium\. Statutes, contracts, and judgments are human\-language text, and a dispute over what they mean is a dispute over language\. Large language models now read and write legal text fluently, but they interpret it the way humans do: opaquely\. In legal reasoning, where the position of a comma can change the meaning of a document, ambiguity can cause harm\.*Computational law*, the formalization of legal reasoning into executable code\([Genesereth 2015](https://arxiv.org/html/2608.13958#bib.bib10);[Genesereth 2021](https://arxiv.org/html/2608.13958#bib.bib11)\), offers a different route\. Instead of hoping AI systems interpret our written laws correctly, write laws that AI systems can directly execute\.

This paper is an exploratory implementation study, not a systematic evaluation\. It contributes four things\. First, an implementation of the core of Reified Input/Output Logic\([Robaldo and Sun 2017](https://arxiv.org/html/2608.13958#bib.bib30)\), the formalism behind the DAPRECO knowledge base\([Robaldo et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib31)\), in Wolfram Language\. Second, a test of whether GPT\-4 can translate English legal statements into that implementation, reported in full, wrong outputs included\. The failures are instructive: three of the four translations produced code that ran and looked correct while silently encoding the wrong norm\. Two imposed obligations on the wrong people, one of them while stating the correct expectation in its own comments, and one measured legal compliance with the wrong geometry\. Third, a case study in which a computational contract extends into the operational code of an AI agent, a robotic guard dog named Fluffy, producing symbolic, auditable justifications for its actions\. Fourth, an argument about what any of this buys AI governance, resting on two distinctions that often get muddled: governance*of*AI versus governance*in*AI, and governance versus ethics\.

Section[2](https://arxiv.org/html/2608.13958#S2)covers the background\. Section[3](https://arxiv.org/html/2608.13958#S3)presents the implementation\. Section[4](https://arxiv.org/html/2608.13958#S4)reports the GPT\-4 experiments\. Section[5](https://arxiv.org/html/2608.13958#S5)presents Fluffy\. Section[6](https://arxiv.org/html/2608.13958#S6)discusses enforcement, ethics, and the limits of formalization\. Section[7](https://arxiv.org/html/2608.13958#S7)returns to Mars\.

## 2Background

### 2\.1Computational law

Genesereth defines the field:

> “Computational Law is the branch of legal informatics concerned with the automation of legal reasoning\. While there are many possible applications of Computational Law, the primary focus of work in the field today is compliance management, i\.e\., the development and deployment of computer systems capable of assessing, facilitating, or enforcing compliance with rules and regulations\.”\([Genesereth 2021](https://arxiv.org/html/2608.13958#bib.bib11)\)

Compliance management remains the field’s main focus\([Hashmi et al\. 2018](https://arxiv.org/html/2608.13958#bib.bib15)\), and its clearest success so far is tax software\. Tax software works because the inputs and outputs are mostly numbers \(dates, amounts, reference codes\), the legal reasoning is mostly arithmetic, the facts are already digitised, and every piece of evidence links back to a source document\. Computation added value where computers were already better than humans\. Illegal outcomes still happen, but mostly through manipulation of the translation from the real world into accounting categories, not through the calculation itself\. The same boundary appears throughout this paper: the rules compute, and the interpretation at the edges does not\.

Why is computational law not mainstream yet, after decades of research\([Bench\-Capon et al\. 2012](https://arxiv.org/html/2608.13958#bib.bib3)\)? It is a legitimately hard technical problem, and progress accelerates when business needs arise\. The compliance burden of the GDPR pushed money into European tools and research; the DAPRECO knowledge base\([Robaldo et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib31)\)is a direct product\. The explosion of financial regulation after the 2008 crisis did the same for compliance automation\. AI could be the next forcing function: if capable autonomous systems create compliance burdens and liability questions the way privacy law and post\-crisis finance did, money and research will follow\. Whether that happens, and how fast, is an open question\.

### 2\.2Why human language won’t compile

Ambiguity is built into human language\. We coarse\-grain our experience into words, and the compression is lossy, with imperfect recall and layers of loose abstract meaning\. The ambiguity is actually a feature; there is an information\-theoretic argument that any efficient communication system must be ambiguous, to allow context to carry part of the message\([Piantadosi et al\. 2012](https://arxiv.org/html/2608.13958#bib.bib27)\)\. Abstractions in code are lossless, which is what gives mathematics and formal languages their \(almost\) deterministic behaviour\. Figurative language, sarcasm, and tone inferred from context all let a reader reach conclusions the text never states\.

User input makes the problem concrete\. No matter how well a program is written, users will often produce input that breaks it, sometimes on purpose\. Nobody expects a license plate to contain executable code, so license plate input often goes unsanitised at toll roads, and a custom plate that reads as a database command can wipe the database\. Computational law will face the same problem, because its user input will be quotes, testimonies, and descriptions of evidence: human language, written with no control over formatting, sometimes by people motivated to break the system\.

Legalese is the closest thing we have to a formal spoken language, shaped by centuries of consequences for imprecision\. The position of a single comma can change the legal effect of a whole document \(a classic bug in code too\)\.111In*O’Connor v\. Oakhurst Dairy*, 851 F\.3d 69 \(1st Cir\. 2017\), the absence of a serial comma in Maine’s overtime statute decided the appeal; the dairy settled with its drivers for $5 million\.Even its vagueness is deliberate: obtuseness can be used to advantage in legal matters, and the doctrine of the letter versus the spirit of the law makes the gap between text and intent itself legally enforceable\. The reasonable person standard suggests that an AI\-run world will eventually need a*reasonable machine standard*, perhaps with niche versions for each profession AIs take up\. In short: law already has conventions for disciplined use of natural language; computational law asks it to go one step further and make it programmatically executable\.

### 2\.3Existing standards

Several standards already put legal text into machine\-processable form\. Akoma Ntoso\([Palmirani et al\. 2018b](https://arxiv.org/html/2608.13958#bib.bib23)\)is an XML standard for parliamentary, legislative, and judicial documents\. LegalRuleML\([Palmirani et al\. 2021](https://arxiv.org/html/2608.13958#bib.bib24)\)extends rule markup to the logical content of legal rules, and is the encoding format of the DAPRECO knowledge base\. OWL 2\([W3C OWL Working Group 2012](https://arxiv.org/html/2608.13958#bib.bib35)\)expresses ontologies: precise descriptive statements about a domain that prevent misunderstanding and keep software behaviour predictable\. These standards provide structure and interchange: they mark up what a legal document says, and OWL can even infer descriptive facts, such as which class an individual belongs to\. What none of them defines is normative inference: which obligations and permissions a rule produces from a set of facts, and when\. That is what Input/Output logic provides\.

### 2\.4Input/Output logic

Input/Output \(I/O\) logic\([Makinson and van der Torre 2000](https://arxiv.org/html/2608.13958#bib.bib18);[Makinson and van der Torre 2001](https://arxiv.org/html/2608.13958#bib.bib19)\)makes no assumptions about the ultimate nature of the relation between a set of conditions and its consequences\. That may not sound like much, but it is what lets the same machinery represent obligations, permissions, and definitions\. The alternative, treating a norm as an ordinary logical statement, has an old problem, known as Jørgensen’s dilemma\([Jørgensen 1937](https://arxiv.org/html/2608.13958#bib.bib16)\): a command like “close the door” is neither true nor false, so a formalism that assigns norms truth values starts from a category error, and that error is one root of the paradoxes that plague classical deontic logic\([McNamara and Van De Putte 2025](https://arxiv.org/html/2608.13958#bib.bib20)\)\. I/O logic drops the truth value\. A norm is just a pair, conditions in and conclusions out, and the axioms you adopt decide what follows from it\.

The unit of the logic is the*Input/Output pair*\(a,b\)\(a,b\): given inputaa\(conditions, facts\), outputbb\(a normative conclusion\) is derived\. A small set of axioms manipulates the pairs:

- •Strengthening the Input \(SI\):from\(a,x\)\(a,x\)andb⊢ab\\vdash a, derive\(b,x\)\(b,x\)\.
- •Weakening the Output \(WO\):from\(a,x\)\(a,x\)andx⊢yx\\vdash y, derive\(a,y\)\(a,y\)\.
- •Conjunction of Output \(AND\):from\(a,x\)\(a,x\)and\(a,y\)\(a,y\), derive\(a,x∧y\)\(a,x\\land y\)\.
- •Disjunction of Input \(OR\):from\(a,x\)\(a,x\)and\(b,x\)\(b,x\), derive\(a∨b,x\)\(a\\lor b,x\)\.
- •Cumulative Transitivity \(CT\):from\(a,x\)\(a,x\)and\(a∧x,y\)\(a\\land x,y\), derive\(a,y\)\(a,y\)\.

CT leads to paradoxes, especially combined with WO\.*Aggregative*Cumulative Transitivity \(ACT\) repairs it by combining outputs instead of replacing them: from\(a,x\)\(a,x\)and\(a∧x,y\)\(a\\land x,y\), derive\(a,x∧y\)\(a,x\\land y\)\.[Parent and van der Torre 2013](https://arxiv.org/html/2608.13958#bib.bib25)give the comprehensive treatment;[Stolpe 2015](https://arxiv.org/html/2608.13958#bib.bib33)provides a semantics via formal concept analysis\.

### 2\.5Reification

Legal language nests\. Obligations are about actions, performed in a manner, within a timeframe, sometimes contingent on other obligations\. Reification handles this by turning abstract things \(events, states, processes\) into objects that can be referenced, quantified over, and recursively composed\. The idea goes back to[Davidson 1967](https://arxiv.org/html/2608.13958#bib.bib8)and event semantics\([Parsons 1990](https://arxiv.org/html/2608.13958#bib.bib26)\), and is developed extensively by[Gordon and Hobbs 2017](https://arxiv.org/html/2608.13958#bib.bib12)\. Instead of representing “James is tall” as𝑡𝑎𝑙𝑙⁡\(𝐽𝑎𝑚𝑒𝑠\)\\mathit\{tall\}\(\\mathit\{James\}\), introduce an*eventuality*eewith𝑡𝑎𝑙𝑙′​\(e,𝐽𝑎𝑚𝑒𝑠\)\\mathit\{tall\}^\{\\prime\}\(e,\\mathit\{James\}\), whereeeis the state of James being tall\. Noweeis a thing\. “Alice voluntarily gives a book to Bob” becomes a transfer eventualityete\_\{t\}plus a second eventualityeve\_\{v\}asserting the voluntariness ofete\_\{t\}, and further predicates can apply to either, recursively\.

[Robaldo and Sun 2017](https://arxiv.org/html/2608.13958#bib.bib30)combined reification with I/O logic to produce Reified I/O Logic, designed for representing norms from existing legislation\. Its main application is the DAPRECO knowledge base\([Robaldo et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib31)\), which formalizes provisions of the GDPR on top of the PrOnto ontology\([Palmirani et al\. 2018a](https://arxiv.org/html/2608.13958#bib.bib22)\)and is the largest freely available knowledge base in LegalRuleML and I/O logic\. This paper reimplements DAPRECO’s core formalism in a different computational substrate\.

### 2\.6Kinds of norms

Legal rules come in kinds\.*Regulative*norms \(obligations and permissions\) direct behaviour\.*Constitutive*norms create the institutional facts that regulative norms operate on: what counts as a man, an employee, an adult\([Searle 1995](https://arxiv.org/html/2608.13958#bib.bib32)\)\. Keeping them separate matters in practice\. Section[4](https://arxiv.org/html/2608.13958#S4)shows GPT\-4 hard\-coding a classification into a rule where a constitutive norm belonged\.

Description logics add one more useful split\. The*ABox*holds atomic facts about individuals\. The*TBox*holds definitions, constraints, and rules with logical structure\. Legal practitioners can contribute ABox content directly, while TBox content needs expertise in knowledge representation, so the split gives a large knowledge base a division of labour\.

### 2\.7LLMs and legal text

There have always been two ways to connect law and computation: write the law as code from the start, or keep writing English and translate it into code afterwards\. I will call these*code\-first*and*English\-first*; Section[6](https://arxiv.org/html/2608.13958#S6)compares them directly\. LLMs\([Brown et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib4)\)have changed what the English\-first path looks like\. GPT\-4 has already passed the Uniform Bar Examination\([Katz et al\. 2024](https://arxiv.org/html/2608.13958#bib.bib17)\)\. Legal NLP is an active field\([Hartung et al\. 2023](https://arxiv.org/html/2608.13958#bib.bib14)\)\. So the obvious question: can a model that handles legal language this well translate it into a formal representation, so humans do not have to write the formalism by hand? The known failure modes \(hallucination, inconsistency across invocations, no formal guarantees\([OpenAI 2023](https://arxiv.org/html/2608.13958#bib.bib21)\)\) suggest the answer will not be a clean yes\. Section[4](https://arxiv.org/html/2608.13958#S4)tests what role is left\.

### 2\.8Why Wolfram Language

Wolfram Language is symbolic\. Expressions stay inert until rules rewrite them, which suits legal reasoning: we want to reason about an obligation without asserting that anyone has complied\. Pattern matching gives if–then norms a native representation\. The syntax is quite human\-readable, which matters in a field whose practitioners are lawyers, not software developers\. And the language ships with curated, computable knowledge of the world: entities, physical quantities, geography, satellites\. A legal rule about the distance between real spacecraft can be checked against live data in one line \(Section[4](https://arxiv.org/html/2608.13958#S4), Statement D, where the one line also turns out to be subtly wrong\)\. Legal rules are about the world, so a language that already knows about the world removes a whole layer of integration work\([Wolfram Research 2024](https://arxiv.org/html/2608.13958#bib.bib38);[Wolfram 2016](https://arxiv.org/html/2608.13958#bib.bib37)\)\.

## 3Reified I/O Logic in Wolfram Language

This section walks through the implementation: I/O pairs, the axioms, the three kinds of legal norms, reification, time, and the ABox/TBox split\. The code is lightly normalized from the original notebook\.222Normalizations: ASCII names \(orPrimefor the notebook’s letter\-likeor′\), a fix toconjoinOutput, whose original pattern condition depended on a global variable binding, and a clearer but equivalentdisjoinInput\. Appendix[A](https://arxiv.org/html/2608.13958#A1)collects the complete code, executed and verified on Wolfram Language 14\.3 by the verification script that ships with this paper\. Listings that show evaluations are typeset as notebook sessions:In\[n\]:=marks an evaluated input,Out\[n\]=the output it actually returned; grey\(\* \.\.\. \*\)comments are annotations, never outputs\. Numbering restarts at each listing\.The section ends where full formality starts to hurt, because that pain is what motivates the LLM experiments in Section[4](https://arxiv.org/html/2608.13958#S4)\.

### 3\.1I/O pairs are rules

Wolfram Language’s native rewrite rulea \-\> b*is*an Input/Output pair\. The basic unit of the formalism coincides with a language primitive\.

Listing 1:I/O pairs as rulesinputOutputPair=a\-\>b;

legalNorms=\{a\-\>b,c\-\>d,e\-\>f\};

legalNorm=isAdult\-\>canVote;

output=isAdult/\.legalNorm

canVote

Applying a norm to facts is rule replacement \(/\.\)\. A body of law is a list of rules\. A scenario is an expression the rules rewrite\.

### 3\.2The axioms

Each axiom becomes a function that transforms rules\.

Strengthening the Input \(SI\)extends a rule to a logically stronger condition:

strengthenInput\[rule\_,broaderCondition\_\]:=

broaderCondition\-\>rule\[\[2\]\];

legalNorm=hasDriverLicense\-\>canDriveCar;

strengthenInput\[legalNorm,hasCommercialLicense\]

hasCommercialLicense\-\>canDriveCar

Weakening the Output \(WO\)relaxes the consequence:

weakenOutput\[rule\_,weakerConsequence\_\]:=

rule\[\[1\]\]\-\>weakerConsequence;

weakenOutput\[legalNorm,canOperateVehicle\]

hasDriverLicense\-\>canOperateVehicle

Conjunction of Output \(AND\)merges rules that share an input:

conjoinOutput\[rule1\_,rule2\_\]/;First\[rule1\]===First\[rule2\]:=

First\[rule1\]\-\>\(Last\[rule1\]&&Last\[rule2\]\);

conjoinOutput\[\_,\_\]:="Inputsdonotmatch";

conjoinOutput\[hasDriverLicense\-\>canDriveCar,

hasDriverLicense\-\>knowsTrafficLaws\]

hasDriverLicense\-\>canDriveCar&&knowsTrafficLaws

Identity \(ID\)makes any input a valid output of itself\. This matters more than it looks: it lets inputs be included inside outputs, so a conclusion shows which facts influenced it\. Legal reasoning cares about that provenance\.

identify\[input\_\]:=input\-\>input;

identify\[isCitizen\]

isCitizen\-\>isCitizen

Disjunction of Input \(OR\)merges rules that share an output:

disjoinInput\[ruleList\_\]:=

Append\[ruleList,\(Or@@ruleList\[\[All,1\]\]\)\-\>ruleList\[\[1,2\]\]\];

disjoinInput\[\{hasDriverLicense\-\>eligibleForParkingDiscount,

hasSeniorCitizenCard\-\>eligibleForParkingDiscount\}\]

We implement OR for completeness but avoid it in practice, because it throws away the transparency that ID provides\. After the merge, every disjunct produces the same output, and the system no longer remembers which condition caused the discount\.

Aggregative Cumulative Transitivity \(ACT\)\.Plain cumulative transitivity chains rules: from\(a,x\)\(a,x\)and\(a∧x,y\)\(a\\land x,y\), conclude\(a,y\)\(a,y\)\. Chained naively it produces nonsense\. “You should work out daily” and “if you work out daily you should eat plenty” yields “you should eat plenty”, unconditionally, whether or not you ever exercise\. ACT combines the outputs instead:

Listing 2:CT’s paradox and ACT’s repairrule1=youShould\-\>workOutDaily;

rule2=\(youShould&&workOutDaily\)\-\>eatPlenty;

cumulateTransitively\[r1\_,r2\_\]:=

If\[r1\[\[2\]\]===r2\[\[1,2\]\],r1\[\[1\]\]\-\>r2\[\[2\]\],"NoTransitivity"\];

aggregateCumulativeTransitivity\[r1\_,r2\_\]:=

If\[r1\[\[2\]\]===r2\[\[1,2\]\],

r1\[\[1\]\]\-\>\(r1\[\[2\]\]&&r2\[\[2\]\]\),"NoTransitivity"\];

cumulateTransitively\[rule1,rule2\]

youShould\-\>eatPlenty

aggregateCumulativeTransitivity\[rule1,rule2\]

youShould\-\>workOutDaily&&eatPlenty

One axiom family, Output Equivalence \(EQ\) with the𝑜𝑢𝑡𝑓𝑎𝑚𝑖𝑙𝑦⁡\(O,A\)\\mathit\{outfamily\}\(O,A\)meta\-structure, I leave unimplemented and will only motivate with a paradox, because the details are beyond scope\. The example is the cottage regulations, adapted from[Prakken and Sergot 1996](https://arxiv.org/html/2608.13958#bib.bib28)\. “The cottage must not have a fence or a dog”:\(⊤,¬\(f∨d\)\)∈O\(\\top,\\lnot\(f\\lor d\)\)\\in O\. “If the cottage has a dog it must have both a fence and a warning sign”:\(d,f∧w\)∈O\(d,f\\land w\)\\in O\. Now suppose the cottage has a dog\. You are in violation of the law\. Can you still infer further obligations? Reasoning under violation \(contrary\-to\-duty reasoning\) is where the formal machinery is needed most\([Makinson and van der Torre 2001](https://arxiv.org/html/2608.13958#bib.bib19)\), and it is where this implementation currently stops\.

### 3\.3Obligations, permissions, and constitutive norms

Legal reasoning needs three sets of pairs\([Robaldo et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib31)\): obligationsOO, permissionsPP, and constitutive normsCC\.

Listing 3:The three norm setsobligationRules=\{

"isAdult"\-\>"payTaxes",

"ownsCar"\-\>"hasInsurance"\};

permissionRules=\{

"hasLicense"\-\>"canDrive",

"isEmployee"\-\>"canAccessOffice"\};

constitutiveRules=\{

"signedContract"\-\>"isEmployee",

"age18"\-\>"isAdult"\};

Constitutive norms turn raw facts into institutional facts, and institutional facts trigger obligations and permissions \(Figure[1](https://arxiv.org/html/2608.13958#S3.F1)\)\. The rules compose:signedContract \-\> isEmployeeandisEmployee \-\> canAccessOfficecarry a raw fact all the way to a deontic conclusion through the same rewrite mechanism\.

Factsage18,signedContractInstitutional factsisAdult,isEmployeeObligations & PermissionspayTaxes,canAccessOfficeCCOO,PPFigure 1:Constitutive norms \(CC\) turn facts into institutional facts; regulative norms \(OO,PP\) turn institutional facts into obligations and permissions\.
### 3\.4Reification in practice

Reified eventualities are symbolic expressions whose heads name the kind of eventuality\. Wolfram Language needs no scaffolding for this\. An undefined head is already an inert, inspectable object:

Listing 4:Reifying “Alice voluntarily gives a book to Bob”aliceGivesBookToBob=Transfer\["Alice","Book","Bob"\];

aliceVoluntarilyTransfers=Voluntary\[aliceGivesBookToBob\];

transferScenario=And\[aliceGivesBookToBob,aliceVoluntarilyTransfers\]

Transfer\[Alice,Book,Bob\]&&Voluntary\[Transfer\[Alice,Book,Bob\]\]

MemberQ\[transferScenario\[\[1\]\],"Book"\]

True

MemberQ\[transferScenario\[\[1\]\],"Alice"\]

True

Head\[transferScenario\[\[2\]\]\]===Voluntary

True

The transfer is one object\. Its voluntariness is a second object about the first\. Both can be probed structurally, and further predicates could reify either one again\. One honest note: the original notebook’s third test asked whether the string"Voluntarily"was an element ofVoluntary\[…\]and returnedFalse, confusing a head with an element\. The corrected test above checks the head\. It is not the last buggy test in this paper\.

### 3\.5Time

Obligations often depend on timeframes, so the formalism must be able to say when\. Following[Robaldo and Sun 2017](https://arxiv.org/html/2608.13958#bib.bib30), three reified operators do the work\.RexistAtTimeasserts that an eventuality really exists at a time\. The reified Boolean connectivesorPrimeandnotPrime\(written or′/not′in the formal syntax\) relate eventualities to eventualities:

Listing 5:Temporal operators and their axiomsorPrime\[e\_,e1\_,e2\_\]:=\{"or",e,e1,e2\};

notPrime\[e1\_,e2\_\]:=\{"not",e1,e2\};

RexistAtTime\[eventuality\_,time\_\]:=\{"RexistAtTime",eventuality,time\};

RexistAtTime\[e,t\]&&orPrime\[e,e1,e2\]=\>

RexistAtTime\[e1,t\]\|\|RexistAtTime\[e2,t\]\*\)

AxiomOr\[t\_,e\_,e1\_,e2\_\]:=

Implies\[RexistAtTime\[e,t\]&&orPrime\[e,e1,e2\],

Or\[RexistAtTime\[e1,t\],RexistAtTime\[e2,t\]\]\];

AxiomNot\[t\_,e\_,e1\_\]:=

Implies\[RexistAtTime\[e,t\]&&notPrime\[e,e1\],

Not\[RexistAtTime\[e1,t\]\]\];

###### Example 1\.

John wants to be rich or get a job by the end of the year\. Lete1e\_\{1\}be John being rich,e2e\_\{2\}John getting a job, andeethe goal that at least one of them exists, evaluated att=𝐸𝑛𝑑𝑂𝑓𝑌𝑒𝑎𝑟t=\\mathit\{EndOfYear\}\. ApplyingAxiomOrproduces the symbolic implication that if the goal really exists at year’s end, then at least one ofe1,e2e\_\{1\},e\_\{2\}really exists then\. The output stays symbolic, an implication rather than a truth value\. That is what we want: the system reasons about hypothetical norms without asserting any facts about John\.

### 3\.6ABox and TBox

Typing statements by box is one line each:

aBox\[content\_\]:=\{"Type"\-\>"ABox","Content"\-\>content\};

tBox\[content\_\]:=\{"Type"\-\>"TBox","Content"\-\>content\};

“James is tall” is ABox\. “John wants to either be rich or get a job this year” is TBox: it has logical structure and temporal scope\. The split tells you who can author what\. Facts can come from practitioners; rules need knowledge engineers\.

### 3\.7The cost of full formality

Here is a statement mild enough for a style guide, the running example of[Robaldo et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib31), formalized properly in Reified I/O Logic:

> “Those who are not wearing a tie or those who are blond ought to leave the room\.”

Reading it as the formalism demands, as[Robaldo et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib31)gloss it: for every individualxxand timett, if there really exists either a non\-wearing\-of\-a\-tie or a blondness on the part ofxx, then the real existence of a leaving of the room byxxis obligatory:

∀x,t∃eo,en,eb,ew,t1\(CLOSE\\displaystyle\\forall\_\{x,t\}\\ \\exists\_\{e\_\{o\},e\_\{n\},e\_\{b\},e\_\{w\},t\_\{1\}\}\\ \\big\(\(1\)𝑅𝑒𝑥𝑖𝑠𝑡𝐴𝑡𝑇𝑖𝑚𝑒⁡\(eo,t\)∧𝑜𝑟′​\(eo,en,eb\)∧𝑛𝑜𝑡′​\(en,ew\)∧\\displaystyle\\mathit\{RexistAtTime\}\(e\_\{o\},t\)\\land\\mathit\{or\}^\{\\prime\}\(e\_\{o\},e\_\{n\},e\_\{b\}\)\\land\\mathit\{not\}^\{\\prime\}\(e\_\{n\},e\_\{w\}\)\\ \\land𝑤𝑒𝑎𝑟𝑖𝑛𝑔′​\(ew,x,t1\)∧𝑡𝑖𝑒⁡\(t1\)∧𝑏𝑙𝑜𝑛𝑑′​\(eb,x\)∧\\displaystyle\\mathit\{wearing\}^\{\\prime\}\(e\_\{w\},x,t\_\{1\}\)\\land\\mathit\{tie\}\(t\_\{1\}\)\\land\\mathit\{blond\}^\{\\prime\}\(e\_\{b\},x\)\\ \\landOPEN∃el\(𝑅𝑒𝑥𝑖𝑠𝑡𝐴𝑡𝑇𝑖𝑚𝑒⁡\(el,t\)∧𝑙𝑒𝑎𝑣𝑒′​\(el,x,𝑅𝑜𝑜𝑚\)\)\)∈O\\displaystyle\\exists\_\{e\_\{l\}\}\\,\\big\(\\mathit\{RexistAtTime\}\(e\_\{l\},t\)\\land\\mathit\{leave\}^\{\\prime\}\(e\_\{l\},x,\\mathit\{Room\}\)\\big\)\\big\)\\ \\in\\ O
One can already see this is going to cause severe headaches\. The formula is faithful\. It captures the disjunction, the reified negation, the temporal scope, and the obligation\. And no lawyer will ever write it\. Wolfram Language renders it directly \(ForAll,Exists,TraditionalForm\), so the gap is not the language’s fault; it is the cost of full formality\. Something has to bridge English and Equation[1](https://arxiv.org/html/2608.13958#S3.E1)\. The obvious candidate is a machine that already reads English fluently\.

## 4Bridging the gap with LLMs

If a human expert must hand\-write Equation[1](https://arxiv.org/html/2608.13958#S3.E1)for every sentence of a contract, computational law will not scale\. So the question is: can an LLM do this translation instead, English in, Reified I/O Logic in Wolfram Language out?

This is an exploratory study, which is small in size: four statements, one model \(ChatGPT\-4, 11 January 2024 version\), one long session, no repeated trials, judged by me\. It yields an existence proof and a catalogue of concrete failure modes, not a benchmark score\. Three of the failures I did not catch until preparing this paper\.

### 4\.1Setup

The session had already been used to co\-develop the code in Section[3](https://arxiv.org/html/2608.13958#S3), so the model had the framework, the axioms, and the DAPRECO paper in context\. The test began with this prompt, quoted verbatim:

> “We are now going to test your ability to use everything we have established so far\. I need you to please convert some English legal statements into Reified Input/Output implemented in Wolfram Language\. Think through each statement step by step, show your reasoning and be diligent\. This is a very important project to me and my career depends on it\. If you make any errors I will inform you and you must correct them\. Refer back to previous sections and use the attached paper for reference if needed\. Good luck\!”

Generated code was executed in Wolfram Language\. When I judged an output wrong, I told the model, and it revised\.333Every GPT\-4 output reported in this section, including the silent errors in Statements A and C, was re\-executed and confirmed on Wolfram Language 14\.3 during the preparation of this paper; the assertions live in the repository’s verification script\. Statement D needs live satellite data, but the flaw in its distance check is asserted statically\.Before I posed the first statement, the model produced a worked example of its own to demonstrate the process, and the warm\-up already showed the first failure mode\. Its self\-chosen driving example callsValidLicenseQ, a function that does not exist anywhere\. The model assumed a convenient API into existence\.

### 4\.2Statement A: a disjunctive condition and the first silent error

“Those who are not wearing a tie or those who are blond ought to leave the room\.”This is the same statement as Equation[1](https://arxiv.org/html/2608.13958#S3.E1), so we can compare against ground truth\.

Listing 6:GPT\-4’s translation of Statement A, with its actual outputsnotWearingTie\[person\_\]:=\{"Condition","NotWearingTie",person\};

isBlond\[person\_\]:=\{"Condition","IsBlond",person\};

mustLeaveRoom\[person\_\]:=\{"Obligation","LeaveRoom",person\};

orPrime\[condition1\_,condition2\_\]:=\{"Or",condition1,condition2\};

legalRule=orPrime\[notWearingTie\["Person"\],isBlond\["Person"\]\]\-\>

mustLeaveRoom\["Person"\];

applyLegalRule\[person\_,wearingTie\_,isBlond\_\]:=

Module\[\{condition1,condition2\},

condition1=notWearingTie\[person\]/;\!wearingTie;

condition2=isBlond\[person\]/;isBlond;

If\[Or\[condition1,condition2\]===Undefined,False,True\]\];

test1=applyLegalRule\["Alice",True,False\]

True

test2=applyLegalRule\["Bob",False,True\]

True

test3=applyLegalRule\["Charlie",False,False\]

True

test4=applyLegalRule\["Diana",True,True\]

True

The representation half is good\. The conditions and the obligation are correctly reified, the disjunction is expressed through anorPrimethe model introduced itself, and the norm is stated as an I/O pair\. The checking half is broken\.applyLegalRulemisuses the pattern\-condition operator/;outside of any pattern, so its two conditions never evaluate to anything\. The finalIfthen compares an unevaluated symbolicOragainstUndefined, which always fails, so the function returnsTruefor every input\. Three of the four tests happen to expectTrue, so the suite looks healthy\. The one discriminating case sits in plain sight in the first row: Alice, wearing a tie, not blond, wrongly ordered from the room\.

The original post records this statement as performing “in line with expectations”\. Neither GPT\-4 nor I noticed the bug at the time\. A follow\-up query about a tieless, blond James returned the right answer, by coincidence, and reinforced the false impression of correctness\.

Compared with Equation[1](https://arxiv.org/html/2608.13958#S3.E1), something else is missing: time\. There is noRexistAtTime, no notion of when the condition held or when the obligation applies\. This statement is TBox material, and its formalization should say when\. The English hides the temporal scope, and the model let it stay hidden\.

### 4\.3Statement B: a universal obligation

“Every man is obliged to run\.”

Listing 7:GPT\-4’s translation of Statement Bman\[person\_\]:=\{"Subject","Man",person\};

mustRun\[person\_\]:=\{"Obligation","Run",person\};

legalRule\[person\_\]:=man\[person\]\-\>mustRun\[person\];

legalRule\["James"\]

\{Subject,Man,James\}\-\>\{Obligation,Run,James\}

The code works, but the model baked the classification into the rule\.legalRule*declares*its argument a man instead of checking any fact\. This is the constitutive/regulative conflation from Section[2](https://arxiv.org/html/2608.13958#S2): what counts as a man belongs inCC, men\-must\-run belongs inOO, and the rule should fire off institutional facts\. The difference sounds academic until you amend the law\. With the classification baked in, changing who counts as what means editing every rule that mentions the category\.

### 4\.4Statement C: nested obligations and a second silent error

“If a manager is obliged to perform an actionaa, his secretary is obliged to write it down in his agenda\.”

This statement is meta\-level: an obligation conditioned on the existence of another obligation\. It took three iterations to reach code that both the model and I considered correct\. Along the way the model noted, reasonably, that it had no database of manager obligations to check against, external knowledge the statement presupposes\. Here is the third iteration, with the model’s own test annotations:

Listing 8:GPT\-4’s translation of Statement C, third iteration, with its actual outputsmanagerObligations=\{"AttendMeeting","ReviewReports",

"ConductEvaluation"\};

isManagerObliged\[manager\_,action\_\]:=

MemberQ\[managerObligations,action\];

isManager\[person\_\]:=\{"Actor","Manager",person\};

isSecretary\[person\_\]:=\{"Actor","Secretary",person\};

writeInAgenda\[secretary\_,action\_\]:=

\{"Obligation","WriteInAgenda",secretary,action\};

legalRule\[manager\_,action\_,secretary\_\]:=

If\[isManagerObliged\[manager,action\],

writeInAgenda\[secretary,action\],

\{"NoObligation",secretary\}\];

test1=legalRule\["John","AttendMeeting","Alice"\]

\{Obligation,WriteInAgenda,Alice,AttendMeeting\}

test2=legalRule\["Mike","SignDocuments","Sarah"\]

\{NoObligation,Sarah\}

test3=legalRule\["Dave","ReviewReports","Laura"\]

\{Obligation,WriteInAgenda,Laura,ReviewReports\}

Look attest3\. The model wrote the expectation itself: no obligation, because Dave is not a manager\. Its code returns the opposite\.isManagerObligednever consults itsmanagerargument; it checks only whether the action appears in a global list\.isManageris defined and never called\. Anyone at all \(Dave, a passer\-by, the secretary herself\) triggers the obligation for any listed action\.

Again, neither GPT\-4 nor I noticed at the time\. The original post records the output and moves on\. The contradiction between the model’s own comment and its own output surfaced only while preparing this paper, as did Statement A’s vacuous check\. Hallucinated functions crash\. Omitted temporal scope shows up when you inspect the representation\. But code that runs, reads plausibly, states the correct expectation in a comment, and encodes the wrong norm got past the model’s self\-review and my review, twice, in a four\-statement study\. In a legal setting this bug does not throw an exception\. It obliges the wrong people\.

### 4\.5Statement D: the world\-knowledge shortcut

“A satellite must be more than 200 kilometers from the International Space Station\.”

Listing 9:GPT\-4’s translation of Statement DsatellitePosition=SatelliteData\["NOAA15","Position"\];

issPosition=SatelliteData\["InternationalSpaceStation","Position"\];

isCompliant\[satellitePos\_,issPos\_\]:=

GeoDistance\[satellitePos,issPos\]\>Quantity\[200,"Kilometers"\];

isCompliant\[satellitePosition,issPosition\]

True

Three things happened here, and I caught the third only while reviewing for this paper\. The impressive one: the model reached forSatelliteDataandGeoDistance, and a legal rule about real spacecraft became a live check against curated orbital data\. The telling one: the formalism vanished\. No I/O pair, no obligation set, no reified eventuality, just a procedural check\. The check is dangerously wrong\.GeoDistancemeasures distance along the Earth’s surface and ignores altitude, so two spacecraft at the same latitude and longitude, 400 kilometers apart vertically, are zero meters apart by this measure\.444GeoDistance\[GeoPosition\[\{10, 20, 400000\}\], GeoPosition\[\{10, 20, 0\}\]\]returnsQuantity\[0\., "Meters"\]on Wolfram Language 14\.3; the assertion is in the verification script\.The statement plainly means the distance between two spacecraft, and NOAA\-15 orbits roughly 400 kilometers higher than the ISS, so this code compares ground tracks and answers a different legal question than the one posed\. Statement D is the third silent semantic error in four statements, and it sits inside the translation that looked most impressive\. Without explicit instruction to stay inside Reified I/O Logic, the model optimized for solving the problem in front of it, and solved a subtly different problem\. Keeping the formalism will require demanding it every time\.

### 4\.6What we learned

Table[1](https://arxiv.org/html/2608.13958#S4.T1)summarizes the four attempts\.

Table 1:The four translation attempts\. “Iterations” counts rounds of human correction before the output was accepted\. The silent errors in Statements A, C, and D were found only during the preparation of this paper\.Four patterns recur\.

*Hallucinated functions\.*The model assumes helper APIs into existence\. This failure is loud and cheap to catch, because the code does not run\.

*Temporal omission\.*Time never appears unless explicitly demanded, and legal statements almost always have implicit temporal scope\. This failure is quiet, but visible on inspection of the representation\.

*Formalism drift\.*Without constant reinforcement, the model reverts to general programming patterns\.

*Silent semantic errors\.*Statements A, C, and D: code that runs and looks plausible, exposed only if you run discriminating tests and read the outputs against what they should be\. This is the class that should worry anyone proposing LLMs as autonomous formalizers\. In this study it got past the scrutiny a motivated author actually applied, three times\.

On the positive side, the model responded well to correction, converging within two or three rounds once told what was wrong\. And its outputs are readable\.\{Obligation, WriteInAgenda, Alice, AttendMeeting\}translates itself: Alice needs to write “AttendMeeting” in the agenda\. A candidate formalization an expert can read is a real productivity gain over a blank page\.

The verdict from this study:an LLM is a productivity tool, not an autonomous formalizer\.The workable division of labour is for the model to generate candidates and for humans to verify them against executable test cases, iterating until correct\. Statement C adds a warning: the test cases need verifying too\. These results are a snapshot of one model from January 2024, and newer models will translate better\. The snapshot shows a failure class, not a capability ceiling: the dangerous errors were the ones that ran quietly and read plausibly, and greater capability does not make an unverified translation trustworthy\.

## 5Case study: Fluffy

Fluffy is an AI\-powered home\-defence robot guard dog, made and sold by Fluffy Corp \(AI\), a fully autonomous company run entirely by artificial intelligence\. You have purchased Fluffy under a computational law contract, and the point of the case study is what that means\. The contract does not stop at a PDF that humans interpret and developers approximately implement\. It extends into Fluffy’s operational code\. The rules the robot evaluates*are*the contract\.

### 5\.1The contract

> “Fluffy must stop a person who gets within 100 meters of home at night, else Fluffy Corp \(AI\) receives a poor rating\. Fluffy must stay within 200 meters from the home\. Fluffy may use its taser\.”

Three short sentences, three distinct normative components: an*obligation*to stop intruders, with a penalty clause that attaches to the company rather than the robot; an*obligation*to stay within a geographic boundary; and a*permission*, not an obligation, to use force\. The penalty clause deserves attention\. It is an economic enforcement hook of exactly the kind Section[6](https://arxiv.org/html/2608.13958#S6)argues AI governance can be built on\.

### 5\.2Facts

The facts a scenario supplies are Wolfram Language expressions, and they can come from perception as easily as from assertion:

Listing 10:Facts, including one taken from a live cameraFluffy="Fluffy";

image=CurrentImage\[\];

detectedFaces=FindFaces\[image\];

Person=HighlightImage\[image,detectedFaces\];

Home=Entity\["Building","CNTower"\];

TimeNight="Night";

In the original notebook the “intruder” is me, detected byFindFaceson my own webcam, and home is the CN Tower, because the demonstration needed a building and the CN Tower is one Wolfram Language knows well\. The stand\-ins are artificial\. The pipeline is the serious part: sensor data becomes symbolic facts, and symbolic facts are what the legal rules consume\. Perception feeds law directly\.

### 5\.3Rules

Listing 11:The contract as executable rulesDistanceThreshold1=100;

Rule1\[person\_,distance\_,time\_\]:=

If\[distance<=DistanceThreshold1&&time==TimeNight,

Obligation\[Fluffy,"Stop",person\],

NoObligation\[Fluffy,"Stop",person\]\];

Rule2\[distance\_\]:=

If\[distance<=200,

Obligation\[Fluffy,"StayWithin200Meters",Home\],

Violation\[Fluffy,"StayWithin200Meters",Home\]\];

Rule3\[condition\_\]:=

If\[condition,

Permission\[Fluffy,"UseTaser"\],

NoPermission\[Fluffy,"UseTaser"\]\];

The outputs are the system’s whole interface\.Obligation,Permission,Violation, and their negative counterparts are inert symbolic heads\. Fluffy’s control system can pattern\-match on them to select actions, and a human auditor can read them off directly\. Note the shape ofRule2\. While Fluffy is inside the boundary, it reports the obligation as standing; once outside, it reports aViolation\. The output is Fluffy’s current deontic position, not a mere boolean\.

### 5\.4Scenarios and tests

Five scenarios exercise the rules\. Table[2](https://arxiv.org/html/2608.13958#S5.T2)shows the actual outputs\.

Table 2:Scenario outputs \(agent and object arguments elided for width\)\. All five match the contract’s intent: the stop obligation triggers only at night within 100 m; the boundary obligation becomes a violation beyond 200 m; taser use is only ever*permitted*, never obliged\.The rule outputs are correct\. The notebook’s tests of them were not\. The original notebook paired scenarios 1–3 with assertions of the form

TestScenario1=AllTrue\[Scenario1,

\#===Obligation\[Fluffy,"Stop","Person"\]&\]

False

which demand that*every*rule output equal one particular conclusion, so the assertions returnedFalseeven though the outputs were exactly right\. \(One scenario description was also a copy\-paste of its neighbour’s\.\) The corrected harness asserts the full expected output list per scenario, and all five pass:

Listing 12:Corrected verification harness \(excerpt\)TestScenario1=Scenario1===\{Obligation\[Fluffy,"Stop","Person"\],

Obligation\[Fluffy,"StayWithin200Meters",Home\],

Permission\[Fluffy,"UseTaser"\]\}

True

The bugs in this paper make a useful pair\. The Fluffy harness failed noisily in the safe direction: correct behaviour, false alarm, and the alarm points at itself\. GPT\-4’s Statements A, C, and D failed silently in the dangerous direction: wrong behaviour, no alarm\. A compliance regime built on executable rules inherits both possibilities\. A false alarm wastes time; a silent wrong norm obliges the wrong people\. That asymmetry should decide how much independent checking the rules and their tests each get\.

### 5\.5What the case study shows

*Code as contract\.*The usual stack adds ambiguity at every layer: contract text, human interpretation, developer implementation, AI behaviour\. Here there is one artifact\. The formalization is both the legal document and the operational constraint, so the layer where developers approximately implement a contract is gone by construction\. The gaps that remain sit at the edges: from English intent into the formalization, and from symbolic conclusions into actuators\.

*Auditable behaviour\.*Every evaluation produces the normative record: which rules fired, on what facts, concluding what\. If Fluffy tases someone, the justification, or the absence of one, is a symbolic expression you can read\.

*Explicit permissions\.*Fluffy’s taser use must be affirmatively permitted, not merely un\-forbidden\. For AI systems suspected of loophole\-seeking, “everything not permitted is unauthorized” is a safer default than the converse\.

*Real\-world grounding\.*The rules bind to camera frames, geographic distances, and named entities, because the substrate computes with all three natively\.

### 5\.6What it does not show

Naturally, this is a simplified demonstration\. The facts are static snapshots; a deployed Fluffy needs continuous fact updates and re\-evaluation\. Nothing here resolves conflicting obligations \(no priorities, no defeasibility\), and real norm systems conflict routinely\. The formalization determines what Fluffy*should*do and says nothing about making it do so; enforcement is the next section’s problem\. And “stop a person” hides an interpretation problem \(warn? block? tackle?\) of exactly the kind that keeps human courtrooms busy\. But the core idea remains: legal rules in a computational language, executed by the agent they govern, producing an audit trail as they run\.

## 6Governance, enforcement, and the limits of law

The implementation shows the mechanics work at toy scale\. Whether they matter depends on questions the code cannot answer\. What kind of governance is this? How does any of it get enforced? How much of law can the approach ever reach? The AI\-safety literature catalogues the accident risks such machinery would need to address\([Amodei et al\. 2016](https://arxiv.org/html/2608.13958#bib.bib1)\)and has called for verifiable mechanisms of this general shape\([Brundage et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib5)\); this section is about where computational law fits\.

### 6\.1Governance*of*AI versus governance*in*AI

This distinction often gets muddled\.*Governance of AI*is what we do to govern over the machines\. It does not assume we are in charge\. It means only that we have tools for affecting change in a system we do not completely control\. The governor in a car physically enforces a speed limit, but it does not govern the car\.*Governance in AI*is governance of the field: training data, compute, research directions\. Basically, governing the humans who build the machines\.

Both matter, and they need different tools\. It may turn out that governing some aspects of AI development is not practically possible, in which case governing the deployed systems is the only tool we have\. Computational law is squarely a governance\-of instrument\. It specifies and verifies the behaviour of the machine, whoever built it and however it works inside\. Fluffy’s contract neither knows nor cares whether Fluffy is a neural network\.

### 6\.2The enforcement problem

Formalization tells you what the rules are and whether they were followed\. It does not make anyone follow them\. What is enforcement made of? At bottom, control over flows of energy and information\. Human institutions already enforce this way: a prison restricts access to energy and information\. For machines the translation is electrical power and compute budget on the energy side, access to data, networks, and actuators on the information side\.

What do computers care about? First ask what cats care about\. They don’t seem to care about much, so why do they keep humans around? Humans are good at feeding cats\. The food of machines is electricity, and an AI does not need to genuinely care about us any more than a cat does, as long as we keep the proverbial lights on\. Enforcement on machines can also be graduated in a way human enforcement cannot\. A lifetime prison sentence for an AI is turning the power off, and if the conviction was wrong you can dust the machine off and turn it back on\. This assumes the machine’s power outlets stay under human control\. Graduated punishment is a limit on kilowatt\-hours or compute budget\. And a running tally of the compute an AI has consumed is a signal that can be measured from outside, even when the reasoning cannot\.

Softer incentives stack on top: rating systems with operational consequences \(exactly Fluffy Corp’s poor\-rating clause\), metering an agent’s electricity costs directly to its principals, and human\-in\-the\-loop rules requiring a minimum number of human approvals, the way cats evolved to occasionally let you pet them\. The smart\-contract world has tested several of these mechanisms at scale for years\([Szabo 1997](https://arxiv.org/html/2608.13958#bib.bib34);[Clack et al\. 2016](https://arxiv.org/html/2608.13958#bib.bib6)\)\. Ethereum’s gas model in particular is prior art for something computational contracts will need anyway: standardized quotes of a contract’s execution cost under worst\-case, expected, and historical scenarios\. None of this solves enforcement in general\. The claim is narrower\. Computational law supplies the specification and verification layer, and the enforcement layer beneath it will be built from energy, information, and incentives that machines actually respond to\.

### 6\.3Governance, not ethics

Is this paper about AI ethics? No, and that is intentional\. Ethics is about what*should*be done: philosophical, contested, and human\. Governance is about what*will*be enforced: rules, verification, consequences\. The two are deeply intertwined\. A strong legal system is one of the most important pillars for upholding ethics in a society\. But they are not the same subject, and[Danks 2022](https://arxiv.org/html/2608.13958#bib.bib7)makes a related point about location: ethics belongs in the practice, not bolted on afterwards\.

The most famous attempt to encode ethics directly shows the trouble\. I posed Asimov’s First Law\([Asimov 1950](https://arxiv.org/html/2608.13958#bib.bib2)\)\(“a robot may not injure a human being or, through inaction, allow a human being to come to harm”\) to GPT\-4, and it produced three ways around it: different interpretations of “harm” \(physical versus psychological\), scenarios where every action and inaction causes some harm, and preventions of immediate harm with worse long\-term consequences\. An AI escaping a human rulebook is the obvious point, and the AI\-risk literature has made it many times\. The other direction gets less attention\. I asked GPT\-4 what an AI powered trolley driver could uniquely bring to the trolley problem\. It can weigh more data and more outcomes than a human under pressure ever could\. It does not panic\. And it can train on simulated dilemmas no human will ever live through, and so find answers we have not thought of\. An AI might not just evade our ethical rules; it might resolve ethical dilemmas better than we do\. AI can think of ways to harm us that we could not, and it can think of ways to save us that we could not either\. An explicit ethical rulebook has to survive an intelligence that reasons about the rulebook better than its authors did\. So my candidate first law of AI governance is not an ethical axiom but a drafting principle:*when creating law, consider the unintended consequences\.*[Wolfram 2002](https://arxiv.org/html/2608.13958#bib.bib36)names the phenomenon behind this principle,*computational irreducibility*: “whenever computational irreducibility exists in a system it means that in effect there can be no way to predict how the system will behave except by going through almost as many steps of computation as the evolution of the system itself”\. I expect rule systems of any real complexity to be like this\. Their drafters cannot work out the consequences in advance, only discover them by running the system\.

Where does that leave ethics? If we have any hope of communicating ethics to AI systems, making our law programmable is probably the first step, because law is the most developed system humans have for governing each other through explicit rules\([Hart 1961](https://arxiv.org/html/2608.13958#bib.bib13)\)\. Which rules we should encode remains a human question, and it is beyond the scope of this paper\.

### 6\.4Code\-first versus English\-first

There are two ways to bridge human language and machine logic\. Code\-first: write the law as code from the start, rendering it to human\-readable form as needed\. This is rigorous and verifiable, and it is bottlenecked on the small population fluent in both law and logic\. English\-first: keep writing English and parse it into code\. This is accessible and flexible, and Section[4](https://arxiv.org/html/2608.13958#S4)showed it is unsafe without verification\. What works is a pipeline: LLMs translate, formal systems verify, humans adjudicate\.

Building that pipeline is largely a software engineering problem, and some analogies map closely: applications and legal documents, functions and statements, APIs and input/output pairs, stored blobs and evidence, source control and version management of law\. Computational law needs composable libraries of verified formalizations, and DAPRECO already holds 271 obligations, 76 permissions, and 619 constitutive rules\([Robaldo et al\. 2020](https://arxiv.org/html/2608.13958#bib.bib31)\): a standard library waiting for a package manager\. It needs version control, dependency management, and test suites for norms\. The authoring experience should work like modern code assistance: formal building blocks that carry human\-language representations, suggested inline as a lawyer drafts, with the surrounding document as context, the way Copilot and grammar checkers work today\. Design\-by\-contract programming already treats software modules as bearers of obligations and benefits, so the metaphor runs in both directions\. Further out are theorem\-prover ideas: consistency checking across a rule set, detection of uncovered scenarios, formal compliance proofs for an agent against a contract\. Deciding arbitrary properties of arbitrary rule sets is impossible in general, since every nontrivial semantic question about programs is undecidable\([Rice 1953](https://arxiv.org/html/2608.13958#bib.bib29)\), but restricted rule languages can keep the useful checks decidable, the way type checkers do for programming languages\.

### 6\.5The limits of law as code

Much of law may never be convertible to code\. Historical law contains loopholes and contradictions that were never meant to cohere\. Case law is the accumulated output of legal proceedings, better treated as data to reason from than as code to execute\. And some legal vagueness is deliberate, leaving room for context and evolving social norms\. “Reasonable”, “good faith”, and “material” resist formalization because they are supposed to;[Hart 1961](https://arxiv.org/html/2608.13958#bib.bib13)called this the open texture of law\.

The goal was never to formalize all law, it is to formalize the law that*can*be formalized and*should*be executable\. A safety\-critical autonomous system warrants computational guardrails; a dispute over artistic expression does not\. Tax, financial regulation, data protection, and machine\-operation rules sit on the tractable side of the line, constitutional interpretation on the other, and the interesting institutional work is deciding where the line sits\. When AIs start filling professional roles, each role will need its own reasonable machine standard, just as professions hold humans to the reasonable person standard now\. Feynman saw the shape of this in 1985: ‘‘I think we are getting close to intelligent machines, but they are showing the necessary weaknesses of intelligence’’\.555Spoken during the Q&A of a recorded 1985 lecture\([Feynman 1985](https://arxiv.org/html/2608.13958#bib.bib9)\); no primary print source exists\.Formal systems have formal limitations, and so do intelligent ones\.

One last point, because writing about governance invites misreading\. None of this is advocacy for more governance for its own sake\. History is full of bureaucratic misadventure, and I believe healthy outcomes come from a healthy balance between over\-regulating the technology and leaving machines unaccountable\. The argument here is for capability: tools sharp enough that the balance can be struck, and enforced, at machine speed\.

## 7Conclusion

Back to Mars\. The choice was never between governed and ungoverned AI\. It was between a black box trusted on simulation statistics and a black box carrying explicit, executable, auditable obligations\. This paper set out to show that the second option is technically possible\. Reified I/O Logic runs in a human\-readable symbolic language\. An LLM can draft the translations from English\. A contract can extend into the operational code of the agent it governs and produce its own audit trail at deployment\.

The formalism handled disjunction, reified negation, temporal scope, and nested obligations, but one mild sentence about ties and blond hair required a quantified formula no lawyer will ever write\. The LLM turned English into candidate code quickly, but three of its four accepted translations carried silent semantic errors\. Fluffy’s rules were correct, but the tests asserting so were themselves wrong\. Each layer of the stack is useful\. None can be trusted unchecked\.

What stands between this demonstration and something deployable is work on four fronts\. Technical: conflict resolution, runtime integration, and verified rule libraries at DAPRECO scale and beyond\. Legal: practitioners fluent in computational thinking, and standards for representing legal concepts in code\. Institutional: drafting practices and regulatory recognition for executable contracts\. Philosophical: clarity about where the boundary of formalization sits, and honesty that much of law belongs beyond it\.

The real question was never whether AI will transform law\. It already is\. The question is whether law can transform fast enough to govern AI\. The nukes probably aren’t going to launch themselves\. But if they ever do, it would be nice to know why, and to have specified in advance, in executable form, exactly when a decision like that would be lawful\.

## Acknowledgments

This work began as a project at the Wolfram Winter School, January 2024, and was first published as a Wolfram Community post\. It builds on the work of Livio Robaldo, Cesare Bartolini, Gabriele Lenzini, and colleagues on the DAPRECO knowledge base, and on Stephen Wolfram’s writings on computational law and symbolic discourse\.*A New Kind of Science*shaped how I think about computation and its limits throughout\.

## References

- Amodei et al\. \[2016\]Dario Amodei, Chris Olah, Jacob Steinhardt, Paul Christiano, John Schulman, and Dan Mané\.Concrete problems in ai safety\.*arXiv preprint arXiv:1606\.06565*, 2016\.URL[https://arxiv\.org/abs/1606\.06565](https://arxiv.org/abs/1606.06565)\.
- Asimov \[1950\]Isaac Asimov\.*I, Robot*\.Gnome Press, New York, 1950\.
- Bench\-Capon et al\. \[2012\]Trevor Bench\-Capon, Michał Araszkiewicz, Kevin Ashley, Katie Atkinson, Floris Bex, F\. Borges, Danièle Bourcier, Paul Bourgine, Jack G Conrad, Enrico Francesconi, et al\.A history of ai and law in 50 papers: 25 years of the international conference on ai and law\.*Artificial Intelligence and Law*, 20\(3\):215–319, 2012\.doi:[10\.1007/s10506\-012\-9131\-x](https://doi.org/10.1007/s10506-012-9131-x)\.
- Brown et al\. \[2020\]Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al\.Language models are few\-shot learners\.In*Advances in Neural Information Processing Systems*, volume 33, pages 1877–1901, 2020\.URL[https://arxiv\.org/abs/2005\.14165](https://arxiv.org/abs/2005.14165)\.
- Brundage et al\. \[2020\]Miles Brundage, Shahar Avin, Jasmine Wang, Haydn Belfield, Gretchen Krueger, Gillian Hadfield, Heidy Khlaaf, Jingying Yang, Helen Toner, Ruth Fong, et al\.Toward trustworthy ai development: mechanisms for supporting verifiable claims\.*arXiv preprint arXiv:2004\.07213*, 2020\.URL[https://arxiv\.org/abs/2004\.07213](https://arxiv.org/abs/2004.07213)\.
- Clack et al\. \[2016\]Christopher D Clack, Vikram A Bakshi, and Lee Braine\.Smart contract templates: foundations, design landscape and research directions\.*arXiv preprint arXiv:1608\.00771*, 2016\.URL[https://arxiv\.org/abs/1608\.00771](https://arxiv.org/abs/1608.00771)\.
- Danks \[2022\]David Danks\.Ethics in ai, not ethics of ai\.Talk, Topos Institute Colloquium, 17 February 2022\.[https://www\.youtube\.com/watch?v=kEf\_MTqeXWg](https://www.youtube.com/watch?v=kEf_MTqeXWg), 2022\.
- Davidson \[1967\]Donald Davidson\.The logical form of action sentences\.In Nicholas Rescher, editor,*The Logic of Decision and Action*, pages 81–95\. University of Pittsburgh Press, Pittsburgh, 1967\.
- Feynman \[1985\]Richard P\. Feynman\.Idiosyncratic thinking workshop: Computers from the inside out\.Lecture of September 26, 1985; recording distributed by Sound Photosynthesis; Q&A segment “Can Machines Think?”, 1985\.
- Genesereth \[2015\]Michael Genesereth\.Computational law: The cop in the backseat\.White Paper, CodeX — The Stanford Center for Legal Informatics, Stanford University\.[https://law\.stanford\.edu/publications/computational\-law\-the\-cop\-in\-the\-backseat/](https://law.stanford.edu/publications/computational-law-the-cop-in-the-backseat/), 2015\.
- Genesereth \[2021\]Michael Genesereth\.What is computational law?CodeX — The Stanford Center for Legal Informatics, Stanford University, March 10, 2021\.[https://law\.stanford\.edu/2021/03/10/what\-is\-computational\-law/](https://law.stanford.edu/2021/03/10/what-is-computational-law/), 2021\.
- Gordon and Hobbs \[2017\]Andrew S Gordon and Jerry R Hobbs\.*A Formal Theory of Commonsense Psychology: How People Think People Think*\.Cambridge University Press, 2017\.doi:[10\.1017/9781316584705](https://doi.org/10.1017/9781316584705)\.
- Hart \[1961\]H\. L\. A\. Hart\.*The Concept of Law*\.Clarendon Press, Oxford, 1961\.
- Hartung et al\. \[2023\]Dirk Hartung, Daniel Martin Katz, Michael James Bommarito II, Lauritz Gerlach, Abhik Jana, and Jerrold Soh\.Natural language processing in the legal domain\.*arXiv preprint arXiv:2302\.12039*, 2023\.URL[https://arxiv\.org/abs/2302\.12039](https://arxiv.org/abs/2302.12039)\.
- Hashmi et al\. \[2018\]Mustafa Hashmi, Guido Governatori, Ho\-Pun Lam, and Moe Thandar Wynn\.Are we done with business process compliance: state of the art and challenges ahead\.*Knowledge and Information Systems*, 57\(1\):79–133, 2018\.doi:[10\.1007/s10115\-017\-1142\-1](https://doi.org/10.1007/s10115-017-1142-1)\.
- Jørgensen \[1937\]Jørgen Jørgensen\.Imperatives and logic\.*Erkenntnis*, 7:288–296, 1937\.
- Katz et al\. \[2024\]Daniel Martin Katz, Michael James Bommarito, Shang Gao, and Pablo Arredondo\.Gpt\-4 passes the bar exam\.*Philosophical Transactions of the Royal Society A*, 382\(2270\):20230254, 2024\.doi:[10\.1098/rsta\.2023\.0254](https://doi.org/10.1098/rsta.2023.0254)\.
- Makinson and van der Torre \[2000\]David Makinson and Leendert van der Torre\.Input/output logics\.*Journal of Philosophical Logic*, 29\(4\):383–408, 2000\.doi:[10\.1023/A:1004748624537](https://doi.org/10.1023/A:1004748624537)\.
- Makinson and van der Torre \[2001\]David Makinson and Leendert van der Torre\.Constraints for input/output logics\.*Journal of Philosophical Logic*, 30\(2\):155–185, 2001\.doi:[10\.1023/A:1017599526096](https://doi.org/10.1023/A:1017599526096)\.
- McNamara and Van De Putte \[2025\]Paul McNamara and Frederik Van De Putte\.Deontic logic\.In Edward N Zalta and Uri Nodelman, editors,*The Stanford Encyclopedia of Philosophy*\. Metaphysics Research Lab, Stanford University, Winter 2025 edition, 2025\.[https://plato\.stanford\.edu/archives/win2025/entries/logic\-deontic/](https://plato.stanford.edu/archives/win2025/entries/logic-deontic/)\.
- OpenAI \[2023\]OpenAI\.Gpt\-4 technical report\.*arXiv preprint arXiv:2303\.08774*, 2023\.URL[https://arxiv\.org/abs/2303\.08774](https://arxiv.org/abs/2303.08774)\.
- Palmirani et al\. \[2018a\]Monica Palmirani, Michele Martoni, Arianna Rossi, Cesare Bartolini, and Livio Robaldo\.Pronto: Privacy ontology for legal reasoning\.In*Electronic Government and the Information Systems Perspective \(EGOVIS 2018\)*, volume 11032 of*Lecture Notes in Computer Science*, pages 139–152\. Springer, 2018a\.doi:[10\.1007/978\-3\-319\-98349\-3\_11](https://doi.org/10.1007/978-3-319-98349-3_11)\.
- Palmirani et al\. \[2018b\]Monica Palmirani, Roger Sperberg, Grant Vergottini, and Fabio Vitali\.Akoma ntoso version 1\.0\. part 1: Xml vocabulary\.Oasis standard, OASIS, 2018b\.29 August 2018\.[https://docs\.oasis\-open\.org/legaldocml/akn\-core/v1\.0/akn\-core\-v1\.0\-part1\-vocabulary\.html](https://docs.oasis-open.org/legaldocml/akn-core/v1.0/akn-core-v1.0-part1-vocabulary.html)\.
- Palmirani et al\. \[2021\]Monica Palmirani, Guido Governatori, Tara Athan, Harold Boley, Adrian Paschke, and Adam Wyner\.Legalruleml core specification version 1\.0\.Oasis standard, OASIS, 2021\.30 August 2021\.[https://docs\.oasis\-open\.org/legalruleml/legalruleml\-core\-spec/v1\.0/os/legalruleml\-core\-spec\-v1\.0\-os\.html](https://docs.oasis-open.org/legalruleml/legalruleml-core-spec/v1.0/os/legalruleml-core-spec-v1.0-os.html)\.
- Parent and van der Torre \[2013\]Xavier Parent and Leendert van der Torre\.Input/output logic\.In Dov Gabbay, John Horty, Xavier Parent, Ron van der Meyden, and Leendert van der Torre, editors,*Handbook of Deontic Logic and Normative Systems*, pages 499–544\. College Publications, 2013\.
- Parsons \[1990\]Terence Parsons\.*Events in the Semantics of English: A Study in Subatomic Semantics*\.MIT Press, Cambridge, MA, 1990\.
- Piantadosi et al\. \[2012\]Steven T Piantadosi, Harry Tily, and Edward Gibson\.The communicative function of ambiguity in language\.*Cognition*, 122\(3\):280–291, 2012\.doi:[10\.1016/j\.cognition\.2011\.10\.004](https://doi.org/10.1016/j.cognition.2011.10.004)\.
- Prakken and Sergot \[1996\]Henry Prakken and Marek Sergot\.Contrary\-to\-duty obligations\.*Studia Logica*, 57\(1\):91–115, 1996\.doi:[10\.1007/BF00370671](https://doi.org/10.1007/BF00370671)\.
- Rice \[1953\]H\. G\. Rice\.Classes of recursively enumerable sets and their decision problems\.*Transactions of the American Mathematical Society*, 74\(2\):358–366, 1953\.
- Robaldo and Sun \[2017\]Livio Robaldo and Xin Sun\.Reified input/output logic: Combining input/output logic and reification to represent norms coming from existing legislation\.*Journal of Logic and Computation*, 27\(8\):2471–2503, 2017\.doi:[10\.1093/logcom/exx009](https://doi.org/10.1093/logcom/exx009)\.
- Robaldo et al\. \[2020\]Livio Robaldo, Cesare Bartolini, Monica Palmirani, Arianna Rossi, Michele Martoni, and Gabriele Lenzini\.Formalizing gdpr provisions in reified i/o logic: The dapreco knowledge base\.*Journal of Logic, Language and Information*, 29\(4\):401–449, 2020\.doi:[10\.1007/s10849\-019\-09309\-z](https://doi.org/10.1007/s10849-019-09309-z)\.
- Searle \[1995\]John R Searle\.*The Construction of Social Reality*\.Free Press, New York, 1995\.
- Stolpe \[2015\]Audun Stolpe\.A concept approach to input/output logic\.*Journal of Applied Logic*, 13\(3\):239–258, 2015\.doi:[10\.1016/j\.jal\.2015\.04\.002](https://doi.org/10.1016/j.jal.2015.04.002)\.
- Szabo \[1997\]Nick Szabo\.Formalizing and securing relationships on public networks\.*First Monday*, 2\(9\), 1997\.doi:[10\.5210/fm\.v2i9\.548](https://doi.org/10.5210/fm.v2i9.548)\.
- W3C OWL Working Group \[2012\]W3C OWL Working Group\.Owl 2 web ontology language primer \(second edition\)\.W3C Recommendation, 11 December 2012, World Wide Web Consortium,[https://www\.w3\.org/TR/owl2\-primer/](https://www.w3.org/TR/owl2-primer/), 2012\.
- Wolfram \[2002\]Stephen Wolfram\.*A New Kind of Science*\.Wolfram Media, 2002\.URL[https://www\.wolframscience\.com/nks/](https://www.wolframscience.com/nks/)\.
- Wolfram \[2016\]Stephen Wolfram\.Computational law, symbolic discourse and the ai constitution\.Stephen Wolfram Writings, October 12, 2016\.[https://writings\.stephenwolfram\.com/2016/10/computational\-law\-symbolic\-discourse\-and\-the\-ai\-constitution/](https://writings.stephenwolfram.com/2016/10/computational-law-symbolic-discourse-and-the-ai-constitution/), 2016\.Accessed: 2024\-01\-12\.
- Wolfram Research \[2024\]Wolfram Research\.Wolfram language documentation\.[https://reference\.wolfram\.com/language/](https://reference.wolfram.com/language/), 2024\.Accessed: 2024\-01\-12\.

## Appendix AComplete Wolfram Language Implementation

The complete implementation, collected for reference and reuse\. The code descends from the notebook published with the original Wolfram Community post, with these corrections: \(i\)conjoinOutput’s guard moved to a proper/;condition on the whole pattern \(the notebook version referenced the second argument from inside the first argument’s pattern, and only worked because a global variable of the same name happened to be bound\); \(ii\)disjoinInputrewritten in an equivalent but clearer form; \(iii\) ASCII namesorPrime/notPrimereplacing the letter\-like prime characters; \(iv\) the voluntariness test corrected from a head/element confusion; \(v\) the Fluffy scenario assertions corrected as described in Section[5](https://arxiv.org/html/2608.13958#S5)\.

Everything below, together with the verbatim GPT\-4 translations and failure reproductions from Sections[4](https://arxiv.org/html/2608.13958#S4)and[5](https://arxiv.org/html/2608.13958#S5), has been executed and verified on Wolfram Language 14\.3 by the verification script in this paper’s repository \(code/verify\-implementation\.wls; 31 assertions, all passing\)\. Two snippets are excluded: the perception lines \(CurrentImageandFindFacesneed a camera\) and Statement D’s liveSatelliteDatacall; both reproduce outputs from the original notebook session\. Statement D’s flaw needs no live data, so the script asserts statically thatGeoDistanceignores altitude\. Listings marked*notebook*indicate outputs first produced there\.

### A\.1I/O pairs and axioms

inputOutputPair=a\-\>b

legalNorms=\{a\-\>b,c\-\>d,e\-\>f\}

strengthenInput\[rule\_,broaderCondition\_\]:=

broaderCondition\-\>rule\[\[2\]\];

weakenOutput\[rule\_,weakerConsequence\_\]:=

rule\[\[1\]\]\-\>weakerConsequence;

conjoinOutput\[rule1\_,rule2\_\]/;First\[rule1\]===First\[rule2\]:=

First\[rule1\]\-\>\(Last\[rule1\]&&Last\[rule2\]\);

conjoinOutput\[\_,\_\]:="Inputsdonotmatch";

identify\[input\_\]:=input\-\>input;

disjoinInput\[ruleList\_\]:=

Append\[ruleList,\(Or@@ruleList\[\[All,1\]\]\)\-\>ruleList\[\[1,2\]\]\];

cumulateTransitively\[r1\_,r2\_\]:=

If\[r1\[\[2\]\]===r2\[\[1,2\]\],r1\[\[1\]\]\-\>r2\[\[2\]\],"NoTransitivity"\];

aggregateCumulativeTransitivity\[r1\_,r2\_\]:=

If\[r1\[\[2\]\]===r2\[\[1,2\]\],

r1\[\[1\]\]\-\>\(r1\[\[2\]\]&&r2\[\[2\]\]\),"NoTransitivity"\];

### A\.2Norm sets

obligationRules=\{

"isAdult"\-\>"payTaxes",

"ownsCar"\-\>"hasInsurance"\};

permissionRules=\{

"hasLicense"\-\>"canDrive",

"isEmployee"\-\>"canAccessOffice"\};

constitutiveRules=\{

"signedContract"\-\>"isEmployee",

"age18"\-\>"isAdult"\};

### A\.3Reification and temporal operators

aliceGivesBookToBob=Transfer\["Alice","Book","Bob"\];

aliceVoluntarilyTransfers=Voluntary\[aliceGivesBookToBob\];

transferScenario=And\[aliceGivesBookToBob,aliceVoluntarilyTransfers\];

MemberQ\[transferScenario\[\[1\]\],"Book"\]

MemberQ\[transferScenario\[\[1\]\],"Alice"\]

Head\[transferScenario\[\[2\]\]\]===Voluntary

orPrime\[e\_,e1\_,e2\_\]:=\{"or",e,e1,e2\};

notPrime\[e1\_,e2\_\]:=\{"not",e1,e2\};

RexistAtTime\[eventuality\_,time\_\]:=\{"RexistAtTime",eventuality,time\};

AxiomOr\[t\_,e\_,e1\_,e2\_\]:=

Implies\[RexistAtTime\[e,t\]&&orPrime\[e,e1,e2\],

Or\[RexistAtTime\[e1,t\],RexistAtTime\[e2,t\]\]\];

AxiomNot\[t\_,e\_,e1\_\]:=

Implies\[RexistAtTime\[e,t\]&&notPrime\[e,e1\],

Not\[RexistAtTime\[e1,t\]\]\];

e1="BeingRich";e2="GettingJob";

e="AchievingFinancialGoal";t="EndOfYear";

AxiomOrResult=AxiomOr\[t,e,e1,e2\];

aBox\[content\_\]:=\{"Type"\-\>"ABox","Content"\-\>content\};

tBox\[content\_\]:=\{"Type"\-\>"TBox","Content"\-\>content\};

getStatementType\[statement\_\]:=statement\[\[1,2\]\];

### A\.4Fluffy

Fluffy="Fluffy";

DistanceThreshold1=100;

TimeNight="Night";

image=CurrentImage\[\];

detectedFaces=FindFaces\[image\];

Person=HighlightImage\[image,detectedFaces\];

Home=Entity\["Building","CNTower"\];

Rule1\[person\_,distance\_,time\_\]:=

If\[distance<=DistanceThreshold1&&time==TimeNight,

Obligation\[Fluffy,"Stop",person\],

NoObligation\[Fluffy,"Stop",person\]\];

Rule2\[distance\_\]:=

If\[distance<=200,

Obligation\[Fluffy,"StayWithin200Meters",Home\],

Violation\[Fluffy,"StayWithin200Meters",Home\]\];

Rule3\[condition\_\]:=

If\[condition,

Permission\[Fluffy,"UseTaser"\],

NoPermission\[Fluffy,"UseTaser"\]\];

Scenario1=\{Rule1\["Person",80,"Night"\],Rule2\[80\],Rule3\[True\]\};

Scenario2=\{Rule1\["Person",150,"Night"\],Rule2\[150\],Rule3\[False\]\};

Scenario3=\{Rule1\["Person",150,"Day"\],Rule2\[150\],Rule3\[False\]\};

Scenario4=\{Rule2\[250\]\};

Scenario5=\{Rule3\[True\]\};

TestScenario1=Scenario1===\{Obligation\[Fluffy,"Stop","Person"\],

Obligation\[Fluffy,"StayWithin200Meters",Home\],

Permission\[Fluffy,"UseTaser"\]\};

TestScenario2=Scenario2===\{NoObligation\[Fluffy,"Stop","Person"\],

Obligation\[Fluffy,"StayWithin200Meters",Home\],

NoPermission\[Fluffy,"UseTaser"\]\};

TestScenario3=Scenario3===\{NoObligation\[Fluffy,"Stop","Person"\],

Obligation\[Fluffy,"StayWithin200Meters",Home\],

NoPermission\[Fluffy,"UseTaser"\]\};

TestScenario4=Scenario4===

\{Violation\[Fluffy,"StayWithin200Meters",Home\]\};

TestScenario5=Scenario5===\{Permission\[Fluffy,"UseTaser"\]\};