Precise logical formalization of legal text helps automated compliance analysis and machine-readable legal reasoning, which help streamline and prove complex queries in industries like law and insurance. Achieving this is challenging, as legal text includes ambiguity, exceptions, and layered nuances that make it difficult to consistently translate into logical rules. Existing large language model-based methods often generate inconsistent predicates, drift in meaning, and fail to capture complex legal structures. This thesis introduces a structured pipeline for converting legal text into Defeasible Deontic Logic and First-Order logic with a focus on keeping key terms consistent and grounding predicates in a stable manner. The approach introduces consistency through a symbol-table framework that constrains LLM outputs to a vocabulary of legal actors and actions. Combined with clause segmentation, multi-stage LLM rewriting, and automated Z3 consistency verification, the system produces logical rules that better maintain the intended argument structure of legal statutes. Evaluating with multiple legal examples shows that this method reduces logical errors and produces formalizations suitable for reasoning tasks and analysis. The results demonstrate that integrating symbolic guidance with LLM-based processing provides a path toward generating trustworthy formal representations of legal text.

61 pages

Thesis Committee:
Umut Acar (Chair)
Sherry Tongshuang Wu

Jignesh Patel, Interim Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: School of Computer Science

This page maintained by reports@cs.cmu.edu