Hluboký závěr - Deep inference

Hluboký závěr pojmenuje obecnou myšlenku v teorie strukturního důkazu která se rozbíjí s klasikou následný počet zobecněním pojmu struktura umožnit odvození závěru v kontextech vysoké strukturální složitosti. Termín hluboký závěr je obecně vyhrazeno pro důkazní kameny kde je strukturální složitost neomezená; v tomto článku použijeme plytký závěr označovat kameny, které mají strukturální složitost větší než sekvenční kalkul, ale ne neomezeně, i když to v současné době není zavedená terminologie.

Hluboký závěr není v logice důležitý mimo teorii strukturních důkazů, protože jevy, které vedou k návrhu formální systémy s hlubokým úsudkem souvisí s věta o eliminaci řezu. První počet hlubokých závěrů navrhl Kurt Schütte,[1] ale myšlenka v té době nevyvolala velký zájem.

Nuel Belnap navrhováno logika zobrazení ve snaze charakterizovat podstatu teorie strukturního důkazu. The počet struktur byl navržen s cílem poskytnout bezřízenou charakterizaci nekomutativní logika. Obvodový počet byl vyvinut jako systém hluboké inference umožňující výslovně zohlednit možnost sdílení dílčích komponent.

Poznámky

  1. ^ Kurt Schütte. Teorie důkazů. Springer-Verlag, 1977.

Další čtení

  • Kai Brünnler, „Hluboká inference a symetrie v klasických důkazech“ (disertační práce 2004) [1], rovněž publikoval v knižní podobě Logos Verlag (ISBN  978-3-8325-0448-9).
  • Hluboká inference a počet struktur Úvodní a referenční webová stránka o probíhajícím výzkumu v hlubokém závěru.