Uniform Proofs

Origin. Miller, Nadathur, Pfenning, Scedrov introduced uniform proofs (1991). Characterizes logic programming proof search. Goal-directed: right rules applied eagerly. Hereditary Harrop formulas: logic programming in higher-order setting. Foundation for λProlog.

Models. Goal-directed proof search. Resolution: bottom-up, clause-based. Uniform proofs: top-down, goal-directed. Right rules applied uniformly until atomic. Characterizes operational semantics of logic programming.

Formalism.

Uniform proof: A proof where right (goal) rules are applied eagerly. Atomic goals resolved against program.

Goal formulas (G) — first-order Horn: G ::= ⊤ | A | G₁ ∧ G₂ | G₁ ∨ G₂ | ∃x.G

Definite formulas (D): D ::= A | G ⊃ A | D₁ ∧ D₂ | ∀x.D

Hereditary Harrop formulas: Larger fragment, obtained by admitting implication and universal quantification in goals — which the Horn grammar above deliberately excludes, since those two clauses are exactly what is being added: G ::= ⊤ | A | G₁ ∧ G₂ | G₁ ∨ G₂ | ∃x.G | D ⊃ G | ∀x.G D ::= A | G ⊃ A | D₁ ∧ D₂ | ∀x.D (unchanged)

The two new goal clauses are what give λProlog its module and scoping behaviour: proving D ⊃ G augments the program with D for the duration of G, and proving ∀x.G introduces a fresh constant. Neither is available in the Horn fragment, where the program is fixed throughout the search.

Uniform proof condition: Every right (goal) rule applied until atomic. Then prove atom from program (backchain).

Backchaining: Δ ⊸ A (atom A proved from program Δ). Match A with clause head, prove body uniformly.

Abstract logic programming: Language ⟨D, G, ⊸⟩ is abstract logic programming language if: Δ ⊢ G iff uniform proof exists.

λProlog: Higher-order hereditary Harrop. Adds λ-terms, higher-order unification.

Symbols.

Symbol	Unicode	Name	Meaning
G	—	Goal	Goal formula
D	—	Definite	Program clause
⊃	U+2283	Implies	Clause implication
⊸	U+22B8	Backchain	Prove from program
∀	U+2200	Universal	Goal quantifier
⊢	U+22A2	Proves	Derivability

Metatheory. Uniform proofs = operational semantics. Soundness: uniform proof → validity. Completeness: for hereditary Harrop, validity → uniform proof. Abstract logic programming: general framework. Higher-order: λProlog, Twelf.

Applies to. Logic programming foundations. λProlog language. Theorem proving. Type inference. Logical frameworks. Meta-programming.

Limitations. Not all logics have uniform proofs. Completeness depends on fragment. Higher-order unification undecidable. Efficiency of search. Specialized applications.