They form the most general definition of goal-directed proof-search—in which someone chooses a formula and performs hereditary reductions until the result meets some condition.
The extremal case where reduction only terminates when axioms are reached forms the sub-family of uniform proofs.
[2] Many other sequent calculi has been shown to have the focusing property, notably the nested sequent calculi of both the classical and intuitionistic variants of the modal logics in the S5 cube.
Typically, uniform proofs are not complete for the logic i.e., not all provable sequents or formulas admit a uniform proof, so one considers fragments where they are complete e.g., the hereditary Harrop fragment of intuitionistic logic.
[1] Occasionally, uniform proof-search is implemented in a variant of the sequent calculus for the given logic where context management is automatic, thereby increasing the fragment for which one can define a logic programming language.
[5] The focusing principle was originally classified through the disambiguation between synchronous and asynchronous connectives in linear logic i.e., connectives that interact with the context and those that do not, as a consequence of research on logic programming.
They are now an increasingly important example of control in reductive logic, and can drastically improve proof-search procedures in industry.
The essential idea of focusing is to identify and coalesce the non-deterministic choices in a proof, so that a proof can be seen as an alternation of negative phases (where invertible rules are applied eagerly) and positive phases (where applications of the other rules are confined and controlled).
For negative formulas, provability is invariant under the application of a right rule; and, dually, for a positive formulas provability is invariant under the application of a left rule.
In either case one can safely apply rules in any order to hereditary sub-formulas of the same polarity.
In the case of a right rule applied to a positive formula, or a left rule applied to a negative formula, one may result in invalid sequents e.g., in LK and LJ there is no proof of the sequent
That is, one can commit to focusing on decomposing a formula and its sub-formulas of the same polarity without loss of completeness.
One of the most important operational behaviours a procedure can undergo is backtracking i.e., returning to an earlier stage in the computation where a choice was made.
In focused systems for classical and intuitionistic logic, the use of backtracking can be simulated by pseudo-contraction.
To perform a proof-search the best thing is to choose the left formula, since
is positive, indeed (as discussed above) in some cases there are no proofs where the focus is on the right formula.