Logické programování - Logic programming

Přesměrování „na základě pravidel“ zde. Metodu strojového překladu najdete v tématu Strojový překlad na základě pravidel . Metody strojového učení najdete v tématu strojové učení založené na pravidlech .
Programovací paradigmata

Logické programování je paradigma programování, které je z velké části založeno na formální logice . Jakýkoli program napsaný v logickém programovacím jazyce je sada vět v logické formě, vyjadřující fakta a pravidla o nějaké problémové oblasti. Mezi hlavní rodiny logických programovacích jazyků patří Prolog , programování sad odpovědí (ASP) a Datalog . Ve všech těchto jazycích jsou pravidla napsána ve formě klauzulí :

H :- B1, …, Bn.

a jsou čteny deklarativně jako logické důsledky:

H if B1 and … and Bn.

Hse nazývá hlavou pravidla a ... se nazývá tělo . Fakta jsou pravidla, která nemají tělo a jsou napsána ve zjednodušené formě: B1Bn

H.

V nejjednodušším případě, ve kterém H, ..., jsou všechny atomové vzorce , se tyto klauzule nazývají určité klauzule nebo Hornovy klauzule . Existuje však mnoho rozšíření tohoto jednoduchého případu, z nichž nejdůležitější je případ, kdy podmínky v těle klauzule mohou být také negacemi atomových vzorců. Logické programovací jazyky, které obsahují toto rozšíření, mají schopnosti reprezentace znalostí nemonotonické logiky . B1Bn

V ASP a Datalogu mají logické programy pouze deklarativní čtení a jejich provádění se provádí pomocí procedury důkazu nebo generátoru modelu, jehož chování není určeno k ovládání programátorem. V rodině jazyků Prolog však mají logické programy také procedurální interpretaci jako postupy snižování cílů:

řešit H, řešit a ... a řešit .B1Bn

Zvažte následující klauzuli jako příklad:

fallible(X) :- human(X).

na příkladu, který použil Terry Winograd k ilustraci plánovače programovacího jazyka . Jako klauzuli v logickém programu ji lze použít jak jako proceduru pro testování, zda Xje fallibletestováním, zda Xje human, tak jako proceduru pro nalezení an, Xkterá je falliblenalezením, Xkterá je human. I skutečnosti mají procedurální výklad. Například klauzule:

human(socrates).

lze použít jak jako proceduru k ukázání, která socratesje human, tak jako proceduru k nalezení, Xkterá je human„přiřazením“ socratesk X.

Deklarativní čtení logických programů může programátor použít k ověření jejich správnosti. Logické metody transformace programu lze navíc použít také k transformaci logických programů na logicky ekvivalentní programy, které jsou efektivnější. V rodině logických programovacích jazyků Prolog může programátor ke zlepšení efektivity programů použít také známé chování prováděcího mechanismu při řešení problémů.

Dějiny

Využití matematické logiky k reprezentaci a spouštění počítačových programů je také rysem lambda kalkulu , vyvinutého Alonzo Churchem ve 30. letech 20. století. První návrh na použití klauzální formy logiky pro reprezentaci počítačových programů však předložil Cordell Green . To využilo axiomatizaci podmnožiny LISP spolu se znázorněním vztahu vstup-výstup k výpočtu vztahu simulací provádění programu v LISP. Foster a Elcock's Absys na druhé straně použili kombinaci rovnic a lambda kalkulu v aserciálním programovacím jazyce, který nijak neomezuje pořadí, ve kterém jsou operace prováděny.

Logické programování v jeho současné podobě lze vysledovat v debatách na konci šedesátých a na začátku sedmdesátých let o deklarativních versus procedurálních reprezentacích znalostí v umělé inteligenci . Zastánci deklarativních reprezentací pracovali zejména na Stanfordu , spojeném s Johnem McCarthym , Bertramem Raphaelem a Cordellem Greenem, a v Edinburghu , s Johnem Alanem Robinsonem (akademický návštěvník Syracuse University ), Pat Hayesem a Robertem Kowalskim . Obhájci procedurálních reprezentací byli soustředěni hlavně na MIT pod vedením Marvina Minskyho a Seymoura Paperta .

