User:Giselle.mnr/Focusing (proof theory)
 | This is not a Wikipedia article: It is an individual user's work-in-progress page, and may be incomplete and/or unreliable. For guidance on developing this draft, see Wikipedia:So you made a userspace draft. Find sources: Google (books · news · scholar · free images · WP refs) · FENS · JSTOR · TWL |
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].
References
[edit]External links
[edit]