User:Giselle.mnr/Focusing (proof theory)

Focusing is a sound and complete discipline for proof search in sequent calculus which restricts the search space by reducing the number of applicable inference rules at each step. It is based on the observation that invertible rules can be eagerly applied during a proof, since they only generate validity preserving premises and consequently do not require backtracking. It was first proposed by Andreoli for linear logic [TODO: add reference] and has been later applied to other logics (e.g. classical [ref] and intuitionistic [ref]) and other calculi (e.g. nested sequents) [TODO: add reference].

External links

• www.example.com