Ramy logiczne

W logice ramy logiczne zapewniają środki do zdefiniowania (lub przedstawienia) logiki jako sygnatury w teorii typów wyższego rzędu w taki sposób, że możliwość udowodnienia formuły w oryginalnej logice sprowadza się do problemu zamieszkiwania typu w typie ramowym teoria. Podejście to było z powodzeniem stosowane do (interaktywnego) automatycznego dowodzenia twierdzeń . Pierwszą strukturą logiczną był Automath ; jednak nazwa pomysłu pochodzi od bardziej znanego Edinburgh Logical Framework, LF . Kilka nowszych narzędzi dowodowych, takich jak Isabelle , opiera się na tym pomyśle. W przeciwieństwie do osadzania bezpośredniego podejście oparte na strukturze logicznej umożliwia osadzenie wielu logik w systemie tego samego typu.

Przegląd

Ramy logiczne opierają się na ogólnym traktowaniu składni, reguł i dowodów za pomocą rachunku lambda o typie zależnym . Składnia jest traktowana w stylu podobnym, ale bardziej ogólnym niż system arities Pera Martina-Löfa .

Aby opisać strukturę logiczną, należy podać następujące elementy:

Charakterystyka klasy logiki obiektowej, która ma być reprezentowana;
Odpowiedni metajęzyk;
Charakterystyka mechanizmu reprezentacji logiki obiektowej.

Podsumowuje to:

„ Framework = język + reprezentacja ”.

LF

W przypadku struktury logicznej LF metajęzykiem jest rachunek różniczkowy λΠ . Jest to system typów funkcji zależnych pierwszego rzędu, które są powiązane przez twierdzenia jako zasadę typów z logiką minimalną pierwszego rzędu . Kluczowymi cechami rachunku λΠ jest to, że składa się on z bytów na trzech poziomach: obiektów, typów i rodzajów (lub klas typów lub rodzin typów). Jest predykatywny , wszystkie dobrze napisane terminy są silnie normalizujące , a Church-Rosser i właściwość bycia dobrze wpisanymi to rozstrzygalny . Jednak wnioskowanie o typie jest nierozstrzygalne.

Logika jest reprezentowana w strukturze logicznej LF przez mechanizm reprezentacji ocen jako typów. Jest to inspirowane rozwinięciem przez Pera Martina-Löfa koncepcji osądu Kanta w Wykładach ze Sieny z 1983 roku. Dwa sądy wyższego rzędu $,$ ${\ Displaystyle \ Lambda x \ w JK (x)}$ , , odpowiadają odpowiednio zwykłej i zależnej przestrzeni funkcji. Metodologia sądów-jako-typów polega na tym, że sądy są reprezentowane jako typy ich dowodów. System logiczny jest reprezentowany przez jego sygnaturę, która przypisuje rodzaje i typy skończonemu zbiorowi stałych reprezentujących jego składnię, oceny i schematy $reguł$ Reguły i dowody logiki obiektowej są postrzegane jako prymitywne dowody sądów hipotetyczno-ogólnych ${\ Displaystyle \ Lambda x \ w CJ (x) \ vdash K}$ .

Implementację struktury logicznej LF zapewnia system Twelf na Uniwersytecie Carnegie Mellon . Dwanaście obejmuje

silnik programowania logicznego
rozumowanie metateoretyczne na temat programów logicznych (terminacja, pokrycie itp.)
indukcyjny metalogiczny dowód twierdzeń

Zobacz też

Dalsza lektura

Franka Pfenninga (2002). „Ramy logiczne - krótkie wprowadzenie”. W Helmut Schwichtenberg , Ralf Steinbrüggen (red.). Dowód i niezawodność systemu (PDF) . Springera . ISBN 978-1-4020-0608-1 .
Roberta Harpera , Furio Honsella i Gordona Plotkina . Ramy definiowania logiki . Journal of Association for Computing Machinery, 40(1):143-184, 1993.
Arnon Avron , Furio Honsell, Ian Mason i Randy Pollack. Wykorzystanie rachunku lambda o typie maszynowym do implementacji systemów formalnych na maszynie . Journal of Automated Reasoning, 9:309-354, 1992.
Roberta Harpera. Równania Sformułowanie LF . Raport techniczny, Uniwersytet w Edynburgu , 1988. Raport LFCS ECS-LFCS-88-67.
Robert Harper, Donald Sannella i Andrzej Tarlecki. Ustrukturyzowane prezentacje teorii i reprezentacje logiczne . Annals of Pure and Applied Logic, 67(1-3):113-160, 1994.
Samin Ishtiaq i David Pym. Odpowiednia analiza dedukcji naturalnej . Journal of Logic and Computation 8, 809-838, 1998.
Samin Ishtiaq i David Pym. Modele zasobów Kripkego o typie zależnym, w wiązce -calculus λ $\ displaystyle \ lambda}$ Journal of Logic and Computation 12(6), 1061-1104, 2002.
Per Martin-Löf. „ O znaczeniu stałych logicznych i uzasadnieniach praw logicznych ”. „Nordic Journal of Philosophical Logic”, 1 (1): 11-60, 1996.
Bengt Nordström, Kent Petersson i Jan M. Smith. Programowanie w teorii typów Martina-Löfa . Oxford University Press , 1990. (Nakład książki jest wyczerpany, ale udostępniono bezpłatną wersję ).
Dawid Pym. Uwaga na temat teorii dowodu rachunku różniczkowego $Pi}$ \ Studia Logica 54: 199-230, 1995.
Davida Pyma i Lincolna Wallena . Wyszukiwanie dowodów w rachunku różniczkowym ${\ Displaystyle \ lambda \ Pi$ } W: G. Huet i G. Plotkin (red.), Ramy logiczne, Cambridge University Press, 1991.
Didiera Galmiche i Davida Pyma. Dowód-wyszukiwanie w językach teorii typów: wprowadzenie . Informatyka teoretyczna 232 (2000) 5-53.
Filipa Gardner. Reprezentowanie logiki w teorii typów . Raport techniczny, Uniwersytet w Edynburgu, 1992. Raport LFCS ECS-LFCS-92-227.
Gilles Dowek. Nierozstrzygalność typowalności w rachunku lambda-pi . W M. Bezem, JF Groote (red.), Wpisane Lambda Calculi and Applications. Tom 664 notatek z wykładów z informatyki , 139-145, 1993.
Dawid Pym. Dowody, wyszukiwanie i obliczenia w logice ogólnej . doktorat praca magisterska, Uniwersytet w Edynburgu, 1990.
Dawid Pym. Algorytm unifikacji dla rachunku różniczkowego ${\ Displaystyle \ lambda \ Pi}$ . International Journal of Foundations of Computer Science 3(3), 333-378, 1992.

Linki zewnętrzne

Specyficzne ramy logiczne i implementacje (lista prowadzona przez Franka Pfenninga , ale głównie martwe linki z 1997 r.)