Next: Podsumowanie Up: autoref Previous: Tematyka badañ
Omówienie uzyskanych wyników
W pierwszym rozdziale pokazali¶my kilka przyk³adów znanych logik, prezentowanych jako instytucje (patrz [GB 92]). Na szczególn± uwagê zas³uguj± instytucje wielorodzajowej czê¶ciowej logiki pierwszego rzêdu z podrodzajami, SubPFOEQ, oraz wielorodzajowej czê¶ciowej logiki pierwszego rzêdu z podrodzajami i generowaniem rodzajów, SubCPFOEQ, bêd±ce instytucjami le¿±cymi u podstaw rozwijanego przez grupê CoFI jêzyka CASL (patrz [CASL 99]), a tak¿e instytucja logiki wy¿szego rzêdu HOL. Instytucja HOL zosta³a zdefiniowana w oparciu o idee przedstawione w ksi±¿kach [GM 93] oraz [Paul 94]. Dziêki temu jest ona bliska opisanym w powy¿szych ksi±¿kach komputerowym systemom wspomagaj±cym dowodzenie twierdzeñ dla logiki wy¿szego rzêdu.
W nastêpnym rozdziale, aby lepiej przystosowaæ instytucjê do opisu logik, nad którymi budujemy specyfikacje strukturalne rozpatrywane w dalszej czê¶ci pracy, wyposa¿yli¶my instytucjê w dwie ,,zgodne" klasy morfizmów D oraz T. Tak wzbogacone instytucje nazwali¶my (D,T)-instytucjami. W rozdziale tym podali¶my tak¿e definicje rozszerzaj±ce w naturalny sposób znane w³asno¶ci systemów logicznych na (D,T)-instytucje (w szczególno¶ci (D,T)-interpolacjê oraz s³ab±-(D,T)-amalgamacjê). Przedstawili¶my równie¿ definicje rozszerzenia reprezentacji instytucji i odwzorowañ instytucji do reprezentacji i odwzorowañ (D,T)-instytucji. Zdefiniowali¶my tak¿e w³asno¶ci ekspansji i s³abej-D-amalgamacji dla reprezentacji i odwzorowañ (D,T)-instytucji, maj±ce kluczowe znaczenie w ostatnich rozdzia³ach pracy.
W Rozdziale 3 przeprowadzili¶my krótk± analizê w³asno¶ci (D,T)-interpolacji dla kilku wybranych logik. W rozdziale tym pokazujemy, ¿e wielorodzajowa (czê¶ciowa) logika pierwszego rzêdu nie posiada w³asno¶ci (D,T)-interpolacji, je¿eli klasy D i T zawieraj± pewne nieró¿nowarto¶ciowe morfizmy sygnatur. Dowodzimy tak¿e, ¿e je¿eli obie klasy morfizmów, D i T, s± ró¿nowarto¶ciowe na nazwach rodzajów to wielorodzajowa czê¶ciowa logika pierwszego rzêdu posiada w³asno¶æ (D,T)-interpolacji. Problemem otwartym zostaje pytanie: czy rozpatrywana tu logika posiada w³asno¶æ (D,T)-interpolacji, gdy tylko jedna z klas, D lub T, jest klas± morfizmów ró¿nowarto¶ciowych na nazwach rodzajów?
W Rozdziale 4, wzoruj±c siê na ideach przedstawionych w pracy [ST 88], zdefiniowali¶my formalizm specyfikacji strukturalnych nad dowoln± (D,T)-instytucj±. Podali¶my systemy dowodzenia, zarówno kompozycyjne jak i niekompozycyjne, s³u¿±ce do wyprowadzania logicznych konsekwencji specyfikacji strukturalnych oraz do wyprowadzania relacji u¶ci¶lania miêdzy specyfikacjami strukturalnymi. G³ównym wynikiem tego rozdzia³u jest twierdzenie, ¿e w³asno¶ci (D,T)-interpolacji oraz s³abej-(D,T)-amalgamacji logiki le¿±cej u podstaw rozpatrywanych specyfikacji, s± w³asno¶ciami decyduj±cymi o pe³no¶ci rozpatrywanego systemu logicznego dla specyfikacji strukturalnych. Pokazali¶my równie¿, ¿e w³asno¶æ s³abej-(D,T)-interpolacji danej logiki jest w³asno¶ci± konieczn± do tego, by rozpatrywany system logiczny dla specyfikacji strukturalnych by³ pe³ny. Niestety, pytanie o warunki minimalne (prócz s³abej-(D,T)-interpolacji) zapewniaj±ce pe³no¶æ pozostaje otwarte. W dalszej czê¶ci rozdzia³u formu³ujemy warunki, przy których systemy logiczne, kompozycyjny i niekompozycyjny, odpowiednio, s³u¿±ce wyprowadzaniu relacji u¶ci¶lania specyfikacji strukturalnych s± poprawne i pe³ne.
W Rozdziale 5 pokazali¶my, w jaki sposób mo¿na ,,dope³niæ'' dany system logiczny dla specyfikacji strukturalnych, tj. w jaki sposób mo¿na udowodniæ os±dy, które w danym systemie logicznym s± prawdziwe, natomiast nie mo¿na ich udowodniæ w tym systemie. Do ,,dope³niania'' systemów logicznych dla specyfikacji strukturalnych u¿yli¶my reprezentacji i odwzorowañ (D,T)-instytucji, zanurzaj±cych ,,s³abszy'' system logiczny w ,,silniejszym'' w taki sposób, by rozpatrywane odwzorowania posiada³y w³asno¶ci: ekspansji oraz s³abej-D-amalgamacji. Odwzorowaniami (D,T)-instytucji, spe³niaj±cymi za³o¿enia g³ównych twierdzeñ tego rozdzia³u, s± miêdzy innymi: odwzorowanie instytucji SubPFOEQ w instytucjê HOL, oraz odwzorowanie instytucji SubCPFOEQ w instytucjê HOL.
Dziêki tym odwzorowaniom, do wyprowadzania logicznych konsekwencji specyfikacji strukturalnych oraz relacji u¶ci¶lania miêdzy specyfikacjami strukturalnymi zbudowanymi nad (D,T)-instytucjami SubPFOEQ oraz SubCPFOEQ, le¿±cymi u podstaw formalizmu CASL, mo¿emy u¿yæ systemu dowodzenia dla specyfikacji strukturalnych zbudowanych nad (D,T)-instytucj± HOL.
W ostatnim rozdziale tej pracy podali¶my warunki, przy których wnioskowania o logicznych konsekwencjach specyfikacji strukturalnych i relacji u¶ci¶lania miêdzy specyfikacjami strukturalnymi zbudowanymi nad dan± (D,T)-instytucj±, mo¿na zredukowaæ do wnioskowania w zwyk³ej logice wy¿szego rzêdu, ju¿ bez operacji budowania specyfikacji strukturalnych. Wyniki prezentowane w tym rozdziale (a w szczególno¶ci zaproponowane schematy regu³) mog± pos³u¿yæ jako ,,pomost'' pomiêdzy systemami dowodzenia dla strukturalnych specyfikacji algebraicznych, a istniej±cymi komputerowo wspomaganymi systemami dowodzenia twierdzeñ takimi, jak system HOL (patrz [GM 93]) czy system Isabelle (patrz [Paul 94]).
Na zakoñczenie pracy przedstawili¶my dwa proste przyk³ady, wraz z ich implementaj± w systemie Isabelle, pokazuj±ce, w jaki sposób mo¿emy przenosiæ wnioskowania o specyfikacjach strukturalnych, zbudowanych nad instytucj± SubCPFOEQ do logiki HOL systemu Isabelle.
Next: Podsumowanie Up: autoref Previous: Tematyka badañ RHS Linux User
2000-06-24