Ačkoli to bylo založeno na důkazních metodách logiky, Planner , vyvinutý na MIT, byl prvním jazykem, který se objevil v tomto proceduralistickém paradigmatu. Planner představoval vyvolání procedurálních plánů podle cílů z cílů (tj. Snížení cílů nebo zpětné zřetězení ) az tvrzení (tj. Zřetězení vpřed ). Nejvlivnější implementací Planneru byla podmnožina Planneru, zvaná Micro-Planner, kterou implementovali Gerry Sussman , Eugene Charniak a Terry Winograd . Byl použit k implementaci winogradského programu porozumění přirozenému jazyku SHRDLU , který byl v té době mezníkem. Aby se Planner v té době vyrovnal s velmi omezenými paměťovými systémy, použil řídicí strukturu zpětného sledování, takže najednou musela být uložena pouze jedna možná výpočetní cesta. Planner dal vzniknout programovacím jazykům QA-4, Popler, Conniver, QLISP a souběžnému jazyku Ether.

Hayes a Kowalski v Edinburghu se pokusili skloubit logický deklarativní přístup k reprezentaci znalostí s procedurálním přístupem Plannera. Hayes (1973) vyvinul rovníkový jazyk Golux, ve kterém bylo možné získat různé postupy změnou chování věty. Na druhé straně Kowalski vyvinul rozlišení SLD , což je varianta rozlišení SL, a ukázal, jak považuje důsledky za postupy snižování cílů. Kowalski spolupracoval s Colmerauerem v Marseille, který tyto myšlenky rozvinul při návrhu a implementaci programovacího jazyka Prolog .

Sdružení pro logické programování byl založen na podporu logické programování v roce 1986.

Z Prologu vznikly programovací jazyky ALF , Fril , Gödel , Mercury , Oz , Ciao , Visual Prolog , XSB a λProlog , a také řada souběžných logických programovacích jazyků , omezovací logické programovací jazyky a Datalog .

Pojmy

Logika a ovládání

Hlavní článek: Deklarativní programování

Logické programování lze považovat za řízený odpočet. Důležitým konceptem logického programování je rozdělení programů na jejich logickou a řídicí složku. S čistě logickými programovacími jazyky určuje vytvořená řešení pouze logická komponenta. Řídicí komponentu lze měnit tak, aby poskytovala alternativní způsoby provádění logického programu. Tuto představu vystihuje slogan

Algoritmus = logika + ovládání

kde „Logika“ představuje logický program a „Řízení“ představuje různé strategie prokazující věty.

Řešení problému

Ve zjednodušeném, výrokovém případě, kdy logický program a atomový cíl nejvyšší úrovně neobsahují žádné proměnné, zpětné uvažování určuje strom a nebo strom , což představuje vyhledávací prostor pro řešení cíle. Cílem nejvyšší úrovně je kořen stromu. Vzhledem k libovolnému uzlu ve stromu a klauzuli, jejíž hlava odpovídá uzlu, existuje v těle klauzule sada podřízených uzlů odpovídajících dílčím cílům. Tyto podřízené uzly jsou seskupeny pomocí „a“. Alternativní sady dětí odpovídající alternativním způsobům řešení uzlu jsou seskupeny pomocí „nebo“.

K prohledání tohoto prostoru lze použít libovolnou vyhledávací strategii. Prolog používá sekvenční strategii zpětného sledování poslední v první, ve které je zvažována vždy pouze jedna alternativa a jeden dílčí cíl. Jsou možné i jiné vyhledávací strategie, jako je paralelní vyhledávání, inteligentní zpětné sledování nebo hledání nejlepšího prvního k nalezení optimálního řešení.

V obecnějším případě, kdy dílčí cíle sdílejí proměnné, lze použít i jiné strategie, například zvolit dílčí cíl, který je nejvíce instancován nebo který je dostatečně instancován, takže platí pouze jeden postup. Takové strategie se používají například v souběžném logickém programování .

Negace jako selhání

Hlavní článek: Negace jako selhání

Pro většinu praktických aplikací a také pro aplikace, které vyžadují nemonotónní uvažování v umělé inteligenci, je třeba logické programy klauzule Horn rozšířit na normální logické programy s negativními podmínkami. Klauzule v normálním logického programu má tvar:

H :- A1, …, An, not B1, …, not Bn.

a čte se deklarativně jako logická implikace:

H if A1 and … and An and not B1 and … and not Bn.

