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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 1973
Accession Number
AD0758651

Entities

People

  • Malcolm Newey

Organizations

  • Stanford University

Tags

Communities of Interest

  • Air Platforms
  • Autonomy

DTIC Thesaurus Topics

  • Arithmetic
  • Artificial Intelligence
  • Classification
  • Complex Systems
  • Computations
  • Computer Science
  • Computers
  • Environment
  • Formal Languages
  • Language
  • Sequences
  • Set Theory
  • Standards
  • Theorems
  • Theory Of Computation

Fields of Study

  • Mathematics

Readers

  • Business Analytics
  • Mathematical Modeling and Probability Theory.