Search Constraints
You searched for:
Author
Weyhrauch, Richard W.
Remove constraint Author: Weyhrauch, Richard W.
Genre
technical reports
Remove constraint Genre: technical reports
1 - 3 of 3
Number of results to display per page
Search Results
- Title:
- Checking proofs in the metamathematics of first order logic.
- Author:
- Aiello, Mario and Weyhrauch, Richard W.
- Author (no Collectors):
- Aiello, Mario and Weyhrauch, Richard W.
- 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.
- Topic:
- Computer science
- Subject:
- Stanford University. Computer Science Department
- Language:
- English
- Physical Description:
- 1 text file
- Publication Info:
- cau and Stanford (Calif.)
- Date:
- August 01, 1974
- Place created:
- Stanford (Calif.)
- Imprint:
- Stanford (Calif.), August 1, 1974
- Genre:
- technical reports
- Identifier:
- CS-TR-1974-467
- Repository:
- Stanford University. Libraries. Department of Special Collections and University Archives
- Collection:
- Stanford University, Department of Computer Science, Technical Reports and Stanford Artificial Intelligence Laboratory records, 1963-2009
- Manuscript number:
- 3840/2
- Title:
- The semantics of PASCAL in LCF.
- Author:
- Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard W.
- Author (no Collectors):
- Aiello, Luigia, Aiello, Mario, and Weyhrauch, Richard W.
- Description:
- We define a semantics for the arithmetic part of PASCAL by giving it an interpretation in LCF, a language based on the typed $\lambda$-calculus. Programs are represented in terms of their abstract syntax. We show sample proofs, using LCF, of some general properties of PASCAL and the correctness of some particular programs. A program implementing the McCarthy Airline reservation system is proved correct.
- Topic:
- Computer science
- Subject:
- Stanford University. Computer Science Department
- Language:
- English
- Physical Description:
- 1 text file
- Publication Info:
- cau and Stanford (Calif.)
- Date:
- August 01, 1974
- Place created:
- Stanford (Calif.)
- Imprint:
- Stanford (Calif.), August 1, 1974
- Genre:
- technical reports
- Identifier:
- CS-TR-1974-447
- Repository:
- Stanford University. Libraries. Department of Special Collections and University Archives
- Collection:
- Stanford University, Department of Computer Science, Technical Reports and Stanford Artificial Intelligence Laboratory records, 1963-2009
- Manuscript number:
- 3840/2
- Title:
- Final report: Basic Research in Artificial Intelligence and Foundations of Programming.
- Author:
- McCarthy, John, Binford, Thomas O., Luckham, David C., Manna, Zohar, Weyhrauch, Richard W., and Earnest, Les
- Author (no Collectors):
- McCarthy, John, Binford, Thomas O., Luckham, David C., Manna, Zohar, Weyhrauch, Richard W., and Earnest, Les
- Description:
- Recent research results are reviewed in the areas of formal reasoning, mathematical theory of computation, program verification, and image understanding.
- Topic:
- Computer science
- Subject:
- Stanford University. Computer Science Department
- Language:
- English
- Physical Description:
- 1 text file
- Publication Info:
- cau and Stanford (Calif.)
- Date:
- May 01, 1980
- Place created:
- Stanford (Calif.)
- Imprint:
- Stanford (Calif.), May 1, 1980
- Genre:
- technical reports
- Identifier:
- CS-TR-1980-808
- Repository:
- Stanford University. Libraries. Department of Special Collections and University Archives
- Collection:
- Stanford University, Department of Computer Science, Technical Reports and Stanford Artificial Intelligence Laboratory records, 1963-2009
- Manuscript number:
- 3840/2