kde Ha všechny a jsou atomové vzorce. Negace v záporných literálech se běžně označuje jako „ negace jako selhání “, protože ve většině implementací se negativní podmínka projeví tím, že se ukáže, že pozitivní podmínka přestane platit. Například: AiBi not Bi not Bi Bi

canfly(X) :- bird(X), not abnormal(X).
abnormal(X) :- wounded(X).
bird(john).
bird(mary).
wounded(john).

Vzhledem k cíli najít něco, co může létat: 

:- canfly(X).

existují dvě kandidátská řešení, která řeší první dílčí cíl bird(X), a to X = johna X = mary. Druhé dílčí cíl not abnormal(john)prvního kandidátského řešení se nezdaří, protože wounded(john)uspěje, a proto abnormal(john)uspěje. Druhé dílčí cíl not abnormal(mary)druhého kandidátského řešení však uspěje, protože wounded(mary)selže, a proto se abnormal(mary)nezdaří. Proto X = maryje jediným řešením cíle.

Micro-Planner měl konstrukci nazvanou „thnot“, která při použití na výraz vrací hodnotu true, pokud (a pouze pokud) vyhodnocení výrazu selže. V moderních implementacích Prologu obvykle existuje ekvivalentní operátor . Obvykle se píše jako nebo , kde je nějaký cíl (návrh), který má program dokázat. Tento operátor se liší od negace v logice prvního řádu: negace, jako je selhání, když byla proměnná vázána na atom , ale ve všech ostatních případech, včetně případů, kdy je nevázaná , uspěje . Díky tomu je logika Prologu nemonotónní : vždy selže, zatímco může uspět, vazba na podle toho, zda byla původně vázána (všimněte si, že standardní Prolog provádí cíle v pořadí zleva doprava). not(Goal)\+ GoalGoal\+ X == 1X1XX = 1, \+ X == 1\+ X == 1, X = 1X1X

Logický stav negace jako selhání byl nevyřešen, dokud Keith Clark [1978] neukázal, že za určitých přírodních podmínek jde o správnou (a někdy úplnou) implementaci klasické negace s ohledem na dokončení programu. Dokončení zhruba odpovídá množině všech klauzulí programu se stejným predikátem na levé straně, řekněme

H :- Body1.
…
H :- Bodyk.

jako definice predikátu

H iff (Body1 or … or Bodyk)

kde „iff“ znamená „tehdy a jen tehdy“. Zápis dokončení také vyžaduje explicitní použití predikátu rovnosti a zahrnutí sady vhodných axiomů pro rovnost. Implementace negace jako selhání však vyžaduje pouze poloviny definic bez axiomů rovnosti.

Dokončení výše uvedeného programu je například:

canfly(X) iff bird(X), not abnormal(X).
abnormal(X) iff wounded(X).
bird(X) iff X = john or X = mary.
X = X.
not john = mary.
not mary = john.

Pojem dokončení úzce souvisí s McCarthyho sémantikou vymezení pro výchozí uvažování a s předpokladem uzavřeného světa .

Jako alternativa k dokončení sémantiky, negace jako selhání může také být interpretováno epistemicky, jak v stabilní modelových sémantiky z odpovědí set programování . V této interpretaci ne (B i ) doslova znamená, že B i není znám nebo se mu nevěří. Epistemická interpretace má tu výhodu, že ji lze velmi jednoduše kombinovat s klasickou negací, jako v „rozšířeném logickém programování“, a formalizovat takové fráze jako „opak nelze ukázat“, kde „opak“ je klasická negace a „nelze být ukázán “je epistemická interpretace negace jako selhání.

Reprezentace znalostí

Skutečnost, že Hornovým doložkám lze podat procedurální výklad a naopak, že postupy snižování cílů lze chápat jako Hornovy doložky + zpětné uvažování, znamená, že logické programy kombinují deklarativní a procedurální reprezentaci znalostí . Zahrnutí negace jako selhání znamená, že logické programování je druh nemonotonické logiky .

Navzdory své jednoduchosti ve srovnání s klasickou logikou se tato kombinace klaunů Horn a negace jako selhání ukázala jako překvapivě expresivní. Například poskytuje přirozenou reprezentaci zákonů příčiny a následku selského rozumu, formalizovaných jak situačním kalkulem, tak kalkulem událostí . Ukázalo se také, že zcela přirozeně odpovídá poloformálnímu jazyku legislativy. Prakken a Sartor zejména připisují reprezentaci britského zákona o národnosti jako logického programu tím, že „mají obrovský vliv na vývoj výpočetních reprezentací legislativy a ukazují, jak logické programování umožňuje intuitivně přitažlivé reprezentace, které lze přímo nasadit a generovat automatické závěry“. .

