savannah-register-public
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Savannah-register-public] [task #3924] Submission of Isar Mathematical


From: Slawomir Kolodynski
Subject: [Savannah-register-public] [task #3924] Submission of Isar Mathematical Library
Date: Wed, 23 Mar 2005 23:54:03 +0000
User-agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.7.5) Gecko/20041111 Firefox/1.0 (Debian package 1.0-2)

URL:
  <http://savannah.gnu.org/task/?func=detailitem&item_id=3924>

                 Summary: Submission of Isar Mathematical Library
                 Project: Savannah Administration
            Submitted by: slawekk
            Submitted on: Wed 03/23/2005 at 23:54
         Should Start On: Wed 03/23/2005 at 00:00
   Should be Finished on: Sat 04/02/2005 at 00:00
                Category: Project Approval
                Priority: 5 - Normal
                  Status: None
                 Privacy: Public
        Percent Complete: 0%
             Assigned to: None
             Open/Closed: Open
                  Effort: 0.00

    _______________________________________________________

Details:


Site Admin. Approval/Edition URL:
 <https://savannah.gnu.org/admin/groupedit.php?group_id=7455>


###### ORIGINAL SUBMISSION DETAILS ######

System Group Name:
-----------------
  isarmathlib


Full Name:
----------
  Isar Mathematical Library
  

Type:
-----
  non-GNU


License:
-------- 
  Modified BSD License


Other License: 
--------------
  


Description:
------------
  The goal of the project is to create a library of formalized mathematics,
written for the Isabelle/Isar theorem prover.
In formalized mathematics definitions and theorems are written in a computer
language (Isar in this case) so that they can be verified by a machine.

Preliminary sources of the IsarMathLib project can be found at
http://www.skokodyn.com/IsarMathLib/ .

For some background on formalized mathematics I suggest
ftp://ftp.mcs.anl.gov/pub/qed/manifesto



Other Software Required:
------------------------
  The project depends on the Isabelle/Isar theorem prover 
(http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html),
distributed under the BSD license.




Other Comments:
---------------
  

#########################################







    _______________________________________________________

Reply to this item at:

  <http://savannah.gnu.org/task/?func=detailitem&item_id=3924>

_______________________________________________
  Message sent via/by Savannah
  http://savannah.gnu.org/





reply via email to

[Prev in Thread] Current Thread [Next in Thread]