From: Brian Atkins (brian@posthuman.com)
Date: Sat Jun 30 2001 - 17:29:24 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?
There was some discussion of this and alternate systems over in SL4
a while back. Sorry I don't recall the exact thread name. Check:
http://sysopmind.com/archive-sl4/
>
> 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.
>
Here's an article that was on the kurzweilai.net newsfeed a few days
back:
http://www.beyond2000.com/news/Jun_01/story_1198.html
it talks about getting software to be able to reason about those "fine
points"
-- Brian Atkins Director, Singularity Institute for Artificial Intelligence http://www.singinst.org/
This archive was generated by hypermail 2.1.5 : Sat Nov 02 2002 - 08:08:23 MST