From: Robert J. Bradbury (bradbury@aeiveos.com)
Date: Sat Jun 30 2001 - 17:02:56 MDT
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
This archive was generated by hypermail 2.1.5 : Sat Nov 02 2002 - 08:08:23 MST