Głębokie wnioskowanie

Głębokie wnioskowanie nazywa ogólną ideę w teorii dowodu strukturalnego , która zrywa z klasycznym rachunkiem sekwencyjnym , uogólniając pojęcie struktury , aby umożliwić wnioskowanie w kontekstach o dużej złożoności strukturalnej. Termin głębokie wnioskowanie jest ogólnie zarezerwowany dla rachunków dowodowych , w których złożoność strukturalna jest nieograniczona; w tym artykule będziemy używać niepłytkiego wnioskowania w odniesieniu do rachunków, które mają złożoność strukturalną większą niż rachunek sekwencyjny, ale nie bez ograniczeń, chociaż nie jest to obecnie ustalona terminologia.

Głębokie wnioskowanie nie jest ważne w logice poza teorią dowodu strukturalnego, ponieważ wszystkie zjawiska, które prowadzą do propozycji systemów formalnych z głębokim wnioskowaniem, są związane z twierdzeniem o eliminacji cięcia . Pierwszy rachunek głębokiego wnioskowania zaproponował Kurt Schütte , ale pomysł ten nie wzbudził wówczas większego zainteresowania.

Nuel Belnap zaproponował logikę wyświetlania , próbując scharakteryzować istotę teorii dowodu strukturalnego. Rachunek struktur został zaproponowany w celu uzyskania bezobsługowej charakterystyki logiki nieprzemiennej . Rachunek Cirquent został opracowany jako system głębokiego wnioskowania pozwalający na jawne uwzględnienie możliwości współdzielenia składowych.

Dalsza lektura

•   Kai Brünnler, „Deep Inference and Symmetry in Classical Proofs” ( praca doktorska 2004 ), również opublikowany w formie książkowej przez Logos Verlag ( ISBN 978-3-8325-0448-9 ).
• Deep Inference and the Calculus of Structures Intro i referencyjna strona internetowa poświęcona trwającym badaniom w zakresie głębokiego wnioskowania.