Assigning Meaning to Proofs: a semantic basis for problem solving environments

Proofs are regarded as expressions which denote evidence. Assigning this meaning to proofs gives them the same status as other algebraic expressions, such as polynomials. There are laws governing equality and simplification of proofs which can be used to explain the notion of constructive validity. A proof is called constructive when the evidence it denotes can be computed from it. A sentence is constructively valid when it has a constructive proof. These proofs turn out to be practical ways to present algorithms as has been demonstrated by an implementation of them in the Nuprl proof development system.