Matemaatilise loogika ja algoritmiteooria kateeder
Mehaanika-matemaatikateaduskond
Moskva Riiklik Ülikool
Esmaspäeval, 6. oktoobril 2003, kl 14.00
Küberneetika Maja (Akadeemia tee 21), ruum B101
Kokkuvõte: Multiplikatiivne mittekommutatiivne lineaarloogika defineeritakse sekventsiarvutuse abil, mis saadakse, kui klassikalise loogika sobivalt formuleeritud standardsest sekventsiarvutusest kõik struktuursed reeglid välja jäetakse.
Nagu iga arvutuse kohta, nii ka multiplikatiivse mittekommutatiivse lineaarloogika kohta kerkib küsimus, kui keerukas on selle arvutuse sekventside tõestatavuse probleem. Hiljuti selgus, et see probleem on NP-täielik. Ettekandes visandatakse selle teoreemi tõestus.
Leitud meetod võimaldab tõestada, et matemaatilises lingvistikas (täpsemalt, kategoorses grammatikas) kasutatava Lambeki arvutuse sekventside tõestatavuse probleem on samuti NP-täielik.
M. Pentus, Lambek calculus is NP-complete, CUNY Ph.D. Program in Computer Science Technical Report TR-2003005, CUNY Graduate Center, New York, May 2003. (ps, pdf)