Logické programování

Programovací paradigmata

Logické programování je v širším významu použití matematické logiky jako prostředku pro programování. Jeho počátky lze vystopovat až k návrhu Johna McCarthyho advice taker (rádce) [1958]. V tomto návrhu slouží logika pro čistě deklarativní reprezentaci jazyka a dokazovač vět (theorem-prover) nebo generátor modelů (model-generator) se používá jako řešitel problémů (problem-solver). Řešení problému se tak dělí mezi programátora (ručí za správnost programu vyjádřené v logické formě) a dokazovač vět nebo generátor modelů (odpovídá za efektivní řešení problému).

Častěji se však logické programování chápe v užším smyslu, kdy se logika používá na deklarativní i procedurální reprezentaci jazyka. Vychází z faktu, že zpětně usuzující dokazovač vět (backwards reasoning theorem-prover) použitý na deklarativní větu ve tvaru implikace:

B1 a … a Bn implies H

zachází s touto implikací jako s cíl redukující (goal-reduction) procedurou.

ukaž/vyřeš H, ukaž/vyřeš B1 a … a Bn.

Programátor neručí pouze za správnost programu, ale i za jeho efektivitu. Často je pro dosažení efektivity nezbytné, aby se programátor seznámil se způsobem, jakým dokazovač vět řeší problém a uměl jej využívat. Tím, že logické programovaní používá program k řízení chování vykonavatele programu (program executor) se podobá tradičnímu imperativnímu programování. Od imperativních programů s pouze procedurální interpretací se však logické programy liší existencí deklarativní logické interpretace, která pomáhá zajistit jejich korektnost. Díky tomu, že jsou tyto programy deklarativní (tedy deklarují, co je vstupem a výstupem, a nezabývají se tím, jak výpočet probíhá), jsou na mnohem vyšší konceptuální úrovni než čistě imperativní programy, a jejich vykonavatelé, kteří jsou vlastně dokazovači vět, operují na konceptuálně vyšší úrovni než běžné překladače a interprety.

Historie

Logické programování v širším smyslu dalo vzniknout mnoha implementacím. Například systémy odpovídající na dotazy (question-answering systems) Fischera Blacka (1964), Jamese Slagla (1965) a Cordella Greena (1969) stvořené v duchu McCarthyho návrhu advice taker. Fosterův a Elcockův Absys (1969) byl pravděpodobně první jazyk explicitně vyvíjený jako výrazový programovací jazyk (assertional programming language).

Počátky logického programování v užším slova smyslu můžeme vystopovat do konce šedesátých a počátku sedmdesátých let, kdy se vedly debaty o deklarativní nebo procedurální reprezentaci znalostí v umělé inteligenci. Obhájci deklarativního přístupu působili především na Stanfordově univerzitě (John McCarth, Bertram Raphael a Cordell Green) a Edinburské univerzitě ( Alane Robinsonem, Patrick J. Hayes a Robert Kowalski). Obhájci procedurální reprezentace se soustředili zejména okolo MIT, pod vedením Marvina Minskyho a Seymoura Paperta.

V roce 1960 Carl Hewitt v MIT vyvinul jazyk Planner. I když byl Planner první jazyk založený na logice v užším chápaní, byl silně ovlivněn procedurálním paradigmatem. Nejvýznamnější implementací Planneru byla jeho podmnožina s názvem Micro-Planner, vytvořená Gerry Sussmanem, Eugene Charniakem a Terry Winogradem. Micro-Planner byl použit k implementaci Winogradova programu pro porozumění přirozenému jazyku (SHRDLU), což byl důležitý mezník té doby. Planner byl vybaven vzorově řízeným (pattern-directed) vyvoláváním procedurálních plánů z výrazů i cílů. Protože systémy dostupné v době vývoje byly limitovány velmi malou pamětí, používal Planner backtraking řídící strukturu a bylo možné ukládat pouze jednu výpočetní cestu. Z Planeru vzešly další programovací jazyky, například QA-4, Popler, Conniver, QLISP a paralelní Ether.

