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
⊢	U+22A2	Turnstile / Derivability	Δ ⊢ G: the goal G follows from the program Δ
⊸	U+22B8	Multimap / Backchaining	Here: an atom resolved against a clause head
⊃	U+2283	Superset of / Implication	Clause implication G ⊃ A, and D ⊃ G in Harrop goals
∧	U+2227	Conjunction	Splits a goal into subgoals
∨	U+2228	Disjunction	Branches a goal; a choice point in search
∀	U+2200	Universal quantifier	In clauses always; in goals only for hereditary Harrop
∃	U+2203	Existential quantifier	Goal quantifier, witnessed by unification
⊤	U+22A4	Top / Truth	The immediately satisfied goal
λ	U+03BB	Lambda	Term-level abstraction in λProlog
Δ	U+0394	Delta / Program	The clause database, extended by D ⊃ G goals
⟨ ⟩	U+27E8, U+27E9	Angle brackets	Enclose the triple defining an abstract logic programming language
G	—	Goal formula	Right-hand side of the search judgment
D	—	Definite formula	Program clause
::=	—	Grammar production	Defines the goal and clause fragments

Metatheory. Miller, Nadathur, Pfenning and Scedrov (1991) defined an abstract logic programming language as a triple of definite formulas, goal formulas and a provability relation in which a goal is derivable from a program exactly when it has a uniform proof, and proved that first-order and higher-order hereditary Harrop formulas satisfy the condition while full intuitionistic logic does not — p ∨ q ⊢ p ∨ q is derivable but has no uniform proof, since uniformity forces the disjunction rule and neither disjunct alone follows. The theorem is what makes goal-directed search a complete strategy rather than a heuristic; it is proved by permuting rules in cut-free sequent derivations, so it rests on cut elimination for the ambient logic. The notion extends downward into linear logic: Hodas and Miller (1994) showed the fragment Lolli is an abstract logic programming language, and Miller's Forum (1996) presents all of linear logic as one using multiple-conclusion uniform proofs. In focusing terms a uniform proof is a focused proof with every atom negative.

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

Limitations. Uniformity is a property of a fragment, not of a logic: outside hereditary Harrop the equivalence fails, so classical logic, intuitionistic logic with disjunctive or existential program clauses, and any language wanting negation as a connective rather than as failure all fall outside, and each new connective demands a fresh completeness proof. The higher-order case gains expressiveness and loses decidability — λProlog needs higher-order unification, undecidable by Huet's theorem, so implementations restrict to Miller's pattern fragment and defer the rest as constraints, which makes the operational semantics depend on a solver rather than on the calculus. Goal-directed search is complete without being efficient: the choice of clause stays don't-know nondeterministic, and the depth-first execution actually implemented is incomplete, so implementations are unfaithful to the theorem that justifies them.