Varianty a rozšíření

Prolog

Hlavní článek: Prolog

Programovací jazyk Prolog vyvinul v roce 1972 Alain Colmerauer . Vyplynulo to ze spolupráce mezi Colmerauerem v Marseille a Robertem Kowalskim v Edinburghu. Colmerauer pracoval na porozumění přirozenému jazyku , pomocí logiky reprezentoval sémantiku a používal řešení pro zodpovídání otázek. V létě roku 1971 Colmerauer a Kowalski zjistili, že klauzální formu logiky lze použít k reprezentaci formálních gramatik a že k analýze lze použít prokazovací věty o rozlišení. Poznamenali, že některé dokazovače teorémů, jako hyperrozlišení, se chovají jako analyzátory zdola nahoru a jiné, jako rozlišení SL (1971), se chovají jako analyzátory shora dolů.

Bylo to v následujícím létě roku 1972, kdy Kowalski, opět ve spolupráci s Colmerauerem, vyvinul procedurální interpretaci implikací. Tento duální deklarativní/procedurální výklad se později formalizoval v prologové notaci

H :- B1, …, Bn.

které lze číst (a používat) deklarativně i procesně. Ukázalo se také, že tyto doložky by mohla být omezena na určitých doložek nebo klauzulí Horn , kde H, , ..., jsou všechny atomové přívlastková logické formule, a že SL-rozlišení by mohla být omezena (a generalizované) a bujnou nebo SLD rozlišením . Kowalského procedurální interpretace a LUSH byly popsány ve zprávě z roku 1973, publikované v roce 1974. B1Bn

Colmerauer a Philippe Roussel použili tento duální výklad klauzulí jako základ Prologu, který byl implementován v létě a na podzim roku 1972. První program Prolog, napsaný také v roce 1972 a implementovaný v Marseille, byl francouzský systém odpovědí na otázky . Použití Prologu jako praktického programovacího jazyka dostalo velkou dynamiku vývojem překladače Davida Warrena v Edinburghu v roce 1977. Experimenty prokázaly, že Edinburgh Prolog může konkurovat rychlosti zpracování jiných symbolických programovacích jazyků, jako je Lisp . Edinburgh Prolog se stal de facto standardem a silně ovlivnil definici standardu ISO Prolog.

Abduktivní logické programování

Abduktivní logické programování je rozšířením běžného logického programování, které umožňuje, aby některé predikáty, deklarované jako abdukovatelné predikáty, byly „otevřené“ nebo nedefinované. Klauzule v abduktivním logickém programu má tvar:

H :- B1, …, Bn, A1, …, An.

kde Hje atomový vzorec, který není únosný, všechny jsou literály, jejichž predikáty nejsou únosné, a atomové vzorce, jejichž predikáty jsou únosné. Abdukovatelné predikáty mohou být omezeny omezeními integrity, která mohou mít formu: BiAi

false :- L1, …, Ln.

kde jsou libovolné literály (definované nebo unesitelné a atomové nebo negované). Například: Li

canfly(X) :- bird(X), normal(X).
false :- normal(X), wounded(X).
bird(john).
bird(mary).
wounded(john).

kde je predikát normalúnosný.

Řešení problémů je dosaženo odvozením hypotéz vyjádřených únosnými predikáty jako řešení problémů, které je třeba vyřešit. Těmito problémy mohou být buď pozorování, která je třeba vysvětlit (jako v klasickém abduktivním uvažování ), nebo cíle, které je třeba vyřešit (jako v běžném logickém programování). Hypotéza například normal(mary)vysvětluje pozorování canfly(mary). Stejná hypotéza navíc znamená jediné řešení X = marycíle najít něco, co může létat: 

:- canfly(X).

Abduktivní logické programování bylo použito pro diagnostiku chyb, plánování, zpracování přirozeného jazyka a strojové učení. Bylo také použito k interpretaci negace jako selhání jako forma únosného uvažování.

Metalogické programování

