@article {1521,
title = {Functionality in the Basic Logic of Proofs},
year = {1993},
publisher = {Institut f{\"u}r Informatik und angewandte Mathematik},
abstract = {This report describes the elimination of the injectivity restriction for functional arithmetical interpretations as used in the systems~$\mathcal{PF}$ and~$\mathcal{PFM}$ in the Basic Logic of Proofs. An appropriate axiom system~$\mathcal{PU}$ in a language with operators {\textquoteleft}{\textquoteleft}$x$~is a proof of~$y${\textquoteright}{\textquoteright} is defined and proved to be sound and complete with respect to all arithmetical interpretations based on functional proof predicates. Unification plays a major role in the formulation of the new axioms.},
url = {http://www.iam.unibe.ch/publikationen/techreports/1993/iam-93-004},
author = {Sergei Artemov and Tyko Strassen}
}