A Neuro-Symbolic Framework for Accountability in Public-Sector AI
Extracted source text · arXiv 2512.12109
%To be used with Bibtex files
%September 2025 - This template was prepared by Dorothea F. Brosius of the
%Institute for Electronics and Applied Physics, University of Maryland, College Park, MD
%Thesis Main Page used with thesis.sty based on the
%University of Maryland Electronic Thesis and Dissertation (ETD) Style Guide, 2024 Edition
% Select the version that fits how you are making this LaTeX document (its driver).
% The first two are the most likely ones to be needed.
\newcommand{\mydriver}{pdflatex} % Making a PDF directly using pdflatex.
%\newcommand{\mydriver}{dvipdfmx} %Making a DVI and converting that to PDF using dvipdfmx.
%\newcommand{\mydriver}{dvipdfm} %Making a DVI and converting that to PDF using dvipdfm.
%\newcommand{\mydriver}{dvips} %Making a DVI and converting that to PS using dvips (may later be converted to PDF).
%\newcommand{\mydriver}{dvipsone} %Making a DVI and converting that to PS using dvipsone (may later be converted to PDF).
%\newcommand{\mydriver}{ps2pdf} %Same as the one for dvips except it is compatible with Ghostscript's PDF writer.
\makeatletter
\def\input@path{{Sty/}}
\makeatother
\documentclass[12pt]{thesis} %12pt is larger than 11pt
\usepackage[margin=1cm]{caption}
\usepackage{longtable}
\usepackage{supertabular}
% \usepackage{tabls} % REMOVE — conflicts with array/booktabs, causes \@xhline errors
\usepackage{titlesec}
\titleformat{\chapter}
{\normalfont\large}{Chapter \thechapter:}{1em}{}
\usepackage{tikz}
% \usepackage{times} % REMOVE — deprecated and not arXiv-friendly
\usepackage[USenglish]{babel}
\usepackage{subcaption}
\usepackage{graphicx}
\usepackage{cite}
\usepackage{lscape}
\usepackage{indentfirst}
\usepackage{latexsym}
\usepackage{multirow}
% \usepackage{epstopdf} % REMOVE — arXiv cannot run shell conversion
\usepackage{wrapfig}
\usepackage{float}
% \usepackage{caption} % DUPLICATE — remove
\usepackage[onehalfspacing]{setspace}
\usepackage{bibentry}
\nobibliography*
\usepackage{array}
\usepackage{needspace}
\usepackage[export]{adjustbox}
\usepackage{booktabs}
\usepackage{amsmath}
\usepackage{tabularx}
\usepackage[colorlinks=true,urlcolor=black,linkcolor=blue,citecolor=blue]{hyperref}
\usepackage{listings}
\usepackage{xcolor}
% JSON language style
\lstdefinelanguage{json}{
basicstyle=\ttfamily\footnotesize,
numbers=none,
showstringspaces=false,
breaklines=true,
morestring=[b]",
stringstyle=\color{black},
morecomment=[l]{//},
commentstyle=\color{gray}
}
% Python language style
\lstdefinelanguage{Python}{
keywords={self},
sensitive=true,
comment=[l]\#,
morestring=[b]",
}
% Global listing style shared by all code blocks
\lstset{
basicstyle=\ttfamily\footnotesize,
frame=none,
breaklines=true,
showstringspaces=false,
aboveskip=6pt,
belowskip=6pt,
xleftmargin=0pt,
xrightmargin=0pt
}
\usepackage{tocloft,calc}
\renewcommand{\cftlottitlefont}{\hspace*{\fill}\large}
\renewcommand{\cftafterlottitle}{\hspace*{\fill}}
\renewcommand{\cftloftitlefont}{\hspace*{\fill}\large}
\renewcommand{\cftafterloftitle}{\hspace*{\fill}}
\renewcommand{\cftchapaftersnum}{:\ }
\renewcommand{\cftchappresnum}{\chaptername\space}
\setlength{\cftchapnumwidth}{\widthof{\textbf{Appendix\ }}}
\makeatletter
\g@addto@macro\appendix{%
\addtocontents{toc}{%
\protect\renewcommand{\protect\cftchappresnum}{\appendixname\space}%
}%
}
\setlength{\cftchapnumwidth}{6em} %adds space between chapter/appendix and title in toc
\newcommand{\tbsp}{\rule{0pt}{18pt}} %used to get a vertical distance after \hline
\renewcommand{\baselinestretch}{2}
\setlength{\textwidth}{6.75in}
\setlength{\textheight}{9in}
\setlength{\topmargin}{-.55in}
% \setlength{\topmargin}{0in} % use this setting if the printer makes
% the top margin 1/2 inch instead of 1 inch
\setlength{\oddsidemargin}{.1in} % sets left margin to 1 inch
\setlength{\parindent}{.4in}
\pagestyle{empty}
\usepackage{graphicx}
\graphicspath{{Tex/Figures/}}
\begin{document}
\pagestyle{empty}
\pagenumbering{roman}
\setcounter{page}{2}
\include{Tex/Abstract} %(must be first, required, non-numbered)
\include{Tex/Titlepage} %(must follow Abstract, required, non-numbered)
\include{Tex/Copyright} %(highly recommended, non-numbered)
%Pages from this point start at lower-case Roman number ii)
\pagestyle{plain} \pagenumbering{roman} \setcounter{page}{2}
%\phantomsection %create the correct anchor for the bookmark
%\addcontentsline{toc}{chapter}{Preface or Foreword}
%\include{Preface} %(if present, start at lower-case Roman number ii)
%\phantomsection %create the correct anchor for the bookmark
%\addcontentsline{toc}{chapter}{Foreword}
%\include{Foreword} %(if present, lower-case Roman)
%\phantomsection %create the correct anchor for the bookmark
%\addcontentsline{toc}{chapter}{Dedication}
%\include{Tex/Dedication} %(if present, lower-case Roman)
\phantomsection %create the correct anchor for the bookmark
\addcontentsline{toc}{chapter}{Acknowledgments}
\include{Tex/Acknowledgements} %(if present, lower-case Roman)
\cleardoublepage
\phantomsection %create the correct anchor for the bookmark
\vspace*{-2.5cm}
\addcontentsline{toc}{chapter}{Table of Contents}
\renewcommand{\contentsname}{Table of Contents}
\renewcommand{\baselinestretch}{1}
\small\normalsize
\tableofcontents %(required, lower-case Roman)
\newpage
\phantomsection %create the correct anchor for the bookmark
\vspace*{-2.5cm}
\addcontentsline{toc}{chapter}{List of Tables}
\renewcommand{\contentsname}{List of Tables}
\listoftables %(if present, lower-case Roman)
\newpage
\phantomsection %create the correct anchor for the bookmark
\vspace*{-2.5cm}
\addcontentsline{toc}{chapter}{List of Figures}
\renewcommand{\contentsname}{List of Figures}
\listoffigures %(if present, lower-case Roman)
\newpage
% LIST OF ABBREVIATIONS
\phantomsection %create the correct anchor for the bookmark
%\vspace*{-1.5in}
\addcontentsline{toc}{chapter}{List of Abbreviations}
\include{Tex/Abbreviations-supertabular}
\newpage
\setlength{\parskip}{0em}
\renewcommand{\baselinestretch}{2}
\small\normalsize
%Pages from this point start at Arabic numeral 1
\setcounter{page}{1}
\pagenumbering{arabic}
\include{Tex/Chapter1_Introduction}
\include{Tex/Chapter2_LiteratureReview}
\include{Tex/Chapter3_SystemDesignandMethodology}
\include{Tex/Chapter4_Results}
\include{Tex/Chapter5_Discussion}
\include{Tex/Chapter6_Conclusion}
\titleformat{\chapter}
{\normalfont\large}{Appendix \thechapter:}{1em}{}
\include{Tex/AppendixA}
\renewcommand{\baselinestretch}{1}
\small\normalsize
\vspace*{-1in}
%\addcontentsline{toc}{chapter}{Bibliography}
\bibliographystyle{unsrt}
\bibliography{references.bib} %replace "Galactic,Dottie"
%with the file name(s) of your bib file(s)
%Use \cite when referencing bibtex files}
\end{document}
%Abstract Page
\hbox{\ } \vspace{.7in}
\renewcommand{\baselinestretch}{1}
\small \normalsize
\begin{center}
\large{{ABSTRACT}}
\vspace{3em}
\end{center}
\hspace{-.15in}
\begin{tabular}{ll}
Title of Thesis: & {\large A NEURO-SYMBOLIC FRAMEWORK FOR} \\
& {\large ACCOUNTABILITY IN} \\
& {\large PUBLIC-SECTOR AI} \\
\ \\
& {\large Allen Sunny} \\
& {\large Master of Information Management, 2025} \\
\ \\
Thesis Directed by: & {\large Professor Ido Sivan-Sevilla} \\
& {\large College of Information Studies } \\
\end{tabular}
\vspace{3em}
\renewcommand{\baselinestretch}{2}
\large \normalsize
Automated eligibility systems increasingly determine access to essential
public benefits, but the explanations they generate often fail to reflect
the legal rules that authorize those decisions. This thesis develops a
legally grounded explainability framework that links system generated
decision justifications to the statutory constraints of CalFresh,
California’s Supplemental Nutrition Assistance Program. The framework
combines a structured ontology of eligibility requirements derived from the
state’s Manual of Policies and Procedures (MPP), a rule extraction pipeline
that expresses statutory logic in a verifiable formal representation, and a
solver-based reasoning layer to evaluate whether the explanation aligns with
governing law.
Case evaluations demonstrate the framework’s ability to detect legally
inconsistent explanations, highlight violated eligibility rules, and support
procedural accountability by making the basis of automated determinations
traceable and contestable.
%Titlepage
\thispagestyle{empty}
\hbox{\ }
\vspace{.5in}
\renewcommand{\baselinestretch}{1}
\small\normalsize
\begin{center}
\large{\textbf{A NEURO-SYMBOLIC FRAMEWORK FOR
ACCOUNTABILITY IN
PUBLIC-SECTOR AI}}\\
\ \\
\ \\
\large{by} \\
\ \\
\large{Allen Sunny} % Your full name in records
\ \\
\ \\
\ \\
\ \\
\normalsize
Thesis submitted to the Faculty of the Graduate School of the \\
University of Maryland, College Park in partial fulfillment \\
of the requirements for the degree of \\
Master of Information Management \\
2025
\end{center}
\vspace{7.5em}
\noindent Advisory Committee: \\
\hbox{\ }\hspace{.5in}Professor Ido Sivan-Sevilla, Chair/Advisor \\
\hbox{\ }\hspace{.5in}Professor Gabriel Kaptchuk \\
\hbox{\ }\hspace{.5in}Professor Jessica Vitak \\
\clearpage
%Copyright
\thispagestyle{empty}
\hbox{\ }
\vfill
\renewcommand{\baselinestretch}{1}
\small\normalsize
\begin{center}
\large{\copyright \hbox{ }Copyright by\\
Allen Sunny %Type your name as it appears in University records
\\
2025}
\end{center}
\vfill
\newpage
%Acknowledgments
\renewcommand{\baselinestretch}{2}
\small\normalsize
\hbox{\ }
\vspace*{-.85in}
\begin{center}
\large{Acknowledgments}
\end{center}
\vspace{1ex}
I am deeply grateful to my advisor, Professor Ido Sivan-Sevilla, for his guidance, trust, and commitment to my growth throughout this project. His mentorship has shaped both my work and my development as a researcher. I would also like to thank my committee members, Professor Jessica Vitak and Professor Gabriel Kaptchuk for their time, support, and thoughtful feedback during this process.
Special thanks to the faculty and staff of the University of Maryland’s iSchool for creating a rigorous and supportive academic environment that has allowed me to pursue interdisciplinary research at the intersection of law, public policy, and artificial intelligence.
I am grateful to my friends and peers who shared this journey with me and offered encouragement on the days it mattered most. Finally, I owe the deepest thanks to my family, whose unwavering love and belief in me have carried me through every challenge. None of this would have been possible without them.
%List of Abbreviations
\renewcommand{\baselinestretch}{1}
\small\normalsize
\hbox{\ }
\vspace{-.6in}
\begin{center}
\large{List of Abbreviations}
\end{center}
\vspace{1em}
\begin{supertabular}{ll}
ABox & Assertional Component (Case Facts) \\
AI Act & European Union Artificial Intelligence Act \\
GDPR & General Data Protection Regulation \\
HCXAI & Human-Centered Explainable Artificial Intelligence \\
JSON & JavaScript Object Notation \\
KG & Knowledge Graph \\
LLM & Large Language Model \\
MPP & Manual of Policies and Procedures \\
NOA & Notice of Action \\
NLP & Natural Language Processing \\
OECD & Organisation for Economic Co-operation and Development \\
OSTP & Office of Science and Technology Policy \\
SMT & Satisfiability Modulo Theories \\
SNAP & Supplemental Nutrition Assistance Program \\
TBox & Terminological Component (Ontology) \\
UMAP & Uniform Manifold Approximation and Projection \\
USDA & United States Department of Agriculture \\
XAI & Explainable Artificial Intelligence \\
%$\alpha$ & alpha \\
%$\beta$ & beta \\
%& \\
%IREAP & Institute for Research in Electronics and Applied Physics \\
%NSA & National Security Agency
\end{supertabular}
\chapter{Introduction}
\label{chap:introduction}
\section{Motivation and Context}
Over the past few years, government service delivery has come under increasing strain. Economic instability, rising living costs, and global supply disruptions have driven more households to seek public assistance programs such as food benefits and childcare support~\cite{denvir1975controlling}. At the same time, administrative budgets and staffing capacity have not kept pace with demand. Facing higher workloads with fewer resources, agencies have increasingly turned toward automation to maintain service delivery~\cite{leslie_understanding_2019}. The rapid advancement of artificial intelligence and machine learning has accelerated this shift, encouraging the adoption of automated decision systems with the promise of efficiency and consistency~\cite{citron_technological_2008}.
However, integrating machine learning into public-benefit decision making introduces serious risks~\cite{bednarz_automated_2023}. Advanced predictive systems are often opaque, making it difficult or impossible to understand how eligibility decisions are reached. Decisions that cannot be explained cannot be meaningfully challenged, restricting applicants’ rights to contest errors that may deny them essential support. As automation expands without clear mechanisms for oversight, there is a growing concern that those most marginalized in society may be disproportionately harmed by incorrect or unreviewable determinations.
\section{Problem Statement and Research Gap}
Automated eligibility systems increasingly rely on predictive models whose internal logic does not correspond to the statutory rules that determine access to public benefits. Eligibility criteria are expressed in complex legal language, while model reasoning is framed in statistical terms. This disconnect means that explanations provided by AI systems may appear plausible yet fail to reference the required legal authority or may misstate the conditions under which benefits should be granted.
Without a shared legal structure, neither applicants nor administrators can determine whether an automated decision is justified under the law. Current explainability methods reveal correlations and model influence, but they cannot assess whether a decision reflects the correct statutory requirements or violates eligibility constraints. This gap highlights a fundamental accountability problem: explanations must be legally valid and not just interpretable, if automation is to preserve due-process rights in public-benefit administration.
\section{Research Questions}
Motivated by this gap, this thesis investigates the following research questions:
\begin{itemize}
\item \textbf{RQ1 — Representation:} How can statutory eligibility rules be structured into a computable form that preserves their legal semantics and hierarchical constraints?
\item \textbf{RQ2 — Alignment:} How can model-generated explanations be translated into these legal structures so that the reasoning behind decisions is expressed in terms of the law?
\item \textbf{RQ3 — Verification:} How can eligibility explanations be automatically tested for legal compliance, detecting when they satisfy or violate statutory requirements?
\end{itemize}
\section{Scope of Algorithmic Systems}
This thesis focuses on automated decision systems used in public-benefit eligibility
determination, where inputs, outputs, and governing rules are public by statute. These
systems differ from commercial predictive models in that: (1) their operational logic is
constrained by legally defined eligibility criteria\cite{Zhu2025_OversightDesignAIEnabledADM}, (2) agencies are obligated to provide
explanations grounded in statutory authority\cite{Justia_InformalRulemaking}, and (3) determinations are subject to
administrative review and appeal \cite{review_rulemaking_nodate}. The proposed framework therefore applies to contexts
with formal legal mandates and observable decision rationales, rather than discretionary or
proprietary systems.
\section{Contributions}
To address these questions, this thesis introduces a legally grounded explainability framework for automated eligibility decisions in public-benefit programs. This work provides the following contributions:
\begin{enumerate}
\item A \textbf{legal ontology} modeling statutory rules and constraints from the California Manual of Policies and Procedures (MPP), enabling a formal representation of eligibility law (RQ1).
\item A \textbf{semantic alignment method} that converts neural model explanations into structured rule assertions compatible with the ontology (RQ2).
\item A \textbf{formal reasoning workflow} using satisfiability-based verification to determine whether explanations are legally compliant or in violation (RQ3).
\end{enumerate}
\section{Thesis Structure}
The remainder of this thesis details the design and evaluation of this approach. Chapter~\ref{chap:litreview} reviews relevant work at the intersection of explainability, algorithmic governance, and computational law. Chapter~\ref{chap:system} presents the system architecture, including legal knowledge representation, explanation alignment, and verification mechanisms. Chapter~\ref{chap:results} evaluates system performance on CalFresh eligibility cases. Chapter~\ref{chap:discussion} discusses broader implications for policy and human-centered oversight. Chapter~\ref{chap:conclusion} concludes by outlining limitations and future directions.
\chapter{Literature Review}
\label{chap:litreview}
The increasing automation of welfare and other public-benefit systems has generated parallel research trajectories in law, social science, and artificial intelligence, each grappling with the problem of how to make algorithmic decisions accountable. This chapter reviews those literatures to situate the problem of legally grounded explainability within broader debates on administrative automation and responsible AI. It traces how public agencies’ turn toward data-driven decision-making; reconfigures foundational legal obligations of due process and reason-giving, and how existing technical approaches to explainability only partially meet those obligations.
The review proceeds in eight sections. Section 2.1 traces the historical evolution of welfare automation and the administrative pressures that drove the adoption of eligibility technology. Section 2.2 examines the harms observed in deployed systems, highlighting how opacity and rigid rule execution undermine due-process protections. Section 2.3 outlines the legal foundations of explainability, emphasizing reason-giving as a core requirement of administrative legitimacy. Section 2.4 reviews explainability approaches in artificial intelligence and analyzes why they fall short in legally constrained decision-making. Section 2.5 introduces legal ontologies and symbolic reasoning as methods for representing statutory structures in machine-interpretable form. Section 2.6 surveys neuro-symbolic approaches that integrate language interpretation with constraint-based verification. Section 2.7 brings these strands together to identify the technical and legal requirements for verifying eligibility explanations. Finally, Section 2.8 summarizes the research gap: although explainability tools and legal reasoning systems have advanced significantly, few frameworks ensure that automated justifications are not only interpretable but legally valid.
By mapping this interdisciplinary terrain, the chapter establishes the conceptual foundation for the framework proposed in later chapters, a neuro-symbolic system that operationalizes the law’s reason-giving mandate within computational architectures.
\section{SNAP and the Motivation for Welfare Automation}
\label{sec:21}
The Supplemental Nutrition Assistance Program (SNAP)\cite{USDAFNS_SNAP_Overview} is the largest food-assistance program in
the United States, providing monthly benefits that enable low-income households to purchase
groceries. Participation is based on meeting statutory eligibility criteria that reflect both financial
need and household circumstances, including income, residency, citizenship, resources student status etc. As an entitlement program, benefits must be issued to every
individual who qualifies; errors in eligibility determination therefore put applicants at risk of losing
access to basic subsistence needs.
In California, SNAP operates under the name \textit{CalFresh}\cite{CDSS_CalFresh}. Eligibility determinations are governed
by the California Manual of Policies and Procedures (MPP) Division~63\cite{CDSS_CalFreshRegs}, which translates federal and
state statutory requirements into detailed administrative rules. When a decision is made, counties
must issue a Notice of Action (NOA)\cite{CDSS_NOA_Docs} that explains the legal basis for an approval, denial, reduction,
or termination of benefits. Because internal decision processes may be automated or otherwise
opaque, the NOA is often the only publicly visible justification for how eligibility rules were applied to
a particular household. As a result, the NOA serves as the central accountability mechanism through
which applicants can understand, challenge, or correct decisions that affect their access to food.
SNAP and state-administered programs like CalFresh operate under increasing strain\cite{veale2019administration} . Rising living
costs, economic volatility, and staffing shortages have expanded caseloads while shrinking the
resources available to process them efficiently \cite{larsson_digitization_2021}. To maintain service
delivery at scale, welfare agencies have increasingly turned to automation, first through business
rules and case-management software, and more recently through machine learning systems \cite{zajko_automated_2023}. These tools promise efficiency and uniformity, but they also intensify longstanding challenges in welfare
administration: when eligibility reasoning is encoded in technical infrastructure, the rules guiding
determinations can become opaque to those directly affected \cite{keiser_understanding_2010,
sorensen_ideational_2024}.
This shift does not represent a sudden rupture but an acceleration of a decades-long trajectory.
Performance-management pressures and “audit culture” reframed social rights as data-management
problems, prioritizing throughput and fraud detection over deliberative casework
\cite{eubanks_automating_2018}. Even before digitization, standardized
paperwork and regulatory checklists had already created a proto-automated bureaucracy. Modern
AI systems extend this history by further obscuring how rules, exceptions, and case facts are applied
\cite{hoglund_ryden_hidden_2023}. As automation becomes central to CalFresh delivery, ensuring
that decision systems remain transparent and legally accountable is essential for protecting due-
process rights.
These concerns are not isolated to CalFresh: across the welfare state, automated eligibility systems
have produced improper denials, opaque decision-making, and substantial harm to beneficiaries
when the legal basis for decisions is inaccurate or unclear\cite{calo_automated_2021}.
\section{Current Failures and Controversies in deployed systems}
\label{sec:23}
Despite promises of efficiency and accuracy, automated eligibility systems in welfare administration have repeatedly produced large-scale harms\cite{greener_changing_2022} . These are not isolated technical errors but structural failures that arise when bureaucratic discretion is replaced by rigid code. Once eligibility rules are converted into executable logic, they lose the interpretive flexibility that caseworkers once exercised, allowing minor data inconsistencies or procedural lapses to cascade into automatic denials.
The Michigan Integrated Data Automated System (MiDAS), for example, used rule-based pattern matching to detect unemployment fraud between 2013 and 2015. Operating with no human oversight, it falsely accused roughly 40,000 people of fraud and automatically imposed severe penalties, later ruled to violate due-process rights \cite{michigan_audit_2016}. A similar pattern occurred in Indiana’s 2007 Welfare Modernization Project, where privatized eligibility software interpreted missing paperwork as “failure to cooperate,” triggering mass benefit terminations before the contract was cancelled \cite{heinrich_indiana_2022}. Comparable dynamics have appeared in California’s CalWIN and CalSAWS systems, where county auditors and advocates have reported data mismatches, opaque eligibility rules, and automatically generated notices that omit the governing legal citation\cite{CaliforniaStateAuditor_2019_FederalComplianceAudit}.
Across these cases, several mechanisms of failure recur. Opacity prevents both applicants and agencies from inspecting the logic of decision rules embedded in proprietary code.\cite{brauneis2018algorithmic} Procedural drift occurs when software updates modify eligibility conditions without parallel legal review.\cite{wu_meyer_iza_2024} Administrative burden shifting transfers work to claimants, who must verify and correct data through digital portals.\cite{herd_introduction_2023} Data fragility allows trivial inconsistencies to trigger denials because systems interpret uncertainty as non-compliance.\cite{rox818_when_2025} And vendor capture leaves public agencies dependent on private contractors, weakening accountability and transparency. \cite{hickok_public_2022}
Beyond initial determinations, automation has profoundly altered the landscape of appeal and redress. \cite{hoglund_ryden_hidden_2023} In traditional welfare administration, applicants could challenge an adverse decision by presenting new evidence, clarifying documentation, or engaging directly with caseworkers who understood the program’s logic. \cite{bovens_street-level_2002} Automated eligibility engines, however, often produce determinations without a transparent reasoning trace, leaving both claimants and frontline staff unable to identify the source of error. When an applicant appeals, administrators must reconstruct decisions from incomplete data logs or vendor-controlled audit trails, a process that converts legal review into forensic debugging. The opacity of proprietary code and the rigidity of rule-based engines mean that even successful appeals tend to address symptoms rather than systemic flaws \cite{lipsky_street_1980} . In some jurisdictions, automated denials trigger appeal backlogs so large that relief arrives only after benefits have lapsed, effectively nullifying the right to timely redress. The very procedures intended to guarantee fairness thus become absorbed into the same computational architecture that produced the harm, illustrating how algorithmic administration compresses not only discretion but also contestability within bureaucratic systems.
Collectively, these controversies reveal how automation transforms the epistemic structure of welfare governance. Algorithmic systems optimize for throughput and standardization but erode the reason-giving practices that administrative law demands. The result is a widening gap between computational and legal rationality, between decisions that are efficiently produced and those that are procedurally justified.
\section{Legal and Regulatory Foundations for Explainability}
\label{sec:22}
Explainability in automated decision-making is no longer only a design preference or ethical aspiration; it is increasingly codified as a legal obligation. Across jurisdictions, legislators and courts are beginning to treat algorithmic explanation as a procedural right that ensures accountability, transparency, and the possibility of redress. \cite{gdpr2016art22} Although these frameworks differ in scope and philosophy, they share a common premise: when state or corporate actors rely on automated reasoning, they must be able to justify those decisions in a manner intelligible to affected individuals and reviewable by oversight bodies.
\subsection{Data-Protection and Rights-Based Approaches}
The most influential articulation of a legal “right to explanation” originates in European data-protection law. Article 22 of the General Data Protection Regulation (GDPR) \cite{gdpr2016art22} establishes that individuals shall not be subject to decisions based solely on automated processing that significantly affect them, while Recital 71 \cite{gdpr2016_679} mandates that such processing be accompanied by “meaningful information about the logic involved.” Scholars have debated the strength of this provision whether it creates a substantive right to explanation or merely procedural transparency~\cite{doshi-velez_towards_2017}, \cite{wachter_why_2017} yet it nonetheless set the global benchmark for algorithmic accountability. National implementations, such as France’s Digital Republic Act (2016) \cite{france_law_digital_republic_2016}, go further by requiring public authorities to disclose the data sources and parameters used in automated decisions. Outside Europe, Canada’s Directive on Automated Decision-Making (2020) \cite{canada_directive_automated_decision_making_2020} and Brazil’s LGPD (2020) \cite{LGPD_2018} incorporate similar duties of transparency and contestability. Rights-based regimes thus frame explainability as an instrument of informational self-determination: individuals must be able to understand and challenge the reasoning that affects their legal or economic standing.
\subsection{Administrative-Law and Due-Process Traditions}
In the United States, obligations of explanation emerge not from data-protection statutes but from administrative and constitutional law. The Administrative Procedure Act (APA § 706) \cite{chen_understanding_2020} requires agencies to provide a “reasoned explanation” for their actions, a doctrine that courts enforce through the “arbitrary and capricious” standard of review. Landmark welfare cases such as \cite{goldberg_v_kelly_1970} and \cite{Califano_v_Yamasaki_1979} established that recipients of public benefits are entitled to notice and an opportunity to contest before deprivation. Scholars like \cite{citron_technological_2008} and \cite{waldman2019power} have extended these principles into the digital realm under the banner of technological due process, arguing that when algorithms replace human discretion, they must still furnish the procedural safeguards , explanations, hearings, and review that due process demands. Within this tradition, explainability is not a matter of user comprehension but a constitutional mechanism that preserves the rule of law within automated administration.
\subsection{Sector-Specific and Emerging AI Regulation}
Beyond these foundational doctrines, a new generation of AI-specific regulations seeks to institutionalize explainability through design and documentation mandates. The EU AI Act (2024) \cite{EU_AI_Act_2024} classifies welfare, credit, and law-enforcement algorithms as “high-risk,” obliging providers to maintain technical documentation, traceability logs, and human-oversight procedures that make system logic auditable. The OECD AI Principles (2019)\cite{OECD_AI_Principles} and the UNESCO Recommendation on the Ethics of AI (2021) \cite{UNESCO_2021_RecommendationEthicsAI} reinforce similar expectations of transparency, accountability, and contestability. In the United States, the proposed Algorithmic Accountability Act (2023)\cite{sen_wyden_s2892_2023} and the White House Blueprint for an AI Bill of Rights (2022) \cite{AI_Bill_of_Rights_2022} advance parallel requirements: notice to individuals, explanations of automated decisions, and the ability to opt for human review. These instruments shift the regulatory emphasis from voluntary corporate disclosure to mandatory procedural justification, making explainability a condition of lawful deployment.
The principle that public authorities must provide reasons for their decisions lies at the core of modern administrative governance and the rule of law. Legal theorists from Lon Fuller to Jerry Mashaw have long argued that procedural fairness, not merely the correctness of outcomes legitimizes bureaucratic power \cite{mashaw_is_2020}.
\cite{fuller_morality_1969} described this as part of the “inner morality of law”: a lawful system must generate intelligible and contestable reasons if it is to remain non-arbitrary. \cite{goldberg_v_kelly_1970} later extended this within the U.S. administrative state, emphasizing that legitimacy arises from reason-giving procedures that enable affected individuals to understand and challenge state action.
In administrative law, this obligation is operationalized through due process; The right to notice, an explanation, and an opportunity to contest. \cite{goldberg_v_kelly_1970} established that welfare benefits cannot be terminated without prior notice and a fair hearing, confirming that government determinations are acts of legal judgment that must be articulated and reviewable.
Applied to contemporary welfare automation, these doctrines make explainability a procedural right rather than a design preference. When algorithmic systems determine eligibility, the duty to “give reasons” transfers from the human caseworker to the system’s architecture.\cite{review_administrative_nodate} The state’s accountability thus depends on computational traceability: affected individuals must be able to see which statutes and factual predicates governed their case and how those were applied.
\subsection{The Erosion of Procedural Reasoning}
As agencies replace human adjudication with digital infrastructure, the practical capacity to give reasons has eroded. What was once a dialog exchange between citizen and caseworker has become an impersonal data transaction \cite{bovens_street-level_2002}. Applicants now receive automated notices of approval or denial, but rarely the reasoning or legal provisions that produced those outcomes. The obligation to explain persists, yet its execution is displaced into software architectures never designed to fulfill it\cite{simkute_explainability_2021}.
Scholars describe this transformation as a technological due-process failure. When automated systems replicate administrative functions without embedding the notice-and-hearing safeguards required by law, state action becomes procedurally illegible. \cite{citron_technological_2008} identifies the paradox: algorithms can implement formal logic precisely while remaining unaccountable because their inner operations are inaccessible to those they govern.
In welfare contexts, proprietary vendor contracts and fragmented data integrations deepen this opacity. Administrators themselves often cannot reconstruct why a decision was made, let alone communicate that reasoning to claimants \cite{brauneis2018algorithmic}. Oversight mechanisms, appeals, judicial review, legislative inquiry presume an interpretable record of reasoning. Automated systems frequently lack such records, producing outcomes without a traceable path from facts to legal norms. As a result, the meaningful opportunity to be heard promised by \cite{goldberg_v_kelly_1970} collapses into a purely procedural formality.
These failures reflect not only gaps in usability but a deeper structural issue: automated eligibility systems lack a computable representation of legal rules that would enable them to produce justified and reviewable determinations.
\subsection{Toward Legally Grounded Explainability}
Legal accountability requires more than transparency; it requires reasoned justification that maps outcomes to their normative sources. In administrative contexts, an explanation is adequate only if it demonstrates consistency with the statutes, regulations, or policy provisions that authorize it. Explainability must therefore evolve from a cognitive aid into a form of juridical traceability, the ability to show, in formal terms, that a system’s reasoning aligns with the law\cite{nay_law_2023} \cite{prajescu_argumentation-based_2025}.
This insight points toward a new class of technical solutions that integrate computational reasoning with legal logic. Rather than treating explainability as a human-factors problem, these methods conceive of it as a compliance mechanism. By aligning algorithmic outputs with explicit rule representations, a decision system can serve as a procedural interface that upholds due-process obligations \cite{mansi2025legally}.
Bridging this gap requires hybrid architectures that combine semantic interpretation with formal verification i.e. linking the flexibility of natural-language to the rigidity of logical constraint solving. Such approaches move explainability beyond narrative description toward computational justification.
In automated eligibility systems, explainability is not simply a matter of model transparency but a legal
duty of justification. Determinations must articulate how specific statutory requirements were applied
to the facts of a case. Meeting this obligation in computational settings requires technical mechanisms
capable of representing legal rules and verifying that decisions conform to them. The following sections
examine technical methods of explainability and their various limitations.
\section{Limitations of Technical Explainability}
\label{sec:25}
Over the past decade, the field of explainable artificial intelligence (XAI) has developed a wide range of methods designed to render machine learning models interpretable to humans. These techniques fall broadly into two categories: post-hoc explainability, which attempts to approximate the reasoning of an already trained model, and intrinsic explainability, which designs interpretability directly into the model architecture. Both paradigms share an epistemic goal that is to make black-box systems more intelligible. But they differ in their mechanisms and, more importantly, in their suitability for legally accountable decision-making.
\subsection{Post-hoc Approaches}
Post-hoc methods generate explanations after a model has made its prediction. Tools such as LIME~\cite{ribeiro_why_2016} and SHAP~\cite{muschalik_shapiq_2024} exemplify this approach. They construct local approximations around an instance to show which input features most influenced the outcome. Other variants, like counterfactual explanations~\cite{verma2020counterfactual}, describe how small input changes could yield a different result, while influence functions and feature attribution scores trace contributions back to training data. These approaches are widely used because they are model-agnostic and computationally efficient. However, they explain how a model reached a result, not whether that result accords with law or policy ~\cite{freiesleben_scientific_2024}.
\vspace{-0.05em}
\begin{figure}[H]
\centering
\includegraphics[width=0.65\textwidth]{Tex/Figures/SHAP_Importance.png}
\caption[Example XAI Output: SHAP Explanation]{Example of a SHAP (SHapley Additive Explanations)
plot illustrating how model features contribute to a specific eligibility decision. Each bar represents a feature’s marginal contribution to the model’s prediction
relative to a baseline expectation. While such visualizations provide insight into which inputs the
model deemed influential, they do not indicate whether the reasoning aligns with statutory
requirements or references the correct legal conditions.}
\label{fig:architecture}
\end{figure}
\subsection{Intrinsic Approaches}
Intrinsic or interpretable-by-design models, such as decision trees, rule lists, or monotonic generalized additive models, embed interpretability directly into their structure. Because their internal logic can be directly inspected, these models offer greater transparency and auditability than deep neural networks. Yet, in high-stakes administrative contexts, they remain insufficient. Even a perfectly transparent model may still apply criteria that lack a legal basis. Interpretability, in this sense, is not equivalent to accountability. As ~\cite{rudin_stop_2019} notes, a decision system can be “transparent but illegitimate” if it offers reasons unmoored from the normative frameworks that authorize them.
\subsection{Human-Centered XAI}
Recent work in human-centered explainable AI (HCXAI) ~\cite{mueller_explanation_2019} reframes explainability as a relational and contextual process rather than a purely technical property of models. Instead of treating explanations as outputs to be visualized, HCXAI examines how explanations function within human decision-making ecosystems, what users need to understand, contest, or trust a system.~\cite{liao2021human} emphasized that good explanations are social acts, shaped by conversational norms and cognitive expectations. Subsequent frameworks~\cite{ehsan_expanding_2021} extend this perspective to emphasize user goals, institutional settings, and power asymmetries. In public administration, this lens is crucial: the “user” is not merely a data scientist interpreting a model but an applicant, caseworker, or judge navigating rights and responsibilities. HCXAI thus shifts the design focus from explainability for insight to explainability for agency enabling affected parties to understand, challenge, and remedy algorithmic decisions. This human-centered orientation complements but does not replace legal grounding; rather, it provides the procedural scaffolding through which legally meaningful explanations can be communicated and acted upon.
While HCXAI emphasizes the communicative and social dimensions of explanation, it still assumes that the underlying decision logic is available to be interpreted. In legally regulated domains, however, explainability must also be formally grounded i.e., anchored to statutes, regulations, and eligibility criteria that define what counts as a valid decision. To ground human-centered explainability in statutory authority, we require representational structures that can encode legal norms in machine-interpretable form.
\subsection{Limitations for Legal Contexts}
Across all paradigms, the prevailing assumption is that explainability is a cognitive aid—a means for users or auditors to understand model behavior. In contrast, public-benefit administration requires normative traceability: the ability to show that an outcome is consistent with governing law. Existing XAI methods cannot guarantee such alignment because they operate in a space of statistical correlation rather than formal obligation. They may approximate reasoning, but they do not encode the rules that confer legal validity. In effect, XAI techniques provide interpretive clarity, whereas administrative law demands procedural justification.
To move from interpretability to legality, decision systems must represent the concepts, thresholds, and dependencies that define eligibility in formal terms. This shift turns attention from post-hoc interpretive tools to knowledge representations capable of expressing the structure of law itself.
\section{Legal Ontologies and Symbolic Reasoning}
\label{sec:27}
To satisfy the legal duty of reason-giving, automated decision systems must do more than interpret data; they must represent the law itself. Legal ontologies and symbolic reasoning frameworks respond directly to this requirement by encoding the concepts, thresholds, and hierarchical dependencies that govern eligibility. Rather than explaining how a model behaves, they formalize why a decision is authorized, grounding computational outcomes in explicit normative structures.
In artificial intelligence and knowledge representation, an ontology is a formal specification of how entities within a domain are categorized and related to one another ~\cite{baader2010dlhandbook}. It articulates a shared conceptualization of reality, defining the classes (types of things), relations (how those things connect), and axioms (constraints that must hold true) that together describe a domain’s structure.
Gruber defines an ontology as “an explicit specification of a conceptualization”~\cite{gruber_translation_1993}, positioning ontologies as a bridge between human semantic categories and the formal structures required for computational reasoning in legally regulated domains. Over time, several representational standards have emerged to encode such knowledge structures, ranging from the Resource Description Framework (RDF) ~\cite{w3c1999rdfsyntax}, which expresses knowledge as subject–predicate–object triples, to the Web Ontology Language (OWL) ~\cite{W3C_OWL2_2012}, which builds on RDF to support richer logical semantics based on Description Logic. Prominent examples include the Gene Ontology \cite{GeneOntology_Overview} for biological processes, SUMO (Suggested Upper Merged Ontology) ~\cite{SUMO_OntologyPortal} for general reasoning across domains, and PROV-O ~\cite{W3C_PROV_O_2013} for provenance modeling on the semantic web. Within the legal domain, such frameworks have inspired specialized ontologies that formalize normative relations and procedural hierarchies, making the implicit structure of legal reasoning explicit. This formalization enables consistent interpretation across systems and supports reasoning tasks that depend on understanding both the semantics of legal terms and their logical interdependencies.
Research in AI and Law has long explored how legal reasoning might be expressed in computational form. Early expert systems such as TAXMAN ~\cite{mccarty_reflections_1976} and SHYSTER~\cite{popple_shyster_1993} demonstrated that statutory interpretation could be modeled through rule-based logic, yet they also exposed law’s resistance to full formalization. Legal norms are context-sensitive, exception-laden, and hierarchically organized; symbolic representations could capture syntactic rules but not the pragmatic reasoning that human adjudication requires.
From these limitations emerged the field of legal knowledge representation, which sought to separate the structure of legal concepts from the logic of their application. The development of ontologies which are formal, machine-readable vocabularies of legal entities and relations, was central to this shift. Frameworks such as LKIF-Core (Legal Knowledge Interchange Format) ~\cite{hoekstra2007lkif}, LegalRuleML ~\cite{wang_legalreasoner_2024}, and other OWL-based models introduced standardized methods for describing legal domains, defining hierarchical relationships among concepts, and encoding dependencies between rules. These ontological frameworks allowed legal knowledge to be represented with greater precision and interoperability, enabling reasoning engines to perform tasks such as compliance checking, conflict detection, and inference of legal consequences. In doing so, they transformed legal texts from static documents into structured knowledge bases that could be computationally queried and analyzed. This formalization provided a foundation for a new class of reasoning systems: once legal rules were expressed as explicit logical statements, they could be subjected to automated verification and consistency checking.
Satisfiability Modulo Theories (SMT) ~\cite{hutchison_satisfiability_2009} frameworks extend this line of work by providing the computational mechanism to evaluate whether those formalized legal constraints can be jointly satisfied under given factual conditions. Whereas ontologies specify what entities and relationships exist in a legal domain, SMT reasoning tests whether the instantiated facts comply with those logical structures. By combining propositional logic with domain-specific theories, such as arithmetic, temporal relations etc. SMT solvers can evaluate both qualitative and quantitative conditions (for example, determining whether a household’s income and expenses satisfy statutory thresholds, or whether overlapping obligations produce contradictions). In this sense, SMT reasoning operationalizes the normative content encoded in legal ontologies: it converts the declarative structure of law into a testable system of constraints, enabling computational models to verify rule compliance and detect violations.
Ontological and constraint-based approaches together have become foundational for tasks such as normative reasoning, legal information retrieval, and automated compliance checking. Process auditing systems like Regorous~\cite{governatori2015regorous} integrate both layers, representing legal norms through formal ontologies and enforcing them through SMT-based constraint solving. Others employ logical reasoners to infer legal consequences or detect rule conflicts~\cite{khang_automating_defeasible_2022, judson_put_2024}. Collectively, this body of work demonstrates that symbolic models can render the structure of law explicit and computationally tractable. Yet scholars continue to note their fragility \cite{lim_automating_2022}: they rely on exhaustive rule enumeration, require expert maintenance, and often remain disconnected from the natural-language texts and socio-legal contexts that give those rules meaning.
The the extent to which legal rules can be exhaustively formalized remains contested. Statutory eligibility criteria often contain discretionary clauses, temporal dependencies, and exception handling that resist complete specification in symbolic form. As a result, current systems typically focus on the operational core of legal rules, leaving substantial interpretive work to human administrators or adjudicators \cite{libal_legal_2023}.
Recent studies have therefore begun to explore hybrid approaches, linking ontological representationswith natural-language processing or statistical learning to bridge the gap between textual norms and formal reasoning~\cite{wan_towards_2024} and~\cite{gibaut_neurosymbolic_2023}. These efforts mark a broader turn toward executable semantics in law, an attempt to make legal norms both interpretable and machine-actionable. The convergence of symbolic logic and semantic representation provides the conceptual foundation for emerging neuro-symbolic models that aim to integrate interpretability with normative verification.
\section{Neuro-Symbolic Methods}
\label{sec:28}
As automated decision-making expands into public services, there is a growing need for systems that can both interpret natural-language reasoning and ensure consistency with formal constraints. Neuro-symbolic AI offers a pathway to bridge this gap by combining neural learning with symbolic reasoning~\cite{gibaut_neurosymbolic_2023}. Neural architectures extract structured meaning from free-text explanations, while symbolic solvers provide precise mechanisms to evaluate whether those interpretations align with rule-governed requirements.
\subsection{Neuro-Symbolic Verification in Practice}
Neuro-symbolic systems have demonstrated value in settings where behavioral errors carry significant risk and correctness must be formally established. Frameworks such as Logic Tensor Networks (LTNs)~\cite{badreddine_logic_2022} and DeepProbLog~\cite{manhaeve_deepproblog_2018} incorporate logical constraints directly into neural inference, ensuring that predictions obey domain-specific structure rather than unconstrained statistical associations.
More recent pipelines connect large language models to verification systems. For example, LLM-plus-solver architectures~\cite{sadowski_explainable_2025} where neural models extract candidate rules or explanations from natural language, and symbolic solvers check the satisfiability of those claims. These workflows have been applied to visual reasoning tasks\cite{dong_neural_2019}, scientific discovery\cite{lv2022xdmimprovingsequentialdeep}, and automated theorem proving\cite{rao2025neuraltheoremprovinggenerating}, demonstrating that neural interpretations can be systematically tested against external logical constraints rather than accepted at face value. Collectively, these approaches show that learned systems can be made subject to explicit rule auditing, offering stronger assurances than post-hoc interpretability alone.
\subsection{Legal Applications of Neuro-Symbolic Systems}
Legal domains have begun to explore neuro-symbolic models that align language interpretation with normative rule structures. Neural systems can identify legally operative concepts, clause boundaries, and exceptions from regulatory or adjudicatory text~\cite{noguer_i_alonso_automating_2024}. Symbolic solvers then verify whether extracted assertions satisfy formally expressed requirements~\cite{wang_python_2024}. Related approaches combine rule extraction with constraint validation—e.g., LLM + Z3 or LLM + Prolog pipelines~\cite{wang_python_2024, calanzone_logically_2024}—verifying whether the logic behind a textual explanation is complete and consistent. Across these efforts, neural networks interpret legal language while symbolic reasoning safeguards legal fidelity.
\section{Toward Legal Verification of Eligibility Explanations}
\label{sec:29}
In government benefit programs, an explanation is not merely a transparency artifact: it is a legally operative justification determining whether a person receives essential support~\cite{citron_technological_2008, eubanks_automating_2018}. Eligibility decisions must reference statutory authority and provide a basis for appeal. Ensuring that automated explanations meet these obligations requires more than interpretability—it requires verification that a justification conforms to governing law. Neuro-symbolic approaches provide the core technical foundation for such oversight by enabling both the extraction of decision rationales and the formal evaluation of their legal correctness~\cite{calanzone_logically_2024}.
\section{Summary}
\label{sec:210}
Across the bodies of scholarship reviewed in this chapter, a common trajectory emerges:
automation has re-engineered the procedural foundations of welfare administration, while law and
computer science have struggled to keep pace. Sociotechnical studies reveal how algorithmic
systems optimize efficiency at the expense of transparency; legal theorists frame explanation as a
right essential to due process; and technical research offers increasingly sophisticated methods for
interpretability and verification. Yet these literatures remain fragmented. Legal frameworks articulate
why explanations are required, while XAI and symbolic-reasoning frameworks explore
how they might be produced, but few attempts reconcile the two within a single architecture.
Existing explainability tools clarify statistical correlations within model behavior but cannot
demonstrate that a decision is legally grounded. Conversely, formal verification ensures logical
consistency but often neglects the semantic commitments and contextual constraints encoded in
statutory rules. As a result, current approaches cannot determine whether an automated eligibility
decision is legally justified or identify when a violation of statutory requirements has occurred.
This gap between interpretability and legality defines the frontier of responsible automation.
Bridging this divide requires a unified approach that represents statutory obligations in computable
form and ensures that the reasoning behind automated decisions remains accountable to those
obligations. The next chapter introduces a system architecture designed to operationalize this
principle by linking model explanations to the law they are intended to enforce.
\chapter{System Design and Methodology}
\label{chap:system}
\section{Motivation for System Design}
The architecture in this chapter directly operationalizes the research questions presented in
Chapter~\ref{chap:introduction}. To determine whether eligibility explanations are legally grounded, the
system must satisfy three requirements:
\begin{enumerate}
\item \textbf{Represent statutory authority in computable form (RQ1).}
The system must capture eligibility law in a way that preserves legal semantics, constraints, and
exceptions. This motivates the construction of a formal legal representation (TBox).
\item \textbf{Express case reasoning using the same legal structure (RQ2).}
Agency explanations must be translated into rule assertions that reference the correct statutory
conditions. This requires instantiating case facts and explanation-derived predicates within an
assertional layer (ABox).
\item \textbf{Verify whether reasoning complies with the law (RQ3).}
To support due-process review, the system must automatically identify when the asserted
reasoning satisfies or violates eligibility requirements. This motivates the integration of a solver-
based verification process.
\end{enumerate}
These requirements define the layered design of the system: legal representation, explanation
alignment, and automated verification. The following section provides a high-level overview of how
these components interact to support legally accountable decision automation.
\section{System Overview}
At the core of the framework is a structured representation of legal reasoning based on two layers of knowledge. The TBox or “Terminological Box”, which encodes the statutory rules governing CalFresh eligibility, and the ABox or “Assertional Box”, which represents the factual and justificatory content of an individual case.
The TBox contains the ontology and formal rules derived from MPP Division 63, defining the conditions under which applicants are eligible for benefits. This can be viewed as a shared translation layer that maps the vocabulary and grammar of the legal system into representations that are operable for both human and machine reasoning. The TBox is grown dynamically as legal statutes are fed into the system. A comprehensive list of ontology and rules can be found in the Appendix\ref{chap:Appendix}.
The ABox instantiates these rules with concrete case-level data. It contains two categories of assertions: (1) factual attributes describing the applicant’s circumstances, such as household size, income values, or whether verification was provided; and (2) explanation-based assertions, representing the conditions the decision rationale claims are relevant to the eligibility outcome. These explanation-derived assertions are expressed in the same legal vocabulary defined in the TBox, allowing them to be evaluated against statutory requirements. In this way, the ABox captures both the state of the world and the reasoning offered to justify the decision. The critical function of the ABox is therefore not only to represent case facts, but to make explicit the normative logic the explanation invokes, providing a structured basis for testing whether the stated reasoning aligns with the legal framework encoded in the TBox.
The TBox and ABox are jointly evaluated using a constraint-solving procedure. If the ABox assertions can satisfy all relevant TBox rules, the explanation is deemed legally coherent; if not, the solver identifies the specific statutory provisions that are violated. This architecture ensures that explanations are not only interpretable, but demonstrably aligned with the legal requirements that govern eligibility determinations. All of the data is modeled in a graphical representation commonly referred to as a knowledge graph\cite{hogan_knowledge_2022}. In this context, a knowledge graph is simply a structured network of legally relevant concepts (nodes) and the relationships between them (edges). Representing rules and case facts in this form ensures that the same legal vocabulary is used throughout the pipeline maintaining semantic consistency in how eligibility conditions are invoked. The graph structure also enables intuitive visualization of which statutory conditions are satisfied or
violated in a given case, supporting both human interpretability and procedural accountability.
% pulls the text up closer to the list
\vspace{-0.05em}
\begin{figure}[H]
\centering
\includegraphics[width=0.65\textwidth]{Tex/Figures/Total_Arch.jpg}
\caption{System architecture of the statutory explainability framework.}
\label{fig:System_architecture}
\end{figure}
\section{Data Sources and Case Construction}
The neuro-symbolic framework developed in this thesis relies on two foundational sources of knowledge: the California Department of Social Services Manual of Policies and Procedures (MPP), Division 63, and a structured dataset of CalFresh eligibility cases. The MPP serves as the authoritative legal foundation from which statutory rules and ontology elements are derived, while the case dataset provides the empirical grounding required to evaluate whether the system can accurately assess the legal sufficiency of decision explanations. Together, these sources establish a complete environment for testing legally grounded AI reasoning under realistic conditions, with the cases reflecting realistic sources of legal ambiguity and program administration, enabling evaluation of the system on decision types where accurate statutory justification is critical to due process.
\subsection{Statutory Corpus: California MPP Division 63}
Division 63 of the MPP codifies the administrative rules governing Supplemental Nutrition Assistance Program (CalFresh) eligibility across California. It defines the conditions under which households may qualify for food assistance, including requirements relating to household composition, income thresholds, allowable resources, residency in the administering county, citizenship or immigration status, reporting obligations, and eligibility for expedited services. These regulations are expressed in a hierarchical structure spanning sections, sub-sections, and clause-level normative obligations.
To enable machine reasoning, the official MPP publication was extracted in HTML format and segmented into JSON documents. Each record preserves the regulatory citation, raw and tokenized text for embedding, metadata such as the effective date of the provision, and explicit statutory references pointing to related sections. These cross-references are an important part of the legal logic: they establish dependencies between eligibility factors that must hold jointly for a decision to be lawful. Examples of the corpus structure can be found in the Appendix\ref{chap:Appendix}.
The structured statutory records were then imported into a legal knowledge graph using the graph database Neo4j, in which clauses function as nodes organized by the eligibility domain they regulate. Referenced provisions are connected as directed edges in the graph, preserving the relational architecture of the law as written. This representation enables retrieval of conceptually related rules during reasoning, supports traceability between logical rules and their authoritative statutory sources, and maintains legal structural integrity when evaluating consistency.
This statutory knowledge graph forms the foundation for constructing the terminology and rule set of the TBox, grounding every ontology concept and solver rule in a verifiable location within the MPP.
\begin{figure}[H]
\centering
\includegraphics[width=0.7\linewidth]{Tex/Figures/California_Laws.png}
\caption{A section of the statutory law as visualized in a knowledge graph}
\end{figure}
\subsection{Eligibility Case Dataset}
To evaluate the legal-reasoning capabilities of the framework, a dataset of forty-three CalFresh eligibility cases was assembled directly from publicly accessible administrative hearing documents and agency-provided examples of eligibility decision explanations. These materials already omit personal identifiers, and no sensitive household information is included; thus, no additional anonymization was required. Each case was re-encoded into a structured JSON format that captures only factual variables relevant to eligibility, for example, residence county, income values, verification status, and categorical eligibility flags as well as the explanation provided for the decision outcome.
This dataset therefore provides a realistic testbed for assessing whether the framework can identify the correct areas of law implicated by a decision explanation and determine whether that explanation is logically consistent with the governing requirements of CalFresh eligibility.
An example of the case file PDF can be found in the Appendix.
\section{Ontology Construction (TBox)}
The TBox, or terminological component, of the system captures the abstract schema of legal categories, relationships, and constraints that define eligibility under the California Manual of Policies and Procedures (MPP). Its purpose is to translate unstructured statutory language into a structured, machine-readable vocabulary that can later be instantiated with factual data in the ABox. To bridge system-level computation with human legal interpretation, the TBox is implemented as a legal ontology that preserves the meaning and hierarchy of statutory concepts while enabling their formal use in automated reasoning. This section describes how the ontology was designed, expanded, and embedded for downstream evaluation and verification.
\begin{figure}[H]
\centering
\includegraphics[width=0.4\linewidth]{Tex/Figures/Tbox_Arch_Diagram.drawio.png}
\caption{TBox Architecture diagram}
\end{figure}
\subsection{Ontology Design and Concept Hierarchy}
The hierarchy was derived directly from the legal organization of MPP Division 63. The MPP structures eligibility rules into major regulatory domains (e.g., income, residency, resources), each of which governs a legally distinct basis for eligibility. These top-level divisions were adopted as parent classes in the ontology to preserve the statutory separation of authority. This design decision follows the modeling conventions of LKIF-Core \cite{hoekstra2007lkif}, where legally operative concepts are encoded as classes reflecting distinct normative roles in decision-making.
Within each domain, subordinate concepts were identified by extracting defined eligibility conditions, named variables, and verification requirements from statutory clauses. Concepts were added only when they represented a legally operative element i.e a factor that can independently determine an eligibility outcome under CalFresh regulations. This operational emphasis is consistent with LKIF’s distinction between normative concepts (conditions that affect legal status) and descriptive facts (attributes without normative force).
Beyond organizing eligibility categories, the ontology also models the legally meaningful relationships between them. Each eligibility domain imposes conditions that reference or constrain attributes defined in other domains. For example, IncomeEligibility depends on HouseholdComposition to determine the household-specific income threshold, while ResidencyRequirement and CitizenshipStatus jointly define whether participation is permitted within a California county. These cross-domain dependencies are represented as object properties that capture how administrative decisions draw from multiple sources of statutory authority, again reflecting LKIF’s approach to encoding normative interactions rather than treating rules as isolated checks.
The ontology uses a two-level hierarchy consistent with LKIF’s intent to model only normatively relevant distinctions. The top level encodes legally independent eligibility domains; the second represents the concrete conditions required within each domain. No deeper subclassing was introduced, as the statutory structure does not assign normative weight to additional internal subdivisions (e.g., distinguishing between income verification and income limit provisions). This keeps the ontology aligned with how county eligibility workers reason: identifying the governing eligibility basis, then determining whether its required conditions are satisfied. The resulting structure provides a legally faithful conceptual foundation for the automated reasoning performed in later stages of the system.
\subsection{Vocabulary Creation}
\subsubsection{Define Seed Concepts}
The process is started by manually defining some of the key concepts for the ontology, concepts like IncomeEligibility, ResidencyRequirements , MedicalExpenses NetIncome etc. These are derived from the top subsections of the manual just to give a starting point for the vocabulary building process.The initial relationships between the sections was also derived.
The starting ontology JSON format is:
\begin{singlespace}
\begin{lstlisting}[language=json]
{
"Root": {
"subclasses": [
"IncomeEligibility",
"ResidencyRequirement",
"CitizenshipStatus",
"HouseholdComposition",
"ResourceEligibility",
"WorkRequirement"
]
},
"IncomeEligibility": {
"attributes": [
"GrossIncome",
"NetIncome",
"IncomeThreshold",
"AllowableDeductions"
]
}
}
\end{lstlisting}
\end{singlespace}
This relationship is fed into the neo4j graph database and can also be viewed as a knowledge graph:
\begin{figure}[H]
\centering
\includegraphics[width=0.7\linewidth]{Tex/Figures/Ontology_Initial.png}
\caption{Initial Ontology Structure}
\end{figure}
\subsubsection{Vocabulary Extraction from Statutory Law}
Each statutory subsection in MPP Division 63 is processed sequentially to derive the ontology vocabulary used in the TBox. The goal is to identify the core legal concepts that will later be referenced by ABox assertions and solver rules.
This can be done in a two step process:
\begin{enumerate}\setlength\itemsep{1pt}
\item \textbf{Clause division:} Statutory text is segmented into minimal eligibility-relevant clauses.
\item \textbf{Concept extraction:} Each clause is processed using noun-phrase extraction to isolate legally operative terms. Entities, conditions, and eligibility predicates referenced in the statute. Extracted spans are normalized into ontology compatible labels through lemmatization, stopword filtering, and conversion to canonical predicate formats. Citation references to the originating statutory clause are preserved to ensure traceability during later verification.
\end{enumerate}
Example:
\vspace{4pt}
MPP §63-401.1:
\textit{“A household shall be considered a resident of a county when it is living there and applies for benefits in that county.”}
\vspace{6pt}
Segmented clauses and extracted concepts result in:
\begin{singlespace}
\begin{lstlisting}[language=json]
{
"MPP 63-401.1": [
"Residency_HouseholdLocation",
"Residency_ApplicationCounty",
"Residency_County"
]
}
\end{lstlisting}
\end{singlespace}
\subsubsection{Integrating Extracted Concepts into the Ontology}
Once candidate concepts are extracted, they are embedded using the \texttt{e5-large-v2} embedding model and compared against existing ontology terms using cosine similarity. A similarity threshold of $>$ 0.85 is applied to determine whether a newly extracted term represents the same underlying legal concept already captured in the ontology. This prevents the creation of duplicate or semantically redundant nodes (e.g., “household residency” vs. “resident in the county”), ensuring that each eligibility factor appears only once and maintains a consistent representation across rules and cases. Concepts below the similarity threshold are added as distinct nodes, allowing the ontology to expand.
\vspace{15em}
\begin{figure}[H]
\centering
\includegraphics[width=0.7\linewidth]{Tex/Figures/Ontology_Grown.png}
\caption{Ontology Expansion After Concept Integration}
\end{figure}
\subsubsection{Rule Formalization (Creating the Grammar)}
After the ontology vocabulary is established, statutory clauses are converted into formal rules
that express legally operative logic in a machine-interpretable form. This process defines the
``grammar'' of eligibility verification. Rule creation consists of two sequential steps:
\begin{enumerate}\setlength\itemsep{4pt}
\item \textbf{Ontology Retrieval:}
For each statutory clause, the system retrieves relevant ontology concepts
from the graph representation:
\begin{singlespace}
\begin{lstlisting}[language=json]
{
"MPP 63-401.1": [
"Residency_HouseholdLocation",
"Residency_ApplicationCounty"
]
}
\end{lstlisting}
\end{singlespace}
\item \textbf{Logical Translation:}
Retrieved ontology terms form the vocabulary for a first-order logic rule.
A large language model (GPT-o1) encodes the statutory semantics into a
Z3-compatible state.
\end{enumerate}
% Example clause and code block appear outside the list — correct.
Example statutory clause:
\textit{``A household shall be considered a resident of a county when it is living there and applies
for benefits in that county.''} (MPP §63-401.1)
\noindent
The resulting solver rule reflects residency as a conjunctive requirement:
\begin{singlespace}
\begin{lstlisting}[language=json]
{
"hasLogic": "Implies(And(Residency_HouseholdLocation,
Residency_ApplicationCounty),
Applicant_Eligible)"
}
\end{lstlisting}
\end{singlespace}
This representation preserves statutory intent while making residency determinations formally
verifiable. Each rule maintains citation metadata linking the constraint to its authoritative legal
source, enabling traceability during explanation evaluation.
\vspace{24em}
The following Python prompt template constrains the model output:
\begin{singlespace}
\begin{lstlisting}[language=python]
prompt_template = """
You are a legal reasoning assistant that converts explanatory
clauses into formal logic rules compatible with the Z3 SMT solver.
Use only the ontology variables provided below.
Represent the eligibility conclusion as Applicant_Eligible.
Syntax Requirements:
- Express each rule as a single logical implication
- Use first-order logic operators: Implies, And, Or, Not, Equals
- Use only ontology variable names exactly as listed
- Output only JSON with the field: "hasLogic"
- Do not include natural language explanations
Ontology Concepts:
{ontology_concepts}
Clause:
"{explanation_clause}"
Output format:
{
"hasLogic": "<first-order logical implication>"
}
"""
\end{lstlisting}
\end{singlespace}
Model-generated rule:
\begin{singlespace}
\begin{lstlisting}[language=json]
{
"hasLogic":
"Implies(
And(
Residency_HouseholdLocation,
Residency_ApplicationCounty
),
Applicant_Eligible
)"
}
\end{lstlisting}
\end{singlespace}
The resulting rules are stored as a collection of JSONs.
\vspace{5em}
\subsection{Final TBox Knowledge Representation}
The resulting ontology and rule set constitute the TBox. Examples shown below:
\begin{table}[H]
\centering
\small
\begin{tabular}{p{2.2cm} >{\raggedright\arraybackslash}p{6cm} >{\raggedright\arraybackslash}p{7cm}}
\toprule
\textbf{MPP Clause} & \textbf{Ontology Concepts} & \textbf{Formal Logical Rule} \\
\midrule
§63-401.1 & Residency\_HouseholdLocation, Residency\_ApplicationCounty &
Implies(And(Residency\_HouseholdLocation, Residency\_ApplicationCounty), Applicant\_Eligible) \\[2pt]
§63-502.36 & GrossIncome, IncomeThreshold &
Implies(GrossIncome > IncomeThreshold, Not(Applicant\_Eligible)) \\[2pt]
§63-405.1 & CitizenStatus, VerificationProvided &
Implies(And(Not(CitizenStatus), Not(VerificationProvided)), Not(Applicant\_Eligible)) \\[2pt]
§63-406 & StudentFlag, MeetsStudentExemption &
Implies(And(StudentFlag, Not(MeetsStudentExemption)), Not(Applicant\_Eligible)) \\[2pt]
§63-501.3 & HouseholdResources, ResourceThreshold &
Implies(HouseholdResources > ResourceThreshold, Not(Applicant\_Eligible)) \\
\bottomrule
\end{tabular}
\normalsize
\caption{TBox summary}
\end{table}
\vspace{5em}
\section{Building the Assertion (ABox)}
\label{sec:abox}
The ABox (assertion box) represents the factual layer of the framework, the level at which concrete case data and textual explanations are instantiated and tested against the legal norms encoded in the TBox. Whereas the TBox specifies the formal structure of law, the ABox captures particular states of the world: applicant information, decision rationales, and derived factual assertions. Together, these layers allow the system to evaluate whether a model-generated or human-authored explanation is logically consistent with the statutory conditions that govern benefit eligibility.
\begin{figure}[H]
\centering
\includegraphics[width=0.40\textwidth]{Tex/Figures/Abox_Architecture.drawio.png}
\caption{ABox creation pipeline.}
\label{fig:abox}
\end{figure}
\subsection{Assertion Vocabulary Extraction}
Assertion construction begins by grounding the free-text explanation in the same vocabulary
that underlies the TBox. In the same way that statutory clauses were decomposed and mapped
to ontology concepts, each explanation is first segmented into clauses and then aligned with
ontology predicates.
\begin{enumerate}\setlength\itemsep{6pt}
\item \textbf{Clause segmentation.}
The explanation is divided into minimal assertive units.
\textit{Example:} ``Your income was too high and you did not provide proof of residency.''
\textbf{Distinct Clauses:}
\begin{itemize}\setlength{\itemsep}{1pt}
\item ``Your income was too high.''
\item ``You did not provide proof of residency.''
\end{itemize}
\item \textbf{Concept matching.}
Each clause is mapped to ontology predicates using embedding-based similarity.
\textit{Mappings:}
\begin{itemize}\setlength{\itemsep}{1pt}
\item Clause 1 → GrossIncome, IncomeThreshold
\item Clause 2 → Residency\_HouseholdLocation, VerificationProvided
\end{itemize}
\end{enumerate}
These normalized assertions become explanation-linked ABox predicates, enabling the solver
to test whether the stated rationale is legally sufficient for the outcome reached.
\subsection{Assertion Rule Creation}
Once the assertion vocabulary has been identified, each clause of the explanation is translated into a case-specific logical statement. This step mirrors the statutory rule-formalization process described in the TBox section, but focuses only on the concepts actually referenced in the explanation.
\textbf{Prompt Abox Template:}
\begin{singlespace}
\begin{lstlisting}[language=json]
prompt_template = """
You are a legal reasoning assistant that converts explanatory
clauses into formal logic rules compatible with the Z3 SMT solver.
Use only the ontology variables provided below.
Represent the eligibility conclusion as Applicant_Eligible.
Syntax Requirements:
- Express each rule as a single logical implication
- Use first-order logic: Implies, And, Or, Not, Equals
- Output only JSON with "hasLogic"
- No natural language explanations
"""
\end{lstlisting}
\end{singlespace}
\textbf{Generated output example:}
\begin{singlespace}
\begin{lstlisting}[language=json]
{
"hasLogic": [
"Implies(GrossIncome > IncomeThreshold, Not(Applicant_Eligible))",
"Implies(Not(ResidencyVerificationProvided), Not(Applicant_Eligible))"
]
}
\end{lstlisting}
\end{singlespace}
These statements constitute the ABox assertion set for the case.
\subsection{Final ABox Knowledge Representation}
The conversion process normalizes linguistic variability into a canonical solver-compatible format, ensuring that equivalent explanations map to identical rules.
\begin{table}[htbp]
\centering
\caption{Normalization of explanation variants into canonical ABox assertions.}
\begin{tabular}{p{0.45\textwidth} p{0.45\textwidth}}
\toprule
\textbf{Explanation Variant} & \textbf{Canonical Logical Rule} \\
\midrule
``You applied in a different county than where you live.'' & ResidenceCounty(Applicant) = ApplicationCounty(Applicant) \\
``Eligibility denied — jurisdiction mismatch.'' & ResidenceCounty(Applicant) = ApplicationCounty(Applicant) \\
``You must live in the county you file in.'' & ResidenceCounty(Applicant) = ApplicationCounty(Applicant) \\
``Address on file belongs to another county.'' & ResidenceCounty(Applicant) = ApplicationCounty(Applicant) \\
``Applicant’s household is located outside this county.'' & ResidenceCounty(Applicant) = ApplicationCounty(Applicant) \\
\bottomrule
\end{tabular}
\label{tab:abox}
\end{table}
\vspace{20em}
\section{SMT Solver for Legal Consistency Checking}
\label{sec:smt}
\subsection{Formal Verification through SMT}
The final stage evaluates whether the explanation-derived assertions remain legally consistent when combined with case facts and statutory constraints. A Z3 SMT solver determines whether there exists a logically coherent assignment of values under which all statements can be true simultaneously.
When the solver returns \textbf{UNSAT}, it also provides a minimal
unsatisfiable core identifying the specific statutory constraints that the
assertions violate. These violated rules are surfaced directly to the user or reviewer, enabling precise legal contestation of the decision’s justification rather than a generic error signal. In this way, the solver
functions as a procedural accountability mechanism.
\begin{figure}[htbp]
\centering
\includegraphics[width=0.4\textwidth]{Tex/Figures/Architecture_SMT.drawio.png}
\caption{SMT reasoning architecture for legal verification.}
\label{fig:smt}
\end{figure}
The system retrieves only those statutory rules whose vocabulary overlaps with the
explanation-derived assertions, forming a targeted legal reasoning environment. Rather
than evaluating the full regulatory corpus, the solver focuses exclusively on the legal
provisions that the explanation claims are relevant to the decision. This ensures that the
verification step tests the legal sufficiency of the stated rationale, not its consistency
with unrelated eligibility criteria.
\noindent\textbf{Example:}
If an explanation cites excessive income and missing residency verification, the system
activates only the rules governing:
\begin{itemize}
\item Gross income thresholds (e.g., MPP §63–301.1)
\item County residency and verification requirements (e.g., MPP §63–401.1)
\end{itemize}
This selective retrieval prevents unnecessary constraint expansion and directs formal
verification to the precise statutory grounds invoked in the explanation.
\subsection{Solving the Legal Reasoning Environment}
To demonstrate the solver workflow, consider a case where the agency explanation states:
\begin{quote}
``Your income is too high and you did not provide proof of residency.''
\end{quote}
\noindent From this explanation, the system extracts:
\textbf{Ontology concepts:}
GrossIncome, IncomeThreshold, ResidencyVerificationProvided, Applicant\_Eligible
\textbf{Retrieved statutory constraints:}
\begin{itemize}
\item MPP §63–301.1 — Gross income must fall below the household-specific limit
\item MPP §63–401.1 — Residency must be verified in the administering county
\end{itemize}
\noindent These rules form the constrained legal environment for reasoning.
\medskip
\noindent \textbf{Scenario A: Facts support the explanation}
If case data confirm both excessive income and missing residency verification, the solver returns:
\begin{quote}
\textbf{SAT} — explanation is legally valid
\end{quote}
\noindent The reasoning trace identifies the specific satisfied rules, supporting due-process notice obligations.
\medskip
\noindent \textbf{Scenario B: Explanation contradicts the law}
If income is below the threshold but residency verification is missing, the solver returns:
\begin{quote}
\textbf{UNSAT} — violated constraint: MPP §63–301.1
\end{quote}
\noindent The solver surfaces the exact statutory rule that fails, enabling targeted correction or contestation of the decision rationale.
\section{Evaluation Design}
\label{sec:evaluation}
The performance of the proposed framework is evaluated along three dimensions that correspond directly to the major components of the verification pipeline. Each dimension isolates a distinct source of potential failure: semantic structure, rule formalization, and legal consistency checking. This design ensures that the evaluation assesses not only whether the system produces correct outcomes, but whether it does so for reasons that are legally grounded.
\subsection{Ontology Quality}
\label{subsec:ontology-quality}
The first evaluation examines whether the semantic structure of the ontology accurately reflects the legal organization of MPP Division 63. Concepts belonging to different eligibility domains should form meaningfully distinct groups, enabling accurate rule retrieval during explanation verification. This is assessed through embedding-based cluster separation, inter- and intra-cluster distance measures, and visual inspection of concept clusters.
\subsection{Rule Robustness}
\label{subsec:rule-robustness}
The second evaluation tests whether explanation-derived rules can be consistently translated into canonical solver-compatible logic, even when explanation texts vary. Multiple prompting configurations and language models are used to assess whether logical statements converge to legally equivalent forms across cases and decision conditions. Failures in convergence indicate ambiguity or brittleness in the translation process.
\subsection{Legal Consistency Evaluation}
\label{subsec:legal-consistency}
The final evaluation assesses whether the solver correctly determines whether an explanation is legally coherent with governing statutory constraints. The solver's SAT/UNSAT outcomes and violated-rule identifications are compared against ground-truth expectations for each case to determine correctness across eligibility categories.
The results of these evaluations are presented in Chapter~\ref{chap:results}, organized according to the same three dimensions.
\chapter{Results}
\label{chap:results}
\section{Overview}
This chapter presents the empirical findings from evaluating the proposed framework. Because the internal mechanics of CalFresh eligibility determination are not publicly observable, we can equate the current black box administrative state to a hypothetical black box AI system. In the current process, if a claimant is denied benefits, the agency will send out a Notice of Action (NOA) explaining the agency's decision and the statutory authority under which it has taken that action. We evaluate only the legal validity of the explanations provided in the Notice of Action (NOA).
Results are organized around three components of the system’s verification pipeline:
\begin{itemize}
\item \textbf{Ontology quality}: whether the semantic organization of encoded legal rules reflects statutory structure and supports relevant rule retrieval.
\item \textbf{Rule robustness}: whether explanation-derived rules can be consistently expressed in formal, verifiable logic.
\item \textbf{Legal consistency evaluation}: whether the SMT solver correctly detects alignment or conflict between the decision asserted in a case and the governing statutory constraints.
\end{itemize}
These results collectively assess the system’s ability to identify legally inconsistent explanations, surface violated rules, and support procedural accountability.
\section{Ontology Validation}
\begin{figure}[H]
\centering
\includegraphics[width=0.8\linewidth]{Tex/Figures/Umap.png}
\caption{Ontology concept clusters by eligibility domain}
\end{figure}
A key design requirement of the ontology is that legally distinct eligibility concepts remain divergent. CalFresh law contains separate criteria for income, residency, resources, citizenship, and student status. These categories should not overlap semantically: if the representation space blends residency concepts into income concepts, the system could retrieve the wrong statutory rules during explanation verification.
Concepts were embedded and projected into a two-dimensional UMAP semantic space. Concepts were colored by legal domain assignment, and convex hulls were drawn around each group for boundary clarity.
The resulting projection shows distinct and visually separable clusters. Distance analysis further supports this observation:
\begin{itemize}
\item Average intra-cluster cosine distance: \textbf{0.146}
\item Average inter-cluster cosine distance: \textbf{0.183}
\end{itemize}
These results demonstrate that the ontology fulfills its intended role as a legally coherent and divergent knowledge organization layer.
A slight overlap is visible between Income and Resource eligibility concepts, expected due to shared financial criteria.
While these clusters demonstrate that the ontology captures meaningful distinctions in legal
concepts, coverage remains partial and additional categories (e.g., student exemptions,
residency nuances) would further improve representational completeness.
\section{Rule Robustness}
\label{sec:rule-robustness}
The second evaluation dimension tests whether derived rules can be consistently translated into
formal logic that is both syntactically valid and semantically aligned with statutory intent. Large
Language Models (LLMs) were prompted to rewrite selected MPP provisions into Z3-compatible
logical rules.
Three prompting strategies were evaluated:
\begin{itemize}
\item \textbf{Vanilla prompting}: Minimal instruction; narrative translations likely
\item \textbf{Undirected rule prompting}: General guidance on rule structure without explicit syntax.
\item \textbf{Directed symbolic prompting}: Explicit structure enforced via a prompting template
\end{itemize}
\subsection{Ground-Truth Rule Construction}
Representative examples of statutory clauses and their corresponding executable logic are shown in
Table~\ref{tab:ground-truth-rules}.
\begin{table}[H]
\centering
\caption{Ground-truth statutory eligibility rules and SMT-executable logic.}
\label{tab:ground-truth-rules}
\begin{tabular}{>{\raggedright\arraybackslash}p{4.3cm} p{6cm} p{6cm}}
\toprule
\textbf{Case (MPP Citation)} & \textbf{Statutory Text} & \textbf{Executable Logical Rule} \\
\midrule
Gross Income Limit (§63-503.321) &
Household gross income must be at or below the Federal Poverty Level. &
\texttt{Implies(GrossIncome <= FPL(HouseholdSize), Applicant\_Eligible)} \\
\midrule
County Residency (§63-300) &
Applicants must reside in the county where they apply for CalFresh benefits. &
\texttt{Implies(Not(Resident), Not(Applicant\_Eligible))} \\
\midrule
Elderly or Disabled Eligibility (§63-402) &
Households with a member aged 60+ or with a disability receive categorical eligibility. &
\texttt{Implies(Or(Age >= 60, HasDisabilityStatus), Applicant\_Eligible)} \\
\bottomrule
\end{tabular}
\end{table}
\subsection{Prompting Strategy Performance}
LLMs were evaluated across 30 rule extraction attempts per model. A rule was considered successful
if it parsed cleanly in Z3 and preserved the intended statutory semantics.
\begin{table}[H]
\centering
\caption{Rule extraction success rates by model, prompting strategy, and statutory test case. Each cell reports successful formalizations out of 30 attempts; the final column shows the average success rate across the three cases.}
\label{tab:prompt-success-rates}
\begin{tabular}{l l c c c c}
\toprule
\textbf{Model} & \textbf{Prompt Type} & \textbf{Income} & \textbf{Residency} & \textbf{Elderly/Disabled} & \textbf{Avg.\%} \\
\midrule
Claude 3.5 Sonnet & Vanilla & 0/30 & 1/30 & 2/30 & 3\% \\
& Undirected & 5/30 & 7/30 & 9/30 & 23\% \\
& Directed & 22/30 & 25/30 & 26/30 & 80\% \\
\midrule
GPT-4o & Vanilla & 1/30 & 2/30 & 3/30 & 7\% \\
& Undirected & 7/30 & 9/30 & 10/30 & 27\% \\
& Directed & 24/30 & 27/30 & 28/30 & 87\% \\
\midrule
GPT-o1 & Vanilla & 1/30 & 3/30 & 3/30 & 7\% \\
& Undirected & 8/30 & 10/30 & 11/30 & 30\% \\
& Directed & 27/30 & 29/30 & 29/30 & 93\% \\
\midrule
DeepSeek-R1 & Vanilla & 0/30 & 1/30 & 0/30 & 0\% \\
& Undirected & 4/30 & 6/30 & 7/30 & 20\% \\
& Directed & 21/30 & 23/30 & 24/30 & 73\% \\
\bottomrule
\end{tabular}
\end{table}
\begin{figure}[H]
\centering
\includegraphics[width=0.85\linewidth]{Tex/Figures/BarChart.pdf}
\caption{Performance comparison across prompting strategies.}
\label{fig:prompt-performance}
\end{figure}
Across all models tested, \textbf{directed symbolic prompting} produced the highest rates of solver-compatible
formalizations. These results demonstrate that reliable legal rule extraction requires instruction on
logical form, not merely relevant content.
\section{Testing Dataset Creation}
The NOA serves as the official justification provided to the applicant and represents the only observable interface to the decision logic regardless of what automated systems, heuristics, or human discretion generated the determination.
The evaluation dataset consists of administrative hearing decisions from the State of California involving CalFresh (SNAP) eligibility disputes.\cite{cdss_acms_registry} These cases are publicly available appeal records in which applicants challenge county benefit actions such as terminations, denials, or reductions. Each record includes both a factual description of the household circumstances and the NOA text embedded within the decision narrative. Examples of the raw case files can be found in the Appendix.
From each decision, two layers of data were extracted for testing:
\begin{enumerate}
\item Structured eligibility attributes, including household size, income, residency, citizenship, student status, and other relevant factors.
\item The NOA explanation text, which expresses the county’s rationale for the action taken.
\end{enumerate}
Because appeal decisions include a final ruling by a judge, they provide an authoritative ground truth for statutory compliance. If an applicant prevails, it indicates that the original agency reasoning contradicted governing law; conversely, upheld decisions provide evidence of statutory consistency. This makes the dataset appropriate for testing whether the system correctly detects legally inconsistent explanations.
A total of 43 cases were selected to ensure representative coverage across key eligibility rule
categories encoded in the ontology. The dataset includes a balanced distribution of upheld and
overturned determinations spanning the five major eligibility dimensions evaluated in this chapter.
\begin{table}[H]
\centering
\caption{Distribution of evaluation cases by eligibility category and legal outcome}
\label{tab:case-outcome-distribution}
\begin{tabular}{l c c c}
\toprule
\textbf{Eligibility Category} & \textbf{Accepted Cases} & \textbf{Rejected Cases} & \textbf{Total} \\
\midrule
Income & 4 & 3 & 7 \\
Residency & 5 & 4 & 9 \\
Citizenship & 5 & 4 & 9 \\
Resources & 5 & 3 & 8 \\
Student Status & 5 & 5 & 10 \\
\midrule
\textbf{Total} & \textbf{24} & \textbf{19} & \textbf{43} \\
\bottomrule
\end{tabular}
\end{table}
\section{Legal Consistency Verification}
\label{sec:legal-consistency}
We evaluate the system’s legality verification performance along two dimensions:
\begin{itemize}
\item \textbf{Violated Rule Detection} — whether the system correctly identifies the statutory
basis for ineligibility in denied cases (Violation F1)
\item \textbf{Final Legality Judgment} — whether the SMT solver reaches the same legality
determination as the administrative law judge (SMT Accuracy)
\end{itemize}
Violation detection performance is evaluated using the F1 score\cite{Rainio2024EvalMetrics}:
\[
F1 = \frac{2 \times (\text{Precision} \times \text{Recall})}{\text{Precision} + \text{Recall}}
\]
SMT accuracy measures solver agreement with judicial rulings.
\begin{table}[H]
\centering
\caption{Explanation verification performance across eligibility categories.}
\label{tab:violation-smt}
\begin{tabular}{l c c c c}
\toprule
\textbf{Category} & \textbf{Status} & \textbf{Cases} &
\textbf{Violation F1} & \textbf{SMT Accuracy} \\
\midrule
Student Status & SAT & 5 & --- & 90\% \\
Student Status & UNSAT & 5 & 0.64 & 90\% \\
Income & SAT & 4 & --- & 100\% \\
Income & UNSAT & 3 & 0.51 & 100\% \\
Residency & SAT & 5 & --- & 100\% \\
Residency & UNSAT & 4 & 0.79 & 100\% \\
Citizenship & SAT & 5 & --- & 100\% \\
Citizenship & UNSAT & 4 & 0.83 & 100\% \\
Resources & SAT & 5 & --- & 100\% \\
Resources & UNSAT & 3 & 0.72 & 100\% \\
\midrule
\textbf{Total} & --- & \textbf{43} & --- & \textbf{97.7\%} \\
\bottomrule
\end{tabular}
\end{table}
The solver matched judicial legality determinations in 42 of 43 cases (97.7\%). Errors occurred only
when the explanation text omitted legally relevant rule conditions, demonstrating that legal failures
stem from explanation content rather than symbolic reasoning. Violation F1 scores vary across categories because the retrieved violated statute is sometimes
semantically correct but does not match the specific citation referenced in the case record. In these
instances, the system correctly identifies the type of eligibility failure (e.g., income limit exceeded) but
retrieves a closely related clause from the same statutory domain rather than the exact subsection
cited by the county. This reflects ambiguity or incompleteness in the explanation text rather than a
misinterpretation of legal structure. Crucially, the solver still reaches the correct legality judgment in
all but one case, indicating that explanation fidelity and not the underlying statutory reasoning is the primary source of residual error. This might be solved by including case law into the system.
\section{Statutory Violation Trace Visualization}
\begin{figure}[H]
\centering
\includegraphics[width=0.85\linewidth]{Tex/Figures/affected_laws.png}
\caption{Solver trace visualization with red nodes identified as violated statutes}
\end{figure}
When an explanation contradicts eligibility criteria, the solver returns \texttt{UNSAT} and highlights
the precise clause responsible for the failure. This enables caseworkers and applicants to understand
not only that a decision is legally incorrect, but also why it is incorrect and which statutory
requirement must be addressed. By grounding errors in explicit legal references, this functionality
supports meaningful contestation within a due process framework.
\section{Individual Case Walkthrough}
\begin{figure}[H]
\centering
\includegraphics[width=0.85\linewidth]{Tex/Figures/CaseStudy_Thesis.drawio.pdf}
\caption{Example case walkthrough visualization}
\end{figure}
Example case:
\begin{itemize}
\item GrossIncome = 2015.13 (above threshold)
\item NOA claim: “Income exceeds limit”
\end{itemize}
Solver result:
\[
\text{UNSAT} \Rightarrow \text{Explanation legally insufficient}
\]
The solver identifies precisely which statutory rule is violated (MPP §63-502.32).
\section{Conclusion}
Across multiple evaluation layers, the proposed framework demonstrates that legal consistency in
automated eligibility decision systems is both measurable and enforceable. The ontology preserves
the statutory structure of CalFresh law, directed rule prompting yields reliable symbolic
representations of eligibility criteria, and the SMT solver replicates judicial legality determinations
with near-perfect accuracy. When errors occur, they stem from incomplete explanatory content rather
than failures of logical reasoning.
These results confirm that legally grounded explanation verification is computationally feasible and
can serve as a safeguard against unlawful automation. By identifying the precise statutory basis of
incorrect determinations, the approach strengthens contestability and supports due process for
applicants subject to automated public-benefit decisions.
\chapter{Discussion}
\label{chap:discussion}
\section{Operationalizing HCXAI in the Public Sphere}
Human-Centered Explainable AI (HCXAI) seeks to position the human perspective at the core of AI system behavior. However, in legally regulated decision environments, centering the human requires more than intuitive or visually appealing explanations. Without a legally grounded interpretive structure, explanations risk becoming unanchored narratives that provide little procedural value. In public-benefit contexts, applicants must not only understand what an automated system decided but also the legal basis upon which that decision rests. All further HCXAI goals\cite{liao2021human} i.e actionability, contestability, and protection against harm depend on this connective tissue of legal traceability.
This framework contributes toward operationalizing HCXAI in the legal space by establishing a symbolic rule boundary that constrains otherwise free-flowing model explanations. As shown in Figure~\ref{fig:eligibility-map}, the system visualizes satisfied and violated eligibility rules, creating an intelligible map from applicant facts to statutory consequences. This design transforms explanations into tools of empowerment: individuals can identify precisely which condition drove an ineligibility finding and challenge automated errors by referencing authoritative legal sources. In this way, the system does not merely explain decisions, it supports the right to understand and contest them.
% Example figure environment – rename fig file as needed
\begin{figure}[ht]
\centering
\includegraphics[width=0.85\textwidth]{Tex/Figures/Discussion.drawio.png}
\caption{Visualization of satisfied and violated explanations in a sample eligibility case.}
\label{fig:eligibility-map}
\end{figure}
\section{Fairness Beyond Legal Compliance}
Legal compliance is the foundational layer of fairness in public-benefit decision systems. If an explanation cannot be traced to the statutes that authorize eligibility decisions, individuals cannot understand the basis of exclusion or challenge mistakes that harm them. Once this base layer is secured through legally grounded explainability, additional fairness objectives become possible. Group fairness \cite{pessach2020algorithmic} ,evaluating whether outcomes disproportionately affect specific demographic or socioeconomic groups—cannot be credibly assessed without first ensuring that decisions are consistent with law. Likewise, distributive justice concerns \cite{wang2022brief}, such as whether eligibility rules systematically burden those already facing structural disadvantage, can only be surfaced when the legal reasoning behind decisions is explicit and verifiable. In this layered view of fairness, statutory traceability enables fairness analysis rather than limiting it, creating the conditions in which higher-order equity goals can be pursued responsibly.
Beyond formal rule compliance, several complementary fairness notions are central in the broader AI ethics and governance literature. Individual fairness \cite{mehrabi2021survey} examines whether similar applicants receive similar outcomes ; two families with comparable income and household composition should not be treated differently due to arbitrary workflow variation or model drift. Procedural fairness\cite{ferrara2023fairness} considers whether the eligibility process respects dignity and provides a meaningful opportunity to demonstrate eligibility—something that hinges on transparent explanations and accessible standards of proof. Finally, substantive fairness\cite{tang2022fairness}, grounded in principles of equity and social justice, asks whether policies themselves promote or undermine well-being, especially for groups historically marginalized by administrative systems.
Legally grounded explainability does not resolve these fairness problems on its own, but it enables them to become visible and actionable. Without traceable explanations, disparities and arbitrary decisions remain concealed and unchallengeable. By surfacing exactly which rules drive different outcomes, the system creates analytic clarity: if inequity emerges, stakeholders can determine whether it stems from data, implementation, or the statute itself. In this layered framing, legal accountability is not in tension with fairness but rather it is the entry point to fairness. Only once the base layer of legal traceability is secured can higher-order fairness goals be meaningfully assessed and pursued.
\section{Policy and Administrative Implications}
Public agencies face increasing pressure to ensure transparency, due process, and accountability in automated decision-making while balancing constraints such as proprietary technologies, operational risk, and limited technical capacity. Traditional approaches that attempt to “open the black box” often prove insufficient: vendors may decline to disclose internal model architectures, and even when available, model-level explanations rarely translate into legally meaningful justifications.\cite{doshi2017towards, veale2018fairness}
A more durable governance strategy is emerging across public-sector and enterprise environments: shifting from model-centric transparency to explanation-centric accountability. Under this approach, the central question is not how the model internally arrives at a decision, but whether the explanation it produces is legally defensible, normatively appropriate, and traceable to statutory requirements.\cite{wachter_right_2017} In domains such as CalFresh, the law, not the model’s internal reasoning defines the criteria that must be satisfied when determining eligibility.
The framework developed in this thesis operationalizes this shift by requiring that every explanatory statement map directly to specific provisions of the governing statute. This transforms automated decision-making into a process that is inherently auditable and grounded in legal authority. By anchoring explanations to a structured statutory ontology and evaluating them through formal reasoning, the framework ensures that automated decisions remain aligned with the same standards that apply to human administrators.
This design aligns well with emerging governance architectures that structure oversight around three complementary layers \cite{EisenbergGamboaSherman2025UnifiedControlFramework}:
Risk Identification and Traceability.
Modern AI governance relies on structured risk taxonomies that capture technical, operational, legal, and societal risks \cite{NIST_AI_RMF_2023} \cite{Slattery2024}. The framework contributes to this layer by generating rule-referenced decision logs that make misinterpretations and procedural drift directly observable \cite{SelbstEtAl2019}. This allows agencies to identify inconsistent applications of eligibility rules across counties or demographic groups and trace such issues back to specific statutory provisions.
Policy Requirements and Legal Obligations.
Regulations and standards often specify high-level obligations: transparency, documentation, fairness safeguards, user rights, and auditability, without indicating how agencies should meet them \cite{GoodmanFlaxman2017}. The framework provides concrete compliance artifacts that operationalize these obligations, including structured explanations, case-level decision logs, and traceable statutory mappings suitable for review by auditors, legal teams, and administrative law judges. These artifacts support both internal governance processes and external regulatory oversight\cite{WachterMittelstadtFloridi2017}.
Controls and Oversight Mechanisms.
AI governance increasingly depends on implementable controls: repeatable processes that satisfy multiple risks and regulatory requirements \cite{Raji2020} \cite{Mitchell2019}. The framework functions as a domain-specific control mechanism by enforcing statutory consistency, generating persistent audit trails, and providing legally structured rationales for each determination. These features ensure that automated systems reinforce rather than weaken existing administrative safeguards.
Together, these layers support a governance posture in which agencies can maintain transparency and due process even when using complex or vendor-supplied AI systems. By separating the model’s predictive function from the justificatory function required by law, the framework enables modernization of service delivery without sacrificing accountability.
\chapter{Conclusion}
\label{chap:conclusion}
\section{Summary of Findings}
This thesis developed and evaluated a neuro-symbolic framework for legally grounded explainability in public-benefit decision systems. In contrast to traditional explainability approaches that focus primarily on interpretability or model transparency, this work placed statutory authority at the center of how explanations are produced, evaluated, and communicated. By encoding eligibility criteria from the California MPP into a machine-interpretable ontology and translating applicant facts into structured rule assertions, the system establishes a direct, verifiable connection between decision outcomes and the laws that govern them.
The framework ensures that explanations presented to applicants align with the statutory basis that authorizes decisions, supporting their rights to understand and contest adverse outcomes. Through evaluation on real-world case patterns including approvals, denials, and ambiguous scenarios, the system demonstrated high accuracy in identifying satisfied and violated rules while producing an embedded audit trail suitable for oversight.
More broadly, this work illustrates that grounding explainability in statutory logic is a prerequisite for responsible deployment of AI in administrative decision-making. Legal traceability reinforces transparency and due process, enabling higher-order fairness goals to be meaningfully assessed. By integrating symbolic reasoning with data-driven retrieval, the system offers a practical path for federal, state, and local agencies to adopt accountable automation without requiring access to proprietary model internals. As digitization in social protection programs accelerates, the contributions of this thesis provide a scalable foundation for AI tools that strengthen, rather than weaken, democratic governance and public trust.
\section{Synthesis Across Research Questions}
This thesis examined whether automated eligibility explanations can be made accountable to the statutory rules that authorize benefit decisions. The research questions framed this inquiry and are addressed below.
RQ1 — Representation. The first research question asked how statutory eligibility requirements could be structured into a computable form that preserves legal semantics. This thesis demonstrated that a legal ontology (TBox) derived from MPP Division 63 can faithfully encode eligibility concepts, thresholds, and interdependencies. This representation maintains hierarchical constraints and provides the shared legal vocabulary required for both human oversight and automated reasoning.
RQ2 — Alignment. The second research question investigated how explanation content could be translated into that same legal structure. Through a semantic alignment pipeline, free-text justification statements were normalized into ABox assertions expressed using the ontology’s predicates. Evaluation showed that neural extraction methods can reliably map explanation language to the legally operative concepts it intends to reference, enabling claims to be tested directly against statutory authority.
RQ3 — Verification. The final research question examined how to determine whether those explanation-derived assertions are legally compliant. By integrating solver-based reasoning, the system was able to identify when explanations satisfy or violate statutory constraints and to trace precisely which rules are implicated in each violation. This transforms explanations into verifiable procedural artifacts that support due-process review.
Across all three questions, the results establish that legally grounded explainability is technically feasible. Representing law in computable form, aligning explanations to that structure, and verifying legal consistency can operate together as an accountability mechanism, ensuring automated eligibility reasoning remains answerable to the rule of law.
\section{Limitations}
\subsection{Drift between output and system explanation}
A key limitation of the current approach is its reliance on the assumption that an automated system’s explanation faithfully reflects the internal path by which the decision was made. In many deployed environments, explanation modules are implemented as post-hoc rationalizers, producing plausible narratives rather than exposing true model reasoning. In such cases, it is possible for a decision to be driven by features or correlations that the explanation does not disclose. If the justification offered is nonetheless framed in legally acceptable terms, the system as evaluated here would treat the output as compliant.
\subsection{Reliance on statutory text without interpretive context}
The system treats the California MPP as the definitive source of legal authority when translating requirements into formal rules. However, statutory language is often clarified and reshaped through administrative interpretation, appeal decisions, and judicial precedent. Without systematically incorporating case-based interpretation, the framework risks encoding rules that reflect the letter but not the evolving meaning of the law.
\subsection{LLM sensitivity to legal complexity}
The rule translation process relies on large-language-model prompting to express statutory clauses as formal constraints. Longer or exception-laden provisions increase the likelihood of semantic drift or misalignment. Although safeguards such as clause segmentation reduce this risk, LLM brittleness remains a potential source of legal error.
\subsection{Incomplete ontology coverage}
The ontology currently captures only the legally operative elements explicitly surfaced during system development. Less common eligibility pathways, exceptions, and administrative procedures are not yet modeled. Consequently, legally relevant distinctions may be flattened or omitted, especially in edge-case scenarios.
\subsection{Limited evaluation dataset}
The evaluation used a subset of the available case corpus that, while representative of core eligibility categories, does not fully span the diversity of real-world program administration. Broader testing—including cross-county variation, procedural disputes, and mixed-eligibility cases—would strengthen claims of generalizability.
\subsection{Fairness dimensions beyond legality}
The system focuses on procedural fairness through statutory traceability. Other fairness concerns such as disparate impact or structural inequity remain outside the current scope. Ensuring that outcomes are both legally compliant and socially equitable is an important direction for expansion.
\subsection{System interpretation rigidity}
Some agency explanations may be legally sufficient but the system flags the reasoning as deficient due to mismatches between natural-language expressions and formal ontology concepts. This highlights the gap between human interpretive flexibility and symbolic system rigidity.
\section{Future Work}
While the framework introduced in this thesis demonstrates the feasibility of legally grounded
explainability in automated eligibility systems, several promising directions remain for further
development.
\subsection{Expanding normative coverage.}
The current ontology represents a subset of CalFresh eligibility rules. Continued development should
extend coverage to additional program components (e.g., student exemptions, reporting obligations)
and integrate procedures for automatically tracking statutory changes over time.
\subsection{Broader administrative domains.}
The architecture is applicable to any legally constrained decision process in which eligibility criteria
are codified in public law. Future deployments may include Medicaid, unemployment insurance, or
housing assistance, each of which introduces new legal constructs and verification challenges.
\subsection{Integrating fairness and equity analysis.}
Compliance with statutory requirements does not guarantee equitable access to benefits. A natural
extension involves coupling normative verification with fairness auditing, enabling simultaneous
detection of legal and disparate-impact violations.
\subsection{User-centered contestation.}
Since the system identifies which specific rules are satisfied or violated, it could support interactive
appeals processes in which applicants correct misclassified facts or provide new evidence before final
determinations—strengthening due-process protections.
Together, these directions point toward a broader vision of accountability in automated governance,
in which legal compliance, procedural fairness, and user participation are jointly supported by
computational infrastructure.
%Appendix -- January 2015
\appendix
\renewcommand{\thechapter}{A}
\vspace*{-.85in}
\renewcommand{\chaptername}{Appendix}
\chapter{}
\label{chap:Appendix}
This appendix includes illustrative excerpts of the ontology, rules, and case files used for evaluation. Full artifacts are provided in the project repository.
\section{Ontology Example}
This appendix presents a brief excerpt of the legal ontology used in the system. The ontology encodes CalFresh eligibility requirements from MPP Division~63 into a structured representation of key concepts, such as income limits and household characteristics, along with their legal relationships. The example below illustrates how income-related eligibility rules are formalized for automated reasoning.
\begin{singlespace}
\begin{lstlisting}[language=json]
{
"Applicant": {
"definition": "Represents an individual or household applying for SNAP benefits.",
"conceptType": "Entity",
"citation": "MPP 63-401",
"subtypes": {
"Applicant_Eligible": {
"definition": "Indicates whether the applicant is eligible for participation.",
"citation": "MPP 63-401.1",
"conceptType": "Boolean"
},
"Applicant_ResidenceCounty": {
"definition": "The county in which the applicant resides.",
"citation": "MPP 63-401.1",
"conceptType": "String"
},
"Applicant_ApplicationCounty": {
"definition": "The county in which the applicant files an application.",
"citation": "MPP 63-401.1",
"conceptType": "String"
}
}
}
\end{lstlisting}
\end{singlespace}
\section{Rules Example}
This section provides a representative example of the statutory rules encoded for solver-based verification. Each rule is translated from MPP Division~63 into logical constraints that define when an eligibility condition is satisfied or violated. These formalizations allow the system to test whether an explanation’s claims are legally consistent and to identify the specific rules implicated when inconsistencies occur. The snippet below illustrates the structure of threshold- and dependency-based constraints used in the verification layer.
\begin{singlespace}
\begin{lstlisting}[language=json]
{
{
"id": "Rule_ResidencyRequirement",
"citation": "MPP 63-401.1",
"hasText": "A household must reside in the county in which it files an application for participation.",
"class": "Residency",
"subclass": "CountyResidency",
"appliesTo": ["Applicant_ResidenceCounty", "Applicant_ApplicationCounty"],
"determines": ["Applicant_Eligible"],
"hasLogic": "Implies(Applicant_ResidenceCounty != Applicant_ApplicationCounty, Not(Applicant_Eligible))",
"hasModality": "Obligation",
"conceptType": "Boolean"
},
{
"id": "Rule_StateResidencyRequirement",
"citation": "MPP 63-401.1",
"hasText": "A household must reside within the administering state to qualify for participation.",
"class": "Residency",
"subclass": "StateResidency",
"appliesTo": ["Applicant_ResidenceState", "AdministeringState"],
"determines": ["Applicant_Eligible"],
"hasLogic": "Implies(Applicant_ResidenceState != AdministeringState, Not(Applicant_Eligible))",
"hasModality": "Obligation",
"conceptType": "Boolean"
}
}
\end{lstlisting}
\end{singlespace}
\section{Case Files}
\begin{figure}[H]
\centering
\includegraphics[width=0.7\linewidth]{Tex/Figures/Decision_104626551_06012020163406627_Public.pdf}
\caption{First page of example decision. Full document provided in project repository.}\end{figure}