www.wikidata.uk-ua.nina.az

Рерайтинг математика У Вікіпедії є статті про інші значення цього терміна Рерайтинг медіа У математиці комп ютерній науц

Рерайтинг (математика)

У Вікіпедії є статті про інші значення цього терміна: Рерайтинг (медіа).

У математиці, комп'ютерній науці та в логіці термін рерайтинг (англ. rewriting) означає широкий діапазон способів (потенційно не детермінованих) заміни елементів формули таким чином, що зміст не міняється.

У самому базовому вигляді системи рерайтинга складаються з набору об'єктів, плюс відносин про те, як перетворити ці об'єкти.

Рерайтинг може бути недетермінованим. Одне правило рерайтинга терму може застосовуватися багатьма різними способами до цього терму, або може бути застосовано більше одного правила. Тоді системи рерайтинга не забезпечують алгоритм зміни одного терму на інший, але забезпечують набір можливих правил програми. Проте у поєднанні з відповідним алгоритмом системи рерайтинга можуть розглядатися як комп'ютерні програми, на рерайтингу термів засновано декілька систем доведення теорем та декларативних мов програмування.

Інтуїтивні приклади Редагувати

Логіка Редагувати

У логіці, процедура одержання формули кон'юнктивної нормальної форми (КНФ) може бути зручно написана за допомогою системи рерайтинга. Правила такої системи будуть:

де символ () вказує на те, що зміст лівої частини може бути поданий як рерайтинг у правій частині.

Лінгвістика Редагувати

У лінгвістиці правила рерайтинга, які також називаються правилами фразової структури, використовуються в деяких системах генеративної граматики, як засіб генерування граматично правильних речень мови. Таке правило зазвичай приймає форму A → X, де A є міткою синтаксичної категорії, наприклад, іменником або реченням, а X є послідовністю таких міток або морфем, що виражає той факт, що A може бути замінений на X при генеруванні складової структури речення. Наприклад, правило S → NP VP означає, що пропозиція може складатися з іменника, що супроводжується дієсловом; подальші правила вказують, з яких субкомпонентів можуть складатися іменник та дієслово, і так далі.

Типи систем рерайтинга Редагувати

Абстрактні системи рерайтинга Редагувати

З наведених вище прикладів зрозуміло, що ми можемо думати про переписування систем абстрактно. Потрібно вказати набір об'єктів та правила, які можуть бути застосовані для їх перетворення. Найбільш загальна (однозначна) установка цього поняття називається абстрактною системою скорочення (англ. ARS), хоча останнім часом автори використовують абстрактну систему рерайтинга.

ARS — це просто набір A, елементи якого називаються об'єктами та разом з бінарним відношенням на A, традиційно позначаються →, і називаються відношенням зменшення, відношенням рерайтинга або просто зменшенням.

Приклад. Припустимо, що набір об'єктів T = {a, b, c} і бінарне співвідношення задано правилами a → b, b → a, a → c, і b → c. Зауважте, що ці правила можуть бути застосовані як до a, так і до b, щоб отримати терм c. Така властивість явно важлива. Зауважте також, що c є, в певному сенсі, «найпростішим» термом у системі, оскільки нічого не може бути застосовано до c, щоб перетворити його далі. Цей приклад веде нас до визначення деяких важливих понять у загальному налаштуванні ARS.

Рядкові системи рерайтинга Редагувати

Рядкова система рерайтинга (англ. SRS), також відома як система semi-Thue, використовує вільну моноїдну структуру рядків (слів) над алфавітом, щоб розширити відношення рерайтинга  для всіх рядків у алфавіті, що містять ліву і відповідно праву сторону деяких правил як підрядка. Формально semi-Thue системи це пара , де  — (найчастіше кінцевий) алфавіт, а це бінарне відношення між деякими (фіксованими) строками в алфавіті, що називаються правилами рерайтинга. Однокрокове відношення рерайтинга відносини викликаної  на  визначається так: для будь-яких строк  якщо і тільки якщо є такі, що , , і . Так як  є відношенням на , пара  підходить до визначення абстрактної системи рерайтинга. Очевидно, що  є підмножиною з . Якщо відношення  є симетричним, тоді система називається системою Thue.

У SRS, відношення скорочення сумісне з моноїдною операцією, що означає, що з витікає для усіх рядків . Аналогічним чином, рефлексивне транзитивне симетричне замикання , позначене , є конгруентність, тобто вона є відношенням еквівалентності (за визначенням), і також сумісна з конкатенацією рядків. Відношення називається конгруентністю Thue що породжується з . У системі Thue, тобто якщо іє симетричним, переписане відношення збігається з конгруентністю Thue .

Поняття системи semi-Thue по суті збігається з представленням моноїда.Так як це конгруентність, ми можемо визначити фактор моноїд вільного моноїда за допомогою конгруентністі Thue звичайним чином. Якщо моноїд ізоморфний з , то система semi-Thue називається моноїдним представленням .

Ми відразу отримуємо деякі дуже корисні зв'язки з іншими областями алгебри. Наприклад, алфавіт {a, b} з правилами { ab → ε, ba → ε }, де ε це порожній рядок, є представленням вільної групи на одному генераторі. Якщо замість цих правил є лише { ab → ε }, то ми отримуємо уявлення про біциклічний моноїд. Таким чином, системи Thue є природною основою для вирішення проблеми слів для моноїдів та груп. По суті, кожен моноїд має представлення форми , тобто він завжди може бути представлен системою semi-Thue, можливо, над нескінченним алфавітом.

Проблема слів для системи semi-Thue в цілому нерозв'язна; цей результат іноді називають теоремою Пост-Маркова.

Системи рерайтингу термів Редагувати

Система рерайтингу термів (TRS) — це система рерайтингу, де об'єктами є терми або вирази з вкладеними підвиразами. Наприклад, система, показана у розділі Логіка вище, є системою рерайтингу термів. Умови в цій системі складаються з бінарних операторів і і універсального оператора . Також у правилах є змінні, кожна з яких представляє будь-який можливий терм (хоча одна змінна завжди представляє один і той же терм в одному правилі).

На відміну від рядкової системи рерайтингу, об'єктами якої є плоскі послідовності символів, об'єкти, на яких працює система переписування, тобто терми, утворюють алгебру термів. Терм можна візуалізувати як дерево символів, набір прийнятих символів фіксується даним підписом.

Системи рерайтинга слідів Редагувати

Теорія слідів дає змогу обговорювати багатопроцесорність формальними термінами, наприклад, через моноїд сліду та моноїд історії. Рерайтинг можна виконувати і в системах слідів.

Філософія Редагувати

Системи рерайтинга можуть розглядатися як програми, які виводять кінцеві ефекти зі списку причинно-наслідкових зв'язків. Таким чином, системи рерайтинга можуть розглядатись як системи автоматичного доведення причинності.

Див. також Редагувати

  • Критична пара (логіка)
  • Алгоритм завершення Knuth-Bendix
  • L-системи вказують на перезапис, який виконується паралельно.
  • Прозорість посилань в галузі інформатики
  • Регульований рерайтинг
  • Rho calculus

Подальше читання Редагувати

  • Marc Bezem, Jan Willem Klop, Roel de Vrijer ("Terese"), Term Rewriting Systems ("TeReSe"), Cambridge University Press, 2003, ISBN 0-521-39115-6.
  • Nachum Dershowitz and Jean-Pierre Jouannaud "Rewrite Systems", Chapter 6 in Jan van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics., Elsevier and MIT Press, 1990, ISBN 0-444-88074-7, pp. 243–320.
  • Nachum Dershowitz and David Plaisted. "Rewriting", Chapter 9 in John Alan Robinson and Andrei Voronkov (Eds.), Handbook of Automated Reasoning, Volume 1.
  • Gérard Huet et Derek Oppen, Equations and Rewrite Rules, A Survey (1980) Stanford Verification Group, Report N° 15 Computer Science Department Report N° STAN-CS-80-785
  • Jan Willem Klop. "Term Rewriting Systems", Chapter 1 in Samson Abramsky, Dov M. Gabbay and Tom Maibaum (Eds.), Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures.
  • David Plaisted. "Equational reasoning and term rewriting systems", in Dov M. Gabbay, C. J. Hogger and John Alan Robinson (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 1.
  • Jürgen Avenhaus and Klaus Madlener. "Term rewriting and equational reasoning". In Ranan B. Banerji (Ed.), Formal Techniques in Artificial Intelligence: A Sourcebook, Elsevier (1990).
  • Ronald V. Book and Friedrich Otto, String-Rewriting Systems, Springer (1993).
  • Benjamin Benninghofen, Susanne Kemmerich and Michael M. Richter, Systems of Reductions. LNCS 277, Springer-Verlag (1987).
  • Martin Davis, Ron Sigal, Elaine J. Weyuker, (1994) Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science – 2nd edition, Academic Press, ISBN 0-12-206382-1.

Примітки Редагувати

  1. Hsiang, Jieh, et al. "The term rewriting approach to automated theorem proving." The Journal of Logic Programming 14.1-2 (1992): 71-99.
  2. Frühwirth, Thom. "Theory and practice of constraint handling rules." The Journal of Logic Programming 37.1 (1998): 95-138.
  3. Clavel, Manuel, et al. "Maude: Specification and programming in rewriting logic." Theoretical Computer Science 285.2 (2002): 187-243.
  4. Kim Marriott; Peter J. Stuckey (1998). Programming with Constraints: An Introduction. MIT Press. с. 436–. ISBN 978-0-262-13341-8. 
  5. ↑ Bezem et al., p. 7,
  6. Book and Otto, p. 10
  7. Baader and Nipkow, pp. 8-9
  8. Martin Davis et al. 1994, p. 178


Це незавершена стаття з логіки.
Ви можете допомогти проєкту, виправивши або дописавши її.


Це незавершена стаття з інформатики.
Ви можете допомогти проєкту, виправивши або дописавши її.
Це незавершена стаття з математики.
Ви можете допомогти проєкту, виправивши або дописавши її.
Ця стаття потребує додаткових посилань на джерела для поліпшення її перевірності. Будь ласка, допоможіть удосконалити цю статтю, додавши посилання на надійні (авторитетні) джерела. Зверніться на сторінку обговорення за поясненнями та допоможіть виправити недоліки.
Матеріал без джерел може бути піддано сумніву та вилучено. (грудень 2017)
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри
Дата публікації:
U Vikipediyi ye statti pro inshi znachennya cogo termina Rerajting media U matematici komp yuternij nauci ta v logici termin rerajting angl rewriting oznachaye shirokij diapazon sposobiv potencijno ne determinovanih zamini elementiv formuli takim chinom sho zmist ne minyayetsya U samomu bazovomu viglyadi sistemi rerajtinga skladayutsya z naboru ob yektiv plyus vidnosin pro te yak peretvoriti ci ob yekti Rerajting mozhe buti nedeterminovanim Odne pravilo rerajtinga termu mozhe zastosovuvatisya bagatma riznimi sposobami do cogo termu abo mozhe buti zastosovano bilshe odnogo pravila Todi sistemi rerajtinga ne zabezpechuyut algoritm zmini odnogo termu na inshij ale zabezpechuyut nabir mozhlivih pravil programi Prote u poyednanni z vidpovidnim algoritmom sistemi rerajtinga mozhut rozglyadatisya yak komp yuterni programi na rerajtingu termiv zasnovano dekilka sistem dovedennya teorem 1 ta deklarativnih mov programuvannya 2 3 Zmist 1 Intuyitivni prikladi 1 1 Logika 1 2 Lingvistika 2 Tipi sistem rerajtinga 2 1 Abstraktni sistemi rerajtinga 2 2 Ryadkovi sistemi rerajtinga 2 3 Sistemi rerajtingu termiv 2 4 Sistemi rerajtinga slidiv 3 Filosofiya 4 Div takozh 5 Podalshe chitannya 6 PrimitkiIntuyitivni prikladi RedaguvatiLogika Redaguvati U logici procedura oderzhannya formuli kon yunktivnoyi normalnoyi formi KNF mozhe buti zruchno napisana za dopomogoyu sistemi rerajtinga 4 Pravila takoyi sistemi budut A A displaystyle neg neg A to A nbsp Podvijne zaperechennya A B A B displaystyle neg A land B to neg A lor neg B nbsp Zakon de Morgana A B A B displaystyle neg A lor B to neg A land neg B nbsp A B C A C B C displaystyle A land B lor C to A lor C land B lor C nbsp Distributivnist A B C A B A C displaystyle A lor B land C to A lor B land A lor C nbsp de simvol displaystyle to nbsp vkazuye na te sho zmist livoyi chastini mozhe buti podanij yak rerajting u pravij chastini Lingvistika Redaguvati U lingvistici pravila rerajtinga yaki takozh nazivayutsya pravilami frazovoyi strukturi vikoristovuyutsya v deyakih sistemah generativnoyi gramatiki yak zasib generuvannya gramatichno pravilnih rechen movi Take pravilo zazvichaj prijmaye formu A X de A ye mitkoyu sintaksichnoyi kategoriyi napriklad imennikom abo rechennyam a X ye poslidovnistyu takih mitok abo morfem sho virazhaye toj fakt sho A mozhe buti zaminenij na X pri generuvanni skladovoyi strukturi rechennya Napriklad pravilo S NP VP oznachaye sho propoziciya mozhe skladatisya z imennika sho suprovodzhuyetsya diyeslovom podalshi pravila vkazuyut z yakih subkomponentiv mozhut skladatisya imennik ta diyeslovo i tak dali Tipi sistem rerajtinga RedaguvatiAbstraktni sistemi rerajtinga Redaguvati Z navedenih vishe prikladiv zrozumilo sho mi mozhemo dumati pro perepisuvannya sistem abstraktno Potribno vkazati nabir ob yektiv ta pravila yaki mozhut buti zastosovani dlya yih peretvorennya Najbilsh zagalna odnoznachna ustanovka cogo ponyattya nazivayetsya abstraktnoyu sistemoyu skorochennya angl ARS hocha ostannim chasom avtori vikoristovuyut abstraktnu sistemu rerajtinga 5 ARS ce prosto nabir A elementi yakogo nazivayutsya ob yektami ta razom z binarnim vidnoshennyam na A tradicijno poznachayutsya i nazivayutsya vidnoshennyam zmenshennya vidnoshennyam rerajtinga 5 abo prosto zmenshennyam 6 Priklad Pripustimo sho nabir ob yektiv T a b c i binarne spivvidnoshennya zadano pravilami a b b a a c i b c Zauvazhte sho ci pravila mozhut buti zastosovani yak do a tak i do b shob otrimati term c Taka vlastivist yavno vazhliva Zauvazhte takozh sho c ye v pevnomu sensi najprostishim termom u sistemi oskilki nichogo ne mozhe buti zastosovano do c shob peretvoriti jogo dali Cej priklad vede nas do viznachennya deyakih vazhlivih ponyat u zagalnomu nalashtuvanni ARS 7 displaystyle stackrel rightarrow nbsp ce tranzitivne zamikannya displaystyle rightarrow cup nbsp de ye vidnoshennya rivnosti tobto displaystyle stackrel rightarrow nbsp ye najmenshim peredporyadkom refleksivnim i tranzitivnim vidnoshennyam sho mistit displaystyle rightarrow nbsp Jogo takozh nazivayut refleksivnim tranzitivnim zamikannyam displaystyle rightarrow nbsp displaystyle leftrightarrow nbsp ce 1 displaystyle rightarrow cup xrightarrow 1 nbsp sho ye ob yednannyam spivvidnoshennya displaystyle rightarrow nbsp z jogo zvorotnim spivvidnoshennyam takozh vidomim yak simetrichne zamikannya displaystyle rightarrow nbsp displaystyle stackrel leftrightarrow nbsp ce tranzitivne zamikannya displaystyle leftrightarrow cup nbsp de displaystyle stackrel leftrightarrow nbsp ye najmenshim vidnoshennyam ekvivalentnosti sho mistit displaystyle rightarrow nbsp Vin takozh vidomij yak refleksivne tranzitivne simetrichne zamikannya displaystyle rightarrow nbsp Ryadkovi sistemi rerajtinga Redaguvati Ryadkova sistema rerajtinga angl SRS takozh vidoma yak sistema semi Thue vikoristovuye vilnu monoyidnu strukturu ryadkiv sliv nad alfavitom shob rozshiriti vidnoshennya rerajtinga R displaystyle R nbsp dlya vsih ryadkiv u alfaviti sho mistyat livu i vidpovidno pravu storonu deyakih pravil yak pidryadka Formalno semi Thue sistemi ce para S R displaystyle Sigma R nbsp de S displaystyle Sigma nbsp najchastishe kincevij alfavit a R displaystyle R nbsp ce binarne vidnoshennya mizh deyakimi fiksovanimi strokami v alfaviti sho nazivayutsya pravilami rerajtinga Odnokrokove vidnoshennya rerajtinga vidnosini R displaystyle xrightarrow R nbsp viklikanoyi R displaystyle R nbsp na S displaystyle Sigma nbsp viznachayetsya tak dlya bud yakih strok s t S displaystyle s t in Sigma nbsp s R t displaystyle s xrightarrow R t nbsp yaksho i tilki yaksho ye x y u v S displaystyle x y u v in Sigma nbsp taki sho s x u y displaystyle s xuy nbsp t x v y displaystyle t xvy nbsp i u R v displaystyle uRv nbsp Tak yak R displaystyle xrightarrow R nbsp ye vidnoshennyam na S displaystyle Sigma nbsp para S R displaystyle Sigma xrightarrow R nbsp pidhodit do viznachennya abstraktnoyi sistemi rerajtinga Ochevidno sho R displaystyle R nbsp ye pidmnozhinoyu z R displaystyle xrightarrow R nbsp Yaksho vidnoshennya R displaystyle R nbsp ye simetrichnim todi sistema nazivayetsya sistemoyu Thue U SRS vidnoshennya skorochennya R displaystyle xrightarrow R nbsp sumisne z monoyidnoyu operaciyeyu sho oznachaye sho z x R y displaystyle x xrightarrow R y nbsp vitikaye u x v R u y v displaystyle uxv xrightarrow R uyv nbsp dlya usih ryadkiv x y u v S displaystyle x y u v in Sigma nbsp Analogichnim chinom refleksivne tranzitivne simetrichne zamikannya R displaystyle xrightarrow R nbsp poznachene R displaystyle overset underset R leftrightarrow nbsp ye kongruentnist tobto vona ye vidnoshennyam ekvivalentnosti za viznachennyam i takozh sumisna z konkatenaciyeyu ryadkiv Vidnoshennya R displaystyle overset underset R leftrightarrow nbsp nazivayetsya kongruentnistyu Thue sho porodzhuyetsya z R displaystyle R nbsp U sistemi Thue tobto yaksho R displaystyle R nbsp iye simetrichnim perepisane vidnoshennya R displaystyle xrightarrow R nbsp zbigayetsya z kongruentnistyu Thue R displaystyle overset underset R leftrightarrow nbsp Ponyattya sistemi semi Thue po suti zbigayetsya z predstavlennyam monoyida Tak yak R displaystyle overset underset R leftrightarrow nbsp ce kongruentnist mi mozhemo viznachiti faktor monoyid M R S R displaystyle mathcal M R Sigma overset underset R leftrightarrow nbsp vilnogo monoyida S displaystyle Sigma nbsp za dopomogoyu kongruentnisti Thue zvichajnim chinom Yaksho monoyid M displaystyle mathcal M nbsp izomorfnij z M R displaystyle mathcal M R nbsp to sistema semi Thue S R displaystyle Sigma R nbsp nazivayetsya monoyidnim predstavlennyam M displaystyle mathcal M nbsp Mi vidrazu otrimuyemo deyaki duzhe korisni zv yazki z inshimi oblastyami algebri Napriklad alfavit a b z pravilami ab e ba e de e ce porozhnij ryadok ye predstavlennyam vilnoyi grupi na odnomu generatori Yaksho zamist cih pravil ye lishe ab e to mi otrimuyemo uyavlennya pro biciklichnij monoyid Takim chinom sistemi Thue ye prirodnoyu osnovoyu dlya virishennya problemi sliv dlya monoyidiv ta grup Po suti kozhen monoyid maye predstavlennya formi S R displaystyle Sigma R nbsp tobto vin zavzhdi mozhe buti predstavlen sistemoyu semi Thue mozhlivo nad neskinchennim alfavitom Problema sliv dlya sistemi semi Thue v cilomu nerozv yazna cej rezultat inodi nazivayut teoremoyu Post Markova 8 Sistemi rerajtingu termiv Redaguvati Sistema rerajtingu termiv TRS ce sistema rerajtingu de ob yektami ye termi abo virazi z vkladenimi pidvirazami Napriklad sistema pokazana u rozdili Logika vishe ye sistemoyu rerajtingu termiv Umovi v cij sistemi skladayutsya z binarnih operatoriv displaystyle vee nbsp i displaystyle wedge nbsp i universalnogo operatora displaystyle neg nbsp Takozh u pravilah ye zminni kozhna z yakih predstavlyaye bud yakij mozhlivij term hocha odna zminna zavzhdi predstavlyaye odin i toj zhe term v odnomu pravili Na vidminu vid ryadkovoyi sistemi rerajtingu ob yektami yakoyi ye ploski poslidovnosti simvoliv ob yekti na yakih pracyuye sistema perepisuvannya tobto termi utvoryuyut algebru termiv Term mozhna vizualizuvati yak derevo simvoliv nabir prijnyatih simvoliv fiksuyetsya danim pidpisom Sistemi rerajtinga slidiv Redaguvati Teoriya slidiv daye zmogu obgovoryuvati bagatoprocesornist formalnimi terminami napriklad cherez monoyid slidu ta monoyid istoriyi Rerajting mozhna vikonuvati i v sistemah slidiv Filosofiya RedaguvatiSistemi rerajtinga mozhut rozglyadatisya yak programi yaki vivodyat kincevi efekti zi spisku prichinno naslidkovih zv yazkiv Takim chinom sistemi rerajtinga mozhut rozglyadatis yak sistemi avtomatichnogo dovedennya prichinnosti Div takozh RedaguvatiKritichna para logika Algoritm zavershennya Knuth Bendix L sistemi vkazuyut na perezapis yakij vikonuyetsya paralelno Prozorist posilan v galuzi informatiki Regulovanij rerajting Rho calculusPodalshe chitannya RedaguvatiMarc Bezem Jan Willem Klop Roel de Vrijer Terese Term Rewriting Systems TeReSe Cambridge University Press 2003 ISBN 0 521 39115 6 Nachum Dershowitz and Jean Pierre Jouannaud Rewrite Systems Chapter 6 in Jan van Leeuwen Ed Handbook of Theoretical Computer Science Volume B Formal Models and Semantics Elsevier and MIT Press 1990 ISBN 0 444 88074 7 pp 243 320 Nachum Dershowitz and David Plaisted Rewriting Chapter 9 in John Alan Robinson and Andrei Voronkov Eds Handbook of Automated Reasoning Volume 1 Gerard Huet et Derek Oppen Equations and Rewrite Rules A Survey 1980 Stanford Verification Group Report N 15 Computer Science Department Report N STAN CS 80 785 Jan Willem Klop Term Rewriting Systems Chapter 1 in Samson Abramsky Dov M Gabbay and Tom Maibaum Eds Handbook of Logic in Computer Science Volume 2 Background Computational Structures David Plaisted Equational reasoning and term rewriting systems in Dov M Gabbay C J Hogger and John Alan Robinson Eds Handbook of Logic in Artificial Intelligence and Logic Programming Volume 1 Jurgen Avenhaus and Klaus Madlener Term rewriting and equational reasoning In Ranan B Banerji Ed Formal Techniques in Artificial Intelligence A Sourcebook Elsevier 1990 Rerajting ryadkivRonald V Book and Friedrich Otto String Rewriting Systems Springer 1993 Benjamin Benninghofen Susanne Kemmerich and Michael M Richter Systems of Reductions LNCS 277 Springer Verlag 1987 InshiMartin Davis Ron Sigal Elaine J Weyuker 1994 Computability Complexity and Languages Fundamentals of Theoretical Computer Science 2nd edition Academic Press ISBN 0 12 206382 1 Primitki Redaguvati Hsiang Jieh et al The term rewriting approach to automated theorem proving The Journal of Logic Programming 14 1 2 1992 71 99 Fruhwirth Thom Theory and practice of constraint handling rules The Journal of Logic Programming 37 1 1998 95 138 Clavel Manuel et al Maude Specification and programming in rewriting logic Theoretical Computer Science 285 2 2002 187 243 Kim Marriott Peter J Stuckey 1998 Programming with Constraints An Introduction MIT Press s 436 ISBN 978 0 262 13341 8 a b Bezem et al p 7 Book and Otto p 10 Baader and Nipkow pp 8 9 Martin Davis et al 1994 p 178 nbsp Ce nezavershena stattya z logiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi nbsp Ce nezavershena stattya z informatiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi nbsp Ce nezavershena stattya z matematiki Vi mozhete dopomogti proyektu vipravivshi abo dopisavshi yiyi Cya stattya potrebuye dodatkovih posilan na dzherela dlya polipshennya yiyi perevirnosti Bud laska dopomozhit udoskonaliti cyu stattyu dodavshi posilannya na nadijni avtoritetni dzherela Zvernitsya na storinku obgovorennya za poyasnennyami ta dopomozhit vipraviti nedoliki Material bez dzherel mozhe buti piddano sumnivu ta vilucheno gruden 2017 Otrimano z https uk wikipedia org w index php title Rerajting matematika amp oldid 38208083