Терең қорытынды - Deep inference

Терең қорытынды жалпы идеяны атайды құрылымдық дәлелдеу теориясы бұл классиканы бұзады дәйекті есептеу ұғымын жалпылау арқылы құрылым құрылымның күрделілігі жоғары контексте тұжырым жасауға мүмкіндік беру. Термин терең қорытынды жалпыға арналған дәлелдер мұнда құрылымдық күрделілік шексіз; осы мақалада біз қолданатын боламыз таяз емес қорытынды құрылымдық күрделілігі дәйекті есептеулерден үлкен, бірақ шексіз емес калькуляцияға сілтеме жасау, дегенмен бұл қазіргі кезде қалыптасқан терминология емес.

Терең тұжырым логикалық тұрғыдан құрылымдық дәлелдеу теориясынан тыс маңызды емес, өйткені ұсынысқа әкелетін құбылыстар ресми жүйелер терең тұжырыммен бәрі байланысты элиминациялық теорема. Терең қорытынды шығарудың алғашқы есебін ұсынған Курт Шютте,[1] бірақ бұл идея ол кезде үлкен қызығушылық тудырмады.

Нуэль Белнап ұсынды логиканы көрсету құрылымдық дәлелдеу теориясының мәнін сипаттауға тырысуда. The құрылымдардың есебі сипаттамасын беру үшін ұсынылды коммутативті емес логика. Циркулентті есептеу ішкі компоненттермен бөлісу мүмкіндігін нақты есепке алуға мүмкіндік беретін терең қорытынды жүйесі ретінде жасалған.

Ескертулер

  1. ^ Курт Шютте. Дәлелдеу теориясы. Springer-Verlag, 1977 ж.

Әрі қарай оқу

  • Кай Брюннлер, «Классикалық дәлелдердегі терең қорытынды және симметрия» (кандидаттық диссертация 2004) [1], сонымен қатар Logos Verlag кітап түрінде басылған (ISBN  978-3-8325-0448-9).
  • Терең қорытынды және құрылымдардың есебі Терең қорытынды жасау бойынша жүргізіліп жатқан зерттеулер туралы кіріспе және анықтамалық веб-парақ.