Lineární logika

Lineární logika je verze formální logiky, v níž při odvození dochází k vyřazení antecedentu z množiny formulí. Máme-li například $\{A\}$ a pravidlo (lineární implikaci) $A⊸B$, můžeme odvodit $\{B\}$, tj. A "zmizí" a není již k dispozici pro další pravidla.

Používá se zejména při zpracování přirozeného jazyka pro generování logické reprezentace vět (poprvé byla pro tuto úlohu použita v lexikálně-funkční gramatice). Například význam slovesa věty John loves Mary lze vyjádřit takto:

$\mathrm{\forall }X,Y.f(subj)⇝X⊸f(obj)⇝Y⊸f⇝love(X,Y)$

Protože v lineaární logice platí ${\varphi }_1⊸{\varphi }_2⊸\psi \equiv {\varphi }_1\otimes {\varphi }_2⊸\psi$ a lineární konjunkce je komutativní, lze stejný konstruktor významu použít beze změny také například pro topikalizovanou verzi stejné věty Mary, John loves.

Externí odkazy

• Šablona:Commonscat