Checking Proofs in the Metamathematics of First Order Logic

Abstract

This is a report on some of the first experiments of any size carried out using the new first order proof checker FOL. The authors present two different first order axiomatizations of the metamathematics of the logic which FOL itself checks and show several proofs using each one. The difference between the axiomatizations is that one defines the metamathematics in a many sorted logic, the other does not.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Aug 01, 1974
Accession Number
ADA007562

Entities

People

  • Mario Aiello
  • Richard W. Weyhrauch

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I

DTIC Thesaurus Topics

  • Abstracts
  • Artificial Intelligence
  • Buildings And Structures
  • Case Studies
  • Classification
  • Computer Science
  • Computers
  • Geometry
  • Language
  • Logic
  • Metamathematics
  • Military Research
  • Motivation
  • Projective Geometry
  • Security
  • Sequences
  • Theorems

Readers

  • Aerospace logistics and air mobility.
  • Computational Linguistics
  • International Journalism and Media Studies.