Navratil GerhardFormalization of Law
by Gerhard Navratil
The thesis discusses laws and algebras. These two topics seem to be quite different. Laws are text books that regulate the life of humans. Algebras are a mathematical method fort he description of properties. However, both describe systems and the methods used seem to be similar. The methods are in both cases classification, abstraction and axiomatic definition.
The thesis describes a method to translate laws into algebras. Starting point is a comparison of the modeling systems. The method requires three steps:
· Identification of the classes
· Definition of data types, operations, and axioms
· Testing with a simple model realisation
It is important to know the contribution of a single paragraph for the model. A paragraph can specify a data type, describe an operation, or define an axiom. The description of the operation consists of three parts. First the operation must be necessary. The operation then requires parameters and produces a result. Finally, the operation must be member of a class. Paragraphs fulfill all tasks. Rather frequently the combined content of several paragraphs solves one task.
The method developed was tested with an example. The example used here was the Austrian land registration law (allgemeines Grundbuchsgesetz). It was translated into an algebraic model without knowledge from the real system. All information was taken from the land registration law or other laws like the civil law code (allgemeines bürgerliches Gesetzbuch).
The algebraic modeling was done in Haskell, a functional programming language. The advantage of Haskell if compared to other programming languages is the mathematical purity. This would also be true for pure mathematics but Haskell is also executable which allows testing the code.
The thesis can be downloaded here

