Axioms and Theorems for Integers, Lists and Finite Sets in Logic for Computable Functions (LCF)

reportActive / Technical Report | Accession Number: AD0758651 | Open PDF

Abstract:

LCF Logic for Computable Functions is being promoted as a formal language suitable for the discussion of various problems in the Mathematical Theory of Computation MTC. To this end, several examples of MTC problems have been formalised and proofs have been exhibited using the LCF proof-checker. However, in these examples, there has been a certain amount of ad-hoc-ery in the proofs namely, many mathematical theorems have been assumed without proof and no axiomatisation of the mathematical domains involved was given. The paper describes a suitable mathematical environment for future LCF experiments and its axiomatic basis. The environment developed, deemed appropriate for such experiments, consists of a large body of theorems from the areas of integer arithmetic, list manipulation and finite set theory.

Author(s):
Newey, Malcolm
Author Organization(s):
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Supplementary Note:
DOI: 10.21236/AD0758651
Pagination:
0059

Security Markings

DOCUMENT & CONTEXTUAL SUMMARY

Distribution:
Approved For Public Release, Document Partially Illegible
Distribution Statement:
Approved For Public Release; Distribution Is Unlimited. Document Partially Illegible.

RECORD

Collection: TR
Identifying Numbers
Report Number(s):
STAN-CS-73-330, AIM-184
Contract/Grant Number(s):
SD-183, NSR-05-020-500
Project Number(s):
ARPA ORDER-457
Monitor Series:
DARPA
 Subject Terms
Joint Capability Areas:
JCA_5_Command and Control; JCA_5.2.2_Develop Knowledge and Situational Awareness; JCA_5.2_Understand; JCA_1.2.6_Concepts; JCA_5.3_Planning; JCA_1.2.7_Experimentation; JCA_6_Net Centric; JCA_4.5.1_Contract Support Integration; JCA_4.5_Operational Contract Support; JCA_6.2.1_Information Sharing; JCA_6.2.2_Computing Services; JCA_6.4.1_Secure Information Exchange; JCA_1.2_Force Preparation; JCA_1_Force Support; JCA_1.2.5_Lessons Learned; JCA_6.2_Enterprise Services; JCA_6.4_Information Assurance
Modernization Areas:
Autonomy
Communities of Interest:
Autonomy
Descriptor(s):
*MATHEMATICAL LOGIC, ARTIFICIAL INTELLIGENCE, COMPILERS, COMPUTER PROGRAMMING, FUNCTIONS(MATHEMATICS), NUMBER THEORY, SEMANTICS, SET THEORY, THEOREMS
Field(s)/Group(s):
Theoretical Mathematics
Keyword(s):
ARITHMETIC, AXIOMS
Report Date:
1973 Jan 01