Hayes a Kowalski z Edinburské univerzity se pokusili spojit logicky založený deklarativní přístup reprezentace znalostí s procedurálním přístupem Planneru. Hayes (1973) vyvinul jazyk Golux pro řešení rovnic (equational language), ve kterém je možné získat různé procedury změnou chování dokazovače vět. Kowalski ukázal jak SL-rezoluce zachází s implikacemi jako s cíl redukujícími (goal-reduction) procedurami. Kowalski spolupracoval s Colmerauerem z Marseille, který rozvinul tyto myšlenky v návrhu a implementaci programovacího jazyka Prolog. Z Prologu se vyvinulo mnoho dalších jazyků: ALF, Fril, Gödel, Mercury, Oz, Ciao, Visual Prolog, XSB, a λProlog. Stejně tak i množství paralelních logických programovacích jazyků, logických programovacích jazyků s omezujícími podmínkami a datalogů.

V roce 1997 udělila Asociace logického programování patnácti významným vědcům v oboru logického programování titul Zakladatel logického programování, aby ocenila jejich průkopnickou činnost v oboru. Mezi tyto vědce patří:

Prolog

Související informace naleznete také v článku Prolog (programovací jazyk).

Jazyk Prolog byl vyvinut Alainem Colmerauerem v roce 1972. Vzešel ze spolupráce mezi Colmerauerem z University v Marseille a Robertem Kowalskim z Edinburské university. Colmerauer pracoval na porozumění přirozeného jazyka. Logiku používal pro reprezentaci sémantiky a rezoluci pro získávaní odpovědí na dotazy (question-answering). Během léta 1971, Colmerauer a Kowalski objevili, že klauzální logika může být použita k reprezentaci formální gramatiky a že rezoluční dokazovač vět (resolution theorem prover) může být využit pro parsování. Zjistili, že některé dokazovače vět jako například hyper rezoluce (hyper-resolution) se chovají jako bottom-up parsery a jiné třeba SL rezoluce (1971) se chovají jako top-down parsery.

Následující léto roku 1972 Kowalski opět za spolupráce s Colmerauerem, vytvořil procedurální interpretaci implikace. Tato duálně deklarativní/procedurální interpretace byla později formalizována v notaci Prologu:

H :- B1, …, Bn.

která může být čtena a použita deklarativně i procedurálně. Bylo také jasné, že tyto klauzule mohou být omezeny pouze na definitní klauzule nebo Hornovské klauzule, kde

H, B1, …, Bn

jsou všechno atomické predikáty logické rovnice a SL rezoluce může být zobecněna na LUSH nebo SLD rezoluci. Kowalskeho procedurální interpretace a LUSH byly popsány v jeho poznámkách v roce 1973 a publikovány následujícího roku.

Colmerauer s Philippem Rousselem použili tuto duální interpretaci jako základ pro Prolog, který byl implementován během léta a podzimu roku 1972. První program v Prologu byl rovněž napsán roku 1972 v Marseille a jednalo se o francouzský systém odpovídání na dotazy. Zásadním impulsem pro použití Prologu jako praktického programovacího jazyka bylo vytvoření překladače Davidem Warrenem v Edinburku roku 1977. Experimenty ukázaly, že Edinburský Prolog může výkonem soupeřit s jinými symbolickými programovacími jazyky, jako je Lisp. Edinburský Prolog se stal de facto standardem a silně ovlivnil znění standardu ISO pro Prolog.

Negace jako selhání

Micro-planner obsahoval konstrukci nazvanou "thot", která po aplikaci na výraz vracela "pravda", pouze když vyhodnocování výrazu selhalo. Ekvivalentní operátor je součástí všech moderních implementací prologu a byl nazýván negace jako selhání. Běžně se značí not(p), kde p je atom, jehož proměnně jsou vytvořeny v době, kdy je not(p) zavolán. Zastaralá, ale standardní syntax je \+ p. Literály negace jako selhání se mohou vyskytnout jako podmínka not(Bi) v těle programu klauzulí.

