ERRATUM FOR UNIFORM PROOFS AS A FOUNDATION FOR LOGIC PROGRAMMING

Dale Miller  Computer and Information Science Department

University of Pennsylvania, Philadelphia, PA 19104

Gopalan Nadathur  Computer Science Department

Duke University, Durham, NC 27706

Frank Pfenning  Computer Science Department

Carnegie Mellon University, Pittsburgh, PA 15213

Andre Scedrov  Mathematics Department

University of Pennsylvania, Philadelphia, PA 19104

A. Felty has pointed out an error in the proof of Lemma 11 in the paper “Uniform Proofs as a Foundation for Logic Programming” (Annals of Pure and Applied Logic, 1991 (51), 125–157). The proof is based on a claim of the following sort: If Δ is an arbitrary set of D-formulas and G′ is a G-formula such that Δ ⟶ G′ has an M′-proof of height h, then (i) if G′ = G_{1} ∧ G_{2}, the sequents Δ ⟶ G_{1} and Δ ⟶ G_{2} have M′-proofs of height less than h, (ii) etc. This claim is not correct, the sequent

P a ⊃ Q, ∀x.P x, R ⟶ Q ∧ R

providing a counterexample. This sequent has an M′-proof of height 3 (the last inference rule in this proof being ⊃-L), but P a ⊃ Q, ∀x.P x, R ⟶ Q does not have an M′-proof of height less than 3.

However, Lemma 11 is still true. In constructing its proof the measure in the claim mentioned above needs to be changed. In particular, the measure of the height of a proof must be replaced by the size of a proof, the latter measure being a count of the number of occurrences of sequents in the proof. The outlined proofs of the claim are correct if this measure is used instead.