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): G ::= A | G₁ ∧ G₂ | G₁ ∨ G₂ | ∃x.G | ⊤ | D ⊃ G | ∀x.G

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

Hereditary Harrop formulas: Larger fragment with implications and universals in goals. G ::= ... | D ⊃ G | ∀x.G

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

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

Abstract logic programming: Language ⟨D, G, —o⟩ 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
—o	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.