Protože matematická logika má dlouhou tradici rozlišování mezi objektovým jazykem a metajazykem, umožňuje logické programování také programování na úrovni meta . Nejjednodušší metalogický program je takzvaný „ vanilkový “ meta-interpret: 

    solve(true).
    solve((A,B)):- solve(A),solve(B).
    solve(A):- clause(A,B),solve(B).

kde true představuje prázdnou spojku a klauzule (A, B) znamená, že existuje klauzule na úrovni objektu ve tvaru A:- B.

Metalogické programování umožňuje kombinovat reprezentace na úrovni objektů a metaúrovně, jako v přirozeném jazyce. Lze jej také použít k implementaci jakékoli logiky, která je uvedena jako odvozovací pravidla . Metalogic se v logickém programování používá k implementaci metaprogramů, které jako data manipulují s jinými programy, databázemi, znalostními bázemi nebo axiomatickými teoriemi.

Logické programování omezení

Hlavní článek: Omezovací logické programování

Logické programování omezení kombinuje logické programování klauzule Horn s řešením omezení . Rozšiřuje klauzule Horn tím, že umožňuje, aby se některé predikáty, deklarované jako predikáty omezení, vyskytovaly jako literály v těle klauzulí. Program logiky omezení je sada klauzulí formuláře:

H :- C1, …, Cn ◊ B1, …, Bn.

kde Ha všechny jsou atomové vzorce a jsou omezení. Deklarativně jsou takové doložky chápány jako běžné logické implikace: BiCi

H if C1 and … and Cn and B1 and … and Bn.

Avšak zatímco predikáty v hlavách klauzulí jsou definovány programem logiky omezení, predikáty v omezeních jsou předdefinovány nějakou doménou specifickou modelem-teoretickou strukturou nebo teorií.

Procedurálně jsou dílčí cíle, jejichž predikáty jsou definovány programem, řešeny pomocí redukce cílů, jako v běžném logickém programování, ale splnění omezení je kontrolováno na splnitelnost pomocí omezovače vazeb specifického pro doménu, který implementuje sémantiku predikátů omezení. Počáteční problém je vyřešen jeho snížením na uspokojivou konjunkci omezení.

Následující program logiky omezení představuje dočasnou databázi john'shistorie jako učitel: 

teaches(john, hardware, T) :- 1990 ≤ T, T < 1999.
teaches(john, software, T) :- 1999 ≤ T, T < 2005.
teaches(john, logic, T) :- 2005 ≤ T, T ≤ 2012.
rank(john, instructor, T) :- 1990 ≤ T, T < 2010.
rank(john, professor, T) :- 2010 ≤ T, T < 2014.

Tady ≤a <jsou omezovači predikáty, se svými obvyklými určených sémantiky. Následující klauzule cíle dotazuje databázi, aby zjistila, kdy johnoba učili logica byla professor:

:- teaches(john, logic, T), rank(john, professor, T).

Řešení je 2010 ≤ T, T ≤ 2012.

Logické programování omezení bylo použito k řešení problémů v takových oblastech, jako je stavebnictví , strojírenství , ověřování digitálních obvodů , automatické časování , řízení letového provozu a finance. Úzce souvisí s abduktivní logickým programováním .

Souběžné logické programování

Hlavní článek: Souběžné logické programování

Souběžné logické programování integruje koncepty logického programování se souběžným programováním . Jeho vývoj dostal v 80. letech velký impuls volbou pro programovací jazyk systémů japonského projektu páté generace (FGCS) .

Souběžný logický program je sada hlídaných klauzí Horn ve tvaru:

H :- G1, …, Gn | B1, …, Bn.

Spojka se nazývá strážcem klauzule a je operátorem závazku. Deklarativně jsou strážné klauzule Horn chápány jako běžné logické implikace: G1, ... , Gn |

H if G1 and … and Gn and B1 and … and Bn.

Pokud však existuje procedurálně několik klauzulí, jejichž hlavy H odpovídají danému cíli, všechny klauzule se provádějí souběžně a kontroluje se, zda jejich stráže drží. Pokud stráže více než jedné klauzule platí, pak se jedna z klauzulí rozhodne a provedení pokračuje s dílčími cíli zvolené klauzule. Tyto dílčí cíle lze také provádět souběžně. Souběžné logické programování tak implementuje spíše formu „nezáleží na nedeterminismu“, než „nevím o nedeterminismu“. G1, ... , Gn B1, ..., Bn

