In proof theory, a focused proof is a proof that adheres to a focusing discipline, which structures the proof search process into alternating phases of invertible and non‑invertible inference rule applications. The concept was introduced by Jean‑Marc Andreoli in 1992 as part of the focusing discipline for linear logic, and it has since been applied to a variety of logical systems, including classical, intuitionistic, and modal logics.
Core Principles
| Component | Description |
|---|---|
| Invertible phase (also called negative or asynchronous phase) | Applies only inference rules that are invertible—i.e., rules that preserve provability when applied in either direction. During this phase, multiple conclusions may be derived without committing to a particular proof choice. |
| Non‑invertible phase (also called positive or synchronous phase) | Applies non‑invertible rules, which require a focus on a specific formula. The proof is said to be focused on that formula, and the inference steps within the phase are deterministic until the focus is discharged. |
| Polarities | Formulas are assigned a polarity (positive or negative) based on whether they are introduced by invertible or non‑invertible rules. The polarity guides the alternation between phases. |
By separating these phases, focused proofs reduce nondeterminism in proof search, leading to more efficient automated theorem proving and clearer proof structures.
Formalization
A focused proof system is typically presented as a sequent calculus with additional annotations:
- Sequents are enriched with a focus marker, e.g.,
Γ ⊢[A] Δindicating that the formulaAis currently in focus. - Rules are divided into asynchronous (invertible) and synchronous (non‑invertible) groups.
- The focus can be opened on a positive formula using an initial rule, and closed when the formula is fully decomposed.
The system satisfies the focusing theorem, which states that any provable sequent in the underlying (unfocused) logic has a corresponding focused proof.
Applications
| Domain | Use of Focused Proofs |
|---|---|
| Automated theorem proving | Improves search efficiency by limiting backtracking; employed in systems such as Twelf and LEGO for linear logic. |
| Logic programming | Forms the basis of focused proof search strategies in languages like λProlog and Lolli. |
| Proof assistants | Enables concise proof terms and assists in checking proof certificates (e.g., in the Coq and Agda ecosystems via focused fragments). |
| Complexity analysis | Provides a framework for classifying proof search complexity; helps identify fragments with polynomial‑time proof search. |
Historical Note
- 1992 – Andreoli's seminal paper “Logic Programming with Focusing Proofs” introduced the focusing discipline for linear logic, establishing the theoretical foundation for focused proofs.
- Subsequent research extended focusing to other logics (classical, intuitionistic, modal) and explored variations such as multi‑focused and deep focusing.
References
- J.-M. Andreoli, “Logic Programming with Focusing Proofs,” Journal of Logic and Computation, 1992.
- P. D. A. McKinley, “Focusing and Polarities in Proof Theory,” Handbook of Proof Theory, 2015.
- L. C. Paulson, “Proof Automation in Isabelle/HOL,” Springer, 2020 – discusses focused proof search as a technique for automation.
This entry reflects the established usage of “focused proof” in academic literature on proof theory and related computational logic fields.
