A response to a query on actkm.org listserv
>I wonder how U.S. congressional bills, say, the current
markup on health care for example, would fare against a machine checking for internal
consistency...? Or any bill, for that matter.
>
Well to start with, the machine doesnt set out to check for overall consistency. It uses grammar and semantics to read the text and convert it into a semantic structure. It has to know about all the tricks of legal documents indexed lists, document references, whatever. While doing so, it uses consistent reasoning locally to reduce ambiguity (it cant be eliminated, so it carries multiple meanings forward). In the building process, it is creating a synthesis among
Propositional logic
Existential logic
Temporal logic
Locational logic (the accident was near the hotel)
Relations on relations to any depth
Group theory
Discourse control
As an example (this one out of a slightly contrived spec)
The system shall be capable of simulating a priority request under operational conditions, and, when near depots, shall determine the result of such simulation before deciding to forward a request to MSS.
Building the synthesis requires a machine, as a person would be overwhelmed by the
number of connections required in even a small document, if attempting it manually. No
notation for such a synthesis exists, except for natural language.
Once built, the structure has several uses. I spent some time looking at SOX and
(Australian) AML
A presentation at http://www.inteng.com.au/presentations/aml.ppt
here is an example of a localised definition (AML)
Extended meaning of permanent establishment
(6) For the purposes of paragraph (2)(j) of this clause:
(a) subsection 20(2) has effect as if each reference in that subsection to a country
included a reference to:
(i) a Territory; and
(ii) a Commonwealth place; and
(b) ignore subsection 20(3).
You can see a definition anchored to a document reference, redefinition of a defined term and existential control over a subsection. The system builds the document structure in parallel with the semantic structure, and they often link together as here, as the system has to be able to find a relation in the semantic structure, then move into the document structure and then out again into the semantic structure. The localised definition means you cant reliably search such a document with key words, because the defined terms mean different things in different parts of the document. So the first use is searching using natural language queries, which link into the semantic structure and become active, creating objects, states or sets and driving them through the structure.
The next use is for detection of ambiguities, errors, inconsistencies (including those found by activating the structure), weak statements. The system is also capable of a little arithmetic, so it can check projections over time, and the linkage between numeric values and logical statements (the system is a general purpose problem solving tool which started life in CPM and engineering design you have to save $900 billion over 20 years, that becomes a constraint and it will work backwards on anything that contributes to the total, or show an inconsistency). The semantic structure is active and visualised, so people can push it around and see what happens.
The most important use is that the system is willing to start again at the beginning whenever a change is made the legislation must be read from the beginning to understand exactly what it means, but a large bill grows by accretion you stuff bits in wherever there is an opening, and it is hard to get motivated enough to spend 8 hours reading it from the beginning afresh that is, forgetting everything you have learned from previous drafts.
There may be 6 bills circulating in the House and Senate. Once a bill has been read, a semantic structure has been built. It is then reasonably easy to automatically compare one structure with another.