From: Ross A. Finlayson (raf@tiki-lounge.com)
Date: Sat Jun 30 2001 - 19:09:09 MDT
Robert J. Bradbury wrote:
> I ran across links on attempts to reconstruct mathematics
> as a computerized entity. These are known as
> The QED project: http://www-unix.mcs.anl.gov/qed/
> and a subset:
> The Mizar Project: http://mizar.org/
>
> I've looked a little at the formal language descriptions
> and they seem to be quite robust. Anyone have any knowledge
> or opinions regarding how this might impact automated
> reasoning or even AI?
>
> Do efforts like this lay the groundwork for similar
> systems for "law"? I.e. you have a mapping from
> natural language into a formal "law language"
> in which contracts are written. Violations
> would be detected by computerized agents and
> disputes would be resolved by automated reasoning
> systems (eliminating some of the costly components
> such as judges and juries). You might still need lawyers
> to mediate the fine points of the translations but presumably
> most of this would be automated too.
>
> Robert
I think the term you consider about law is called "jurimetrics", where
there is a metricization of the law.
In terms of those groups you mention, they are not about computer proof
checking as much as mathematical foundations. The Mizar project
specifies a symbolic mathematical language as part of its verification
scheme wherein additions to its base of foundations are presented in the
Mizar language which is presumed rigorous and machine-verifiable, where
it is. The QED project is moreso a community group based upon
discussion of mathematical foundations, and not machine verification per
se.
About the jurimetrics, one thing is that it would enable that people
would be able to preserve the integrity of their privacy somewhat more
easily, were it an actual fair system of jurimetrics. In terms of the
formalizations of all the implicit microtransactions that occur, that
would seem to be related to but not encompassing of jurimetrics, which
would be more about the extreme codification of all laws.
Ross F.
-- Ross Andrew Finlayson Finlayson Consulting Ross at Tiki-Lounge: http://www.tiki-lounge.com/~raf/ "It's always one more." - Internet multi-player computer game player
This archive was generated by hypermail 2.1.5 : Sat Nov 02 2002 - 08:08:23 MST