Equilibrium Logic

Origin. Pearce (1996). Logic programming semantics. Here-and-there logic. Answer sets as equilibria. Foundation for answer set programming.

Models. HT-models: pairs (H, T) with H ⊆ T. "Here" and "there" worlds. Equilibrium: minimal H for given T. Connection to stable models.

Formalism.

HT-model: (H, T) where H ⊆ T ⊆ At. T: "there" world (classical). H: "here" world (constructive).

Satisfaction: (H,T) ⊨ p iff p ∈ H (H,T) ⊨ ¬φ iff (T,T) ⊭ φ (H,T) ⊨ φ → ψ iff (H,T) ⊭ φ or (H,T) ⊨ ψ, and (T,T) ⊭ φ or (T,T) ⊨ ψ

Total model: (T,T): H = T. Classical model.

Equilibrium model: (T,T) ⊨ φ and no (H,T) ⊨ φ with H ⊂ T. T is minimal model of φ given T-satisfaction.

Stable model connection: T is stable model of program P iff (T,T) is equilibrium model of P. Gelfond-Lifschitz reduct.

Strong equivalence: φ ≡_s ψ iff ∀context C: φ ∧ C ≡ ψ ∧ C Same equilibrium models in all contexts. Characterized by HT-equivalence.

Here-and-there logic: Intermediate logic. Between intuitionistic and classical. Three values: false, here-only, there.

Symbols.

Symbol	Unicode	Name	Meaning
(H,T)	—	HT-model	Here-there pair
≡_s	—	Strong equiv	Same in all contexts
⊨_HT	—	HT-satisfaction	Three-valued

Metatheory. Complete for HT-logic. Strong equivalence decidable. Characterizes ASP. Extensions to first-order.

Applies to. Answer set programming. Non-monotonic reasoning. Knowledge representation. Planning.

Limitations. Technical machinery. Different from classical intuition. Limited to certain syntax forms.