Checking proofs in the metamathematics of first order logic.

Available Online:

https://purl.stanford.edu/dd609fp0649

Title:

Checking proofs in the metamathematics of first order logic.

Relation:

Stanford University. Libraries. Department of Special Collections and University Archives3840/2https://purl.stanford.edu/dd609fp0649, Stanford University, Department of Computer Science, Technical Reports, and Stanford Artificial Intelligence Laboratory records, 1963-2009

PublishDate:

2021-02-05T23:20:06Z

Description:

This is a report on some of the first experiments of any size carried out using the new first order proof checker FOL. We 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.

Identifier:

CS-TR-1974-467

Contributor:

Aiello, Mario (autAuthor) and Weyhrauch, Richard W. (autAuthor)

Type:

Text and technical reports

Date:

1974-08-01

Language:

engEnglish

Format:

1 text file, technical reports, and image/jpeg

Subject:

Stanford University. Computer Science Department and Computer science

Thumbnail:

{data={format=image/jpeg, width=310, @id=https://stacks.stanford.edu/image/iiif/dd609fp0649%2Fdd609fp0649_01/full/!400,400/0/default.jpg, @type=dctypes:Image, service={data={@context=http://iiif.io/api/image/2/context.json, @id=https://stacks.stanford.edu/image/iiif/dd609fp0649%2Fdd609fp0649_01, profile=http://iiif.io/api/image/2/level2.json}}, height=400}}

Exhibit Tags:

Technical Report