Proof Polynomials vs. lambda-terms

Abstract

The Logic of Proofs provides a basic framework for the formalization of reasoning about proofs. It incorporates proof terms into the propositional language, using labeled logical operators "t:" with the intended reading of t:F being "T is a proof of F". In the current paper we demonstrate how the typed lambda calculus and the modal lambda-calculus can be realized in the Logic of Proofs.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 31, 1998
Accession Number
ADA344395

Entities

People

  • S. N. Artemov

Organizations

  • University of California, Berkeley

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Arithmetic
  • Artificial Intelligence
  • Calculus
  • Classification
  • Information Operations
  • Intelligent Systems
  • Language
  • Mathematics
  • Military Research
  • Polynomials
  • Recursive Functions
  • Semantics
  • Specifications
  • Standards
  • Theory Of Computation

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.