Následující souběžný logický program například definuje predikát shuffle(Left, Right, Merge) , který lze použít k zamíchání dvou seznamů Lefta Rightjejich kombinaci do jednoho seznamu, Mergekterý zachovává pořadí dvou seznamů Lefta Right: 

shuffle([], [], []).
shuffle(Left, Right, Merge) :-
    Left = [First | Rest] |
    Merge = [First | ShortMerge],
    shuffle(Rest, Right, ShortMerge).
shuffle(Left, Right, Merge) :-
    Right = [First | Rest] |
    Merge = [First | ShortMerge],
    shuffle(Left, Rest, ShortMerge).

Zde []představuje prázdný seznam a [Head | Tail]představuje seznam s prvním prvkem Headnásledovaným seznamem Tail, jako v Prologu. (Všimněte si, že první výskyt | ve druhé a třetí klauzuli je konstruktor seznamu, zatímco druhý výskyt | je operátor závazku.) Program lze použít například k zamíchání seznamů [ace, queen, king]a [1, 4, 2]vyvolání klauzule cíle: 

shuffle([ace, queen, king], [1, 4, 2], Merge).

Program například nedeterministicky vygeneruje jediné řešení Merge = [ace, queen, 1, king, 4, 2].

Souběžné logické programování je pravděpodobně založeno na předávání zpráv, takže podléhá stejné neurčitosti jako jiné souběžné systémy pro předávání zpráv, například Actors (viz Neurčitost v souběžném výpočtu ). Carl Hewitt tvrdil, že souběžné logické programování není založeno na logice v jeho smyslu, že výpočetní kroky nelze logicky odvodit. V souběžném logickém programování je však jakýkoli výsledek ukončujícího výpočtu logickým důsledkem programu a jakýkoli dílčí výsledek částečného výpočtu je logickým důsledkem programu a zbytkového cíle (síť procesů). Neurčitost výpočtů tedy znamená, že nelze odvodit všechny logické důsledky programu.

Souběžné programování logiky omezení

Hlavní článek: Souběžné programování logiky omezení

Souběžné programování logiky omezení kombinuje souběžné programování logiky a programování logiky omezení pomocí omezení pro řízení souběžnosti. Klauzule může obsahovat ochranný prvek, což je sada omezení, která mohou blokovat použitelnost klauzule. Když jsou splněny stráže několika klauzulí, souběžné programování logiky omezení učiní potvrzenou volbu použít pouze jednu.

Indukční logické programování

Hlavní článek: Indukční logické programování

Indukční logické programování se zabývá generalizací pozitivních a negativních příkladů v kontextu znalostí na pozadí: strojového učení logických programů. Nedávná práce v této oblasti, kombinující logické programování, učení a pravděpodobnost, dala vzniknout nové oblasti statistického relačního učení a pravděpodobnostního induktivního logického programování .

Logické programování vyššího řádu

Několik výzkumníků rozšířilo logické programování o programovací funkce vyššího řádu odvozené z logiky vyššího řádu , jako jsou predikátové proměnné. Mezi takové jazyky patří rozšíření Prolog HiLog a λProlog .

Lineární logické programování

Základem logického programování v lineární logice byl návrh logických programovacích jazyků, které jsou podstatně výraznější než jazyky založené na klasické logice. Programy klauzule klaksonu mohou představovat změnu stavu pouze změnou argumentů na predikáty. V lineárním logickém programování lze k podpoře změny stavu použít okolní lineární logiku. Některé rané designy logických programovacích jazyků založené na lineární logice zahrnují LO [Andreoli & Pareschi, 1991], Lolli, ACL a Forum [Miller, 1996]. Fórum poskytuje cílenou interpretaci veškeré lineární logiky.

Objektově orientované logické programování

F-logic rozšiřuje logické programování o objekty a syntaxi rámců.

Logtalk rozšiřuje programovací jazyk Prolog o podporu objektů, protokolů a dalších konceptů OOP. Jako backend kompilátory podporuje většinu standardních systémů Prolog.

Programování transakční logiky

Transakční logika je rozšířením logického programování o logickou teorii aktualizací upravujících stav. Má jak modelově teoretickou sémantiku, tak procedurální. V systému Flora-2 je k dispozici implementace podmnožiny transakční logiky . K dispozici jsou také další prototypy .

Viz také

Citace

Prameny

Obecné úvody

Jiné zdroje

Další čtení

externí odkazy