Logický status negace jako selhání zůstával dlouho nevyřešen. Až Keith Clark [1978] dokázal, že za určitých podmínek se jedná o korektní (a někdy úplnou) implementaci klasické negace s ohledem na vyplnitelnost (completion) programu. Vyplnitelnost se zhruba vyhodnocuje vzhledem k množině všech klauzulí, které mají stejný predikát 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 když". Stanovení vyplnitelnosti vyžaduje explicitní použití predikátu rovnosti a inkluzi množiny příslušných axiomů rovnosti. Naštěstí implementace negace jako selhání vyžaduje pouze "if" části definic bez axiomu rovnosti.

Pojem vyplnitelnosti je úzce spjat s McCarthyho vymezovací sémantikou pro výchozí usuzování (circumscription semantics for default reasoning) a hypotézou uzavřeného světa (closed world assumption).

Alternativou k sémantice vyplnitelnosti, může být negace jako selhání interpretována epistemicky jako v modelu stabilní sémantiky v programování množinou dotazů (answer set programming). V této interpretaci not(Bi) znamená doslovně, že Bi není známé nebo je neověřitelné. Epistemická interpretace má tu výhodu, že může být snadno zkombinovaná s klasickou negací, jako v případě "rozšířeného logické programování". Můžeme tak formalizovat tvrzení jako "opak nemůže být prokázán", kde "opak" je klasická negace a "nemůže být prokázán" je epistemická interpretace negace jako selhání.

Řešení problému

Ve zjednodušeném případě, kdy pracujeme s výrokovou logikou a logický program ani hlavní cíl atomický neobsahují proměnné, zpětné usuzování (backward reasoning) určí logický a-nebo strom, který stanovuje prostor řešení cíle.

Hlavní cíl je vrchol stromu. Za předpokladu, že nějaký uzel ve stromu odpovídá hlavě klauzule, pak existuje množina potomků tohoto uzlu, která odpovídá mezi-cílům v těle této klauzuli. Potomci uzlu jsou spojení logickou spojkou a. Alternativní množina potomků odpovídající alternativní cestě řešení uzlu je spojeni pomocí logického nebo.

K prohledání prostoru řešení mohou být použity různé strategie. Prolog využívá sekvenční, LIFO a backtracking strategii, při které najednou zpracovává pouze jeden mezi-cíl a alternativní cestu. K hledaní řešení je možné využívat i jiné strategie jako paralelní vyhledávání, inteligentní backtracking anebo hledaní metodou nejlepší-první (best-first).

V více obecném případě, kdy mezi-cíle sdílejí proměnné, mohou být použity další strategie. Například výběr mezi-cíle, který je nejvíce rozvinut nebo je rozvinut do té míry, že může být použita pouze jedna procedura. Tyto strategie se využívají například v paralelním logickém programování.

Fakt existence několika cest jak vykovávat logický program je vyjádřen rovnicí:

Algoritmus = Logika + Řízení

kde Logika představuje logický program a Řízení různé strategie dokazování vět.

Reprezentace znalostí

Skutečnost, že Hornovské klauzule mohou nabývat procedurální interpretace a zároveň že cíl redukující procedura může být chápána jako Hornovské klauzule spojené se zpětným usuzováním, znamená, že logický program kombinuje deklarativní a procedurální reprezentaci znalostí. Inkluze negace jako selhání znamená, že logické programovaní je druh nemonotonické logiky.

Navzdory své jednoduchosti (v porovnání s klasickou logikou) se kombinace Hornovských klauzulí a negace jako selhání prokázala být překvapivě expresivní. Například bylo ukázáno, že s několika rozšířeními poměrně přirozeně odpovídá poloformálnímu jazyku legislativy. Je to také přirozený jazyk pro vyjadřování zákona příčiny a následků v rámci běžného uvažování, podobně jako v situačním a událostním kalkulu.

Paralelní logické programování

Keith Clark, Steve Gregory, Vijay Saraswat, Udi Shapiro, Kazunori Ueda a další vyvinuli rodinu paralelních systémů zasílání zpráv podobnou Prologu používající unifikaci sdílených proměnných a proudů datových struktur pro zprávy. Snahou bylo postavit tyto systémy na matematické logice a posloužily jako základ pro Japonský projekt počítače páté generace (ICOT).

Logické programování vyšších řádů

Řada výzkumů rozšířila logické programování o vlastnosti programování vyšších řádů odvozených z logiky vyšších řádů, jakými jsou například predikátové proměnné. Mezi tyto jazyky patří rozšíření Prologu HiLog a λProlog.

Lineární logické programování

Základní logické programování ve spojení s lineární logikou vyústilo v návrh logických programovacích jazyků, které mají o poznání silnější vyjadřovací prostředky než jazyky založené na klasické logice. Programy sestavené z Hornovských klauzulí reprezentují pouze změnu stavu způsobenou změnou v argumentech vzhledem k predikátům. V lineárním logickém programování je možné použít ambientní lineární logiku pro podporu změny stavu. Mezi některé z raných návrhů logických programovacích jazyků založených na lineární logice patří: LO [Andreoli & Pareschi, 1991], Lolli [Hodas & Miller, 1994], ACL [Kobayashi & Yonezawa, 1994] a Forum [Miller, 1996]. Forum nabízí interpretaci veškeré lineární logiky zaměřenou na cíl (goal-direct).

Související články

Externí odkazy

Read other articles:

Kilo 2 (Jeddah)LingkunganNegaraArab SaudiProvinsiProvinsi MakkahPemerintahan • Wali kotaHani Abu Ras[1] • Gubernur kotaMish'al Al-SaudKetinggian12 m (39 ft)Zona waktuUTC+3 (AST) • Musim panas (DST)ASTKode pos(5 kode digit dimulai dari 23; e.g. 23434)Kode area telepon+966-12Situs webwww.jeddah.gov.sa/english/index.php Kilo 2 (Jeddah) adalah sebuah permukiman padat penduduk di kota Jeddah di Provinsi Makkah, tepatnya di sebelah barat Arab Sa...

 

BiennoComune di BiennoBiennoLuas • Total30 km2 (10 sq mi)Ketinggian462 m (1,516 ft)Populasi • Total3.510Kode area telepon0364Situs webSitus web resmi Bienno adalah komune yang terletak di distrik Provinsi Brescia, Lombardia, Italia. Kota Bienno memiliki luas sebesar 30 km². Bienno memiliki penduduk sebesar 3.510 jiwa. Pranala luar www.comune.brescia.it lbsKomune di Provinsi Brescia, LombardiaAcquafredda • Adro • Agnosine • Alfianello •...

 

Head of state and elective constitutional monarch of Malaysia Yang di-Pertuan Agong and Agong redirect here. For the gong, see Agung. For other uses, see Agung (disambiguation). Supreme Head of the FederationYang di-Pertuan Agongيڠ دڤرتوان اݢوڠ‎Royal coat of armsRoyal StandardIncumbentSultan Ibrahimsince 31 January 2024StyleHis MajestyTypeConstitutional elective federal monarchyResidenceIstana Negara (official)Istana Melawati (secondary)AppointerConference of RulersTer...

Artikel bertopik bandar udara ini perlu dikembangkan agar dapat memenuhi kriteria sebagai entri Wikipedia.Bantulah untuk mengembangkan artikel ini. Jika tidak dikembangkan, artikel ini akan dihapus. Artikel ini tidak memiliki referensi atau sumber tepercaya sehingga isinya tidak bisa dipastikan. Tolong bantu perbaiki artikel ini dengan menambahkan referensi yang layak. Tulisan tanpa sumber dapat dipertanyakan dan dihapus sewaktu-waktu.Cari sumber: Bandar Udara Umbu Mehang Kunda ...

 

Anbanavan Asaradhavan AdangadhavanPoster filmSutradaraAdhik RavichandranProduserS. Michael RayappanDitulis olehAdhik RavichandranPemeranSilambarasanTamannaahShriya SaranPenata musikYuvan Shankar RajaSinematograferKrishnan VasantPenyuntingRubenPerusahaanproduksiGlobal InfotainmentTanggal rilis 23 Juni 2017 (2017-06-23)[1] Durasi160 menit[2]NegaraIndiaBahasaTamil Anbanavan Asaradhavan Adangadhavan, yang juga dikenal sebagai AAA, adalah sebuah film komedi berbahasa Tam...

 

American state election 2014 Michigan gubernatorial election ← 2010 November 4, 2014 2018 → Turnout41.6% 1.3 [1]   Nominee Rick Snyder Mark Schauer Party Republican Democratic Running mate Brian Calley Lisa Brown Popular vote 1,605,034 1,476,904 Percentage 50.9% 46.9% County results Municipality resultsSnyder:      40–50%      50–60%      60–70%     ...

Kyai Haji Imam ZarkasyiLahir21 Maret 1910Gontor, Mlarak, PonorogoMeninggal30 April 1985Madiun, IndonesiaDikenal atasTrimuti Pendiri Pondok Modern Darussalam Gontor PonorogoPenggantiKH Shoiman Lukmanul Hakim Dr. KH Abdullah Syukri Zarkasyi, M.A KH Hasan Abdullah Sahal Drs. KH Imam Badri KH Syamsul Hadi Abdan, S.Ag Prof. Dr. KH. Amal Fathullah Zarkasyi, M.A Drs. KH. M. Akrim Mariyat, Dipl.A.EdAnakDr. KH Abdullah Syukri Zarkasyi, LC., M.A Hj. Siti Khuriyyah Subakir Hj. Dra. Siti Rosyidah Prof. ...

 

Railway station in Kerala, India This article is about the railway station. For the border village, see Walayar. This article needs additional citations for verification. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed.Find sources: Walayar railway station – news · newspapers · books · scholar · JSTOR (May 2018) (Learn how and when to remove this template message) WalayarRegiona...

 

Algerian cyclist Azzedine LagabPersonal informationFull nameAzzedine LagabBorn (1986-09-18) 18 September 1986 (age 37)Algiers, AlgeriaHeight1.75 m (5 ft 9 in)Weight63 kg (139 lb)Team informationCurrent teamMouloudia Club AlgerDisciplineRoadRoleRiderAmateur teams2016Groupement Sportif des Pétroliers d'Algérie2017Naturablue2022–Mouloudia Club Alger Professional teams2009Doha Team2011–2015Groupement Sportif Pétrolier Algérie2018Groupement Sportif d...

Questa voce sull'argomento centri abitati del Michigan è solo un abbozzo. Contribuisci a migliorarla secondo le convenzioni di Wikipedia. Segui i suggerimenti del progetto di riferimento. Lincoln ParkcityLocalizzazioneStato Stati Uniti Stato federato Michigan ConteaWayne AmministrazioneSindacoPatricia Diaz Krause TerritorioCoordinate42°14′37″N 83°10′51″W / 42.243611°N 83.180833°W42.243611; -83.180833 (Lincoln Park)Coordinate: 42°14′37″N 83°...

 

Marble sculpture Daniel WebsterArtistCarl Conrads (after Thomas Ball)MediumMarble sculptureSubjectDaniel WebsterLocationWashington, D.C., United States Daniel Webster is a marble sculpture depicting the American politician of the same name by Carl Conrads (after Thomas Ball), installed in the United States Capitol's National Statuary Hall, in Washington, D.C., as part of the National Statuary Hall Collection. The state was donated by the U.S. state of New Hampshire in 1894.[1] See als...

 

† Палеопропитеки Научная классификация Домен:ЭукариотыЦарство:ЖивотныеПодцарство:ЭуметазоиБез ранга:Двусторонне-симметричныеБез ранга:ВторичноротыеТип:ХордовыеПодтип:ПозвоночныеИнфратип:ЧелюстноротыеНадкласс:ЧетвероногиеКлада:АмниотыКлада:СинапсидыКласс:�...

此條目可参照英語維基百科相應條目来扩充。 (2021年5月6日)若您熟悉来源语言和主题,请协助参考外语维基百科扩充条目。请勿直接提交机械翻译,也不要翻译不可靠、低品质内容。依版权协议,译文需在编辑摘要注明来源,或于讨论页顶部标记{{Translated page}}标签。 约翰斯顿环礁Kalama Atoll 美國本土外小島嶼 Johnston Atoll 旗幟颂歌:《星條旗》The Star-Spangled Banner約翰斯頓環礁�...

 

此條目可参照英語維基百科相應條目来扩充。 (2021年5月6日)若您熟悉来源语言和主题,请协助参考外语维基百科扩充条目。请勿直接提交机械翻译,也不要翻译不可靠、低品质内容。依版权协议,译文需在编辑摘要注明来源,或于讨论页顶部标记{{Translated page}}标签。 约翰斯顿环礁Kalama Atoll 美國本土外小島嶼 Johnston Atoll 旗幟颂歌:《星條旗》The Star-Spangled Banner約翰斯頓環礁�...

 

本條目存在以下問題,請協助改善本條目或在討論頁針對議題發表看法。 此條目需要擴充。 (2013年1月1日)请協助改善这篇條目,更進一步的信息可能會在討論頁或扩充请求中找到。请在擴充條目後將此模板移除。 此條目需要补充更多来源。 (2013年1月1日)请协助補充多方面可靠来源以改善这篇条目,无法查证的内容可能會因為异议提出而被移除。致使用者:请搜索一下条目的...

这是马来族人名,“尤索夫”是父名,不是姓氏,提及此人时应以其自身的名“法迪拉”为主。 尊敬的拿督斯里哈芝法迪拉·尤索夫Fadillah bin Haji YusofSSAP DGSM PGBK 国会议员 副首相 第14任马来西亚副首相现任就任日期2022年12月3日与阿末扎希同时在任君主最高元首苏丹阿都拉陛下最高元首苏丹依布拉欣·依斯迈陛下首相安华·依布拉欣前任依斯迈沙比里 马来西亚能源转型与�...

 

Locomotive wheel arrangement For usage in video production, see Chroma subsampling. The Midland Railway 115 Class 4-2-2 Under the Whyte notation for the classification of steam locomotives, 4-2-2 represents the wheel arrangement of four leading wheels on two axles, two powered driving wheels on one axle, and two trailing wheels on one axle. Other equivalent classifications are: UIC classification: 2A1 French classification: 211 Turkish classification: 14 Swiss classification: 1/4 Like other s...

 

Changes in musical form during the early 20th Century This article needs more complete citations for verification. Please help add missing citation information so that sources are clearly identifiable. (March 2024) (Learn how and when to remove this message) A caricature of the infamous Scandal Concert, conducted by Arnold Schoenberg on 31 March 1913. Major eras ofWestern classical music Early music Medieval c. 500–1400 Transition to Renaissance Renaissance c. 1400–1600 Transi...

الدوري التشيكوسلوفاكي 1987–88 تفاصيل الموسم الدوري التشيكوسلوفاكي  [لغات أخرى]‏  النسخة 81  البلد تشيكوسلوفاكيا  المنظم اتحاد جمهورية التشيك لكرة القدم  البطل سبارتا براغ  مباريات ملعوبة 240   عدد المشاركين 16   الدوري التشيكوسلوفاكي 1986–87  الدوري ا�...

 

المهدي بن عطية المهدي بن عطية مع المغرب في كأس العالم 2018. معلومات شخصية الاسم الكامل المهدي أمين بن عطية المتقي[1] الميلاد 17 أبريل 1987 (العمر 37 سنة)[2]كوركورون،  فرنسا الطول 1.90 م (6 قدم 3 بوصة)[2] مركز اللعب قلب دفاع الجنسية المغرب فرنسا  معلومات النادي ال...