Navratil, G. (2002). Formalisierung von Gesetzen : am Beispiel des Österreichischen Allgemeinen Grundbuchgesetzes [Dissertation, Technische Universität Wien]. reposiTUm. https://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-10040
E120 - Institut für Geoinformation und Landesvermessung
-
Date (published):
2002
-
Keywords:
Österreich; Algebraisches Modell
de
Abstract:
Die Arbeit untersucht Gesetze und Algebra. Auf den ersten Blick sehen diese beiden Themen sehr unterschiedlich aus. Gesetze sind Textwerke, die das Zusammenleben der Menschen regeln, Algebren sind eine mathematische Methode zur Beschreibung von Eigenschaften. Bei näherer Betrachtung fällt allerdings auf, dass in beiden Fällen Systeme modelliert werden und sich die verwendeten Methoden sehr ähnlich sind. In beiden Fällen wird mit Klassenbildung, Abstraktion und axiomatischer Definition gearbeitet. Anhand eines Vergleiches der beiden Modellierungssysteme wird eine Methodik entwickelt, wie man Gesetze in Algebren übersetzen kann. Drei Schritte sind notwendig: • Identifikation der Klassen • Definition von Datentypen, Operationen und Axiomen • Testen anhand einer einfachen Realisierung Wichtig ist dabei vor allem, welchen Beitrag einzelne Paragraphen liefern. Ein Paragraph kann einen Datentyp spezifizieren, eine Operation beschreiben oder ein Axiom festlegen. Die Beschreibung der Operationen zerfällt wiederum in drei Bereiche. Einerseits muss die Notwendigkeit der Operation gegeben sein. Zusätzlich benötigt eine Operation Parameter und produziert ein Ergebnis. Schließlich muss die Operation auch noch einer Klasse zugeordnet werden. All diese Aufgaben werden von Paragraphen erfüllt. Dabei wirken oft mehrere Paragraphen zusammen um eine Aufgabe gemeinsam zu lösen. Die entwickelte Methode wurde anhand eines Beispiels getestet. Das Testbeispiel ist das österreichische allgemeine Grundbuchsgesetz. Dieses wurde ohne Verwendung von Praxiswissen in ein algebraisches Modell überführt. Alle notwendigen Informationen wurden dabei dem allgemeinen Grundbuchsgesetz oder anderen Gesetzen (z.B. dem allgemeinen bürgerlichen Gesetzbuch) entnommen. Die algebraische Umsetzung wurde in Haskell, einer funktionalen Programmiersprache, durchgeführt. Der Vorteil liegt in der mathematischen Reinheit der Sprache, die sie anderen Programmiersprachen voraus hat und in der Ausführbarkeit, die sie von der Mathematik abhebt.
de
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.