# Formalizacja prawa EN: **Computational law and formal legal models** · id `computationallaw` · aliases: computational law, formal models of law, legal knowledge representation, symbolic AI and law, legal expert systems, prawo obliczeniowe, formalizacja przepisów Path: [AI Atlas](https://aiatlasgraph.com/llms.txt) › [AI w prawie](https://aiatlasgraph.com/t/legalai.md) › Formalizacja prawa ## Description - PL: Symboliczny nurt AI i prawa: reprezentacja norm w logice i językach programowania oraz obliczeniowe modele rozumowania i argumentacji prawniczej. - EN: The symbolic strand of AI and law: representing norms in logic and programming languages, and computational models of legal reasoning and argument. ## In one sentence - PL: Zapisywanie przepisów i sposobów argumentowania w języku, który komputer potrafi ściśle wykonać i sprawdzić, zamiast tylko czytać tekst. - EN: Writing laws and ways of arguing in a language a computer can execute and check precisely, rather than merely read as text. ## Problem it solves - PL: Przepisy pisane prozą są niejednoznaczne i rozproszone, więc urzędy i firmy różnie je liczą, a błędy w systemach wychodzą dopiero po latach. - EN: Laws written in prose are ambiguous and scattered, so agencies and firms compute them differently, and errors in systems surface years later. ## What it does - PL: Jak przepisanie przepisu kulinarnego na dokładny algorytm z wagą w gramach: każdy krok i wyjątek musi być nazwany, więc luki od razu wychodzą na jaw. - EN: Like rewriting a recipe as an exact algorithm with gram weights: every step and exception must be named, so gaps show up straight away. ## Everyday example - PL: Kalkulator zasiłku na stronie urzędu liczy kwotę według tej samej, sprawdzonej wersji przepisów, której używa system wypłat. - EN: A benefits calculator on an agency website computes the amount from the same verified version of the rules that the payment system uses. ## This concerns you if you… - PL: projektujesz system liczący podatki, zasiłki lub opłaty - PL: interesuje cię, jak komputer może rozumować o prawie - EN: design a system that computes taxes, benefits or fees - EN: wonder how a computer can reason about law ## Keywords rules as code · Catala · defeasible logic · LegalRuleML · legal ontologies · computational models of argument · HYPO · CATO · ICAIL ## How it works - PL: Normy zapisuje się jako reguły z wyjątkami (logika domyślna i niemonotoniczna), w dedykowanych językach programowania albo jako ontologie pojęć prawnych. Modele argumentacji reprezentują sprawy przez czynniki sprzyjające stronom i formalizują ruchy w sporze. Dziś łączy się je z LLM, które tłumaczą tekst na reguły. - EN: Norms are encoded as rules with exceptions (default and non-monotonic logic), in dedicated programming languages or as ontologies of legal concepts. Argument models represent cases by factors favouring each side and formalise moves in a dispute. Today they are combined with LLMs that translate text into rules. ## Limits - PL: Ręczna formalizacja jest pracochłonna i wymaga prawnika oraz programisty naraz. Nie każdy przepis da się zapisać ściśle, bo prawo celowo zostawia pojęcia nieostre. Status prawny wersji kodowej i jej aktualizacje pozostają otwarte. - EN: Manual formalisation is laborious and needs a lawyer and a programmer together. Not every provision can be stated precisely, as law deliberately leaves concepts vague. The legal status of the coded version and its updates remain open questions. ## Key terms - PL: **logika niemonotoniczna**: Logika, w której nowy fakt może obalić wcześniejszy wniosek. - PL: **system ekspercki**: Program wnioskujący z ręcznie spisanych reguł dziedziny. - PL: **pojęcie nieostre**: Termin prawny celowo nieprecyzyjny, np. „należyta staranność”. - EN: **non-monotonic logic**: A logic in which a new fact can defeat an earlier conclusion. - EN: **expert system**: A program that reasons from hand-written domain rules. - EN: **open-textured concept**: A deliberately imprecise legal term, e.g. 'due care'. ## Know first - [Logika zdań i logika pierwszego rzędu (Propositional and first-order logic)](https://aiatlasgraph.com/t/fol.md) - [Ontologie i sieć semantyczna (RDF, OWL) (Ontologies and the Semantic Web (RDF, OWL))](https://aiatlasgraph.com/t/ontologies.md) ## Subtopics (4 direct, 4 in total) - [Automatyczne sprawdzanie zgodności z przepisami (Automated regulatory compliance checking)](https://aiatlasgraph.com/t/compliancechecking.md): Verifying business processes and documents against legal norms: classically with formal deontic rules, more recently also with LLMs and retrieval. - [Modele argumentacji prawniczej (Computational models of legal argument)](https://aiatlasgraph.com/t/legalargumentation.md): Formal and computational models for generating, evaluating and using legal arguments, especially precedent-based reasoning with factors and dimensions. - [Prawo jako kod (Rules as code)](https://aiatlasgraph.com/t/rulesascode.md): Creating a machine-executable version of legislation alongside the legal text, in dedicated languages or frameworks, ideally at the drafting stage. - [Ustrukturyzowane dokumenty prawne (Structured legal documents)](https://aiatlasgraph.com/t/machinereadablelaw.md): Standards for structured encoding and identification of legal documents in XML and RDF, enabling precise linking, versioning and consolidation. ## Related topics Untyped, symmetric "see also" links. - [Logika i reprezentacja wiedzy (Logic and knowledge representation)](https://aiatlasgraph.com/t/logic.md) ## Sources - [Catala: A Programming Language for the Law]() `merigoux-catala-2021` · by Denis Merigoux, Nicolas Chataing, Jonathan Protzenko - [HYPO's Legacy: Introduction to the Virtual Special Issue]() `benchcapon-hypo-legacy-2017` · by Trevor J. M. Bench-Capon - [Conditional definitions and exceptions — The Catala domain-specific programming language]() `catala-exceptions-docs` · by Catala contributors --- AI Atlas revision 122 (2026-10-30) · HTML: https://aiatlasgraph.com/t/computationallaw · index: https://aiatlasgraph.com/llms.txt · everything: https://aiatlasgraph.com/llms-full.txt · updated 2026-10-30