Building Interactive Digital Libraries of Formal Algorithmic Knowledge

This is a project to design and create a software system for sharing formal algorithmic mathematics among theorem provers, and for making formal algorithmic mathematics accessible to people who value verified accounts of algorithms. The project is also committed to creating interesting specimens of...

Full description

Saved in:
Bibliographic Details
Main Author: Constable, Robert L
Format: Report
Language:English
Subjects:
ALGORITHMS
Computer Programming and Software
COMPUTER PROGRAMS
DIGITAL LIBRARIES
INFORMATION INTENSIVE INFRASTRUCTURES
Information Science
KNOWLEDGE BASED SYSTEMS
KNOWLEDGE MANAGEMENT
MATHEMATICS
Numerical Mathematics
THEOREM PROVING
VERIFICATION
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:This is a project to design and create a software system for sharing formal algorithmic mathematics among theorem provers, and for making formal algorithmic mathematics accessible to people who value verified accounts of algorithms. The project is also committed to creating interesting specimens of formally explained algorithms. Our work enables a new approach to CIP/SW; we call information-intensive infrastructure protection. We describe the rationale for this approach in this report.