Logo    
Деловая газета CitCity.ru CITKIT.ru - все об Open Source Форумы Все публикации Учебный центр Курилка
CitForum    CITForum на CD    Подписка на новости портала Море(!) аналитической информации! :: CITFORUM.RU
IT-консалтинг Software Engineering Программирование СУБД Безопасность Internet Сети Операционные системы Hardware

25.01.2017

Google
WWW CITForum.ru
С Новым годом!
2006 г.

Логические основы Пролога

Лекция из курса Основы программирования на языке Пролог

П. А. Шрайнер
Интернет Университет Информационных Технологий, INTUIT.ru

Эта лекция будет посвящена теоретическим основам языка Пролог. В принципе, вполне можно писать хорошие программы на языке Пролог, не вдаваясь в глубины математической логики. И в этом смысле можно считать эту главу необязательной, факультативной. Однако тем, кому интересно узнать, «как она вертится», мы попробуем объяснить, как устроен Пролог, на чем он основывается.

Давайте начнем с самого начала или почти с самого начала, раз уж мы договорились, что никаких предварительных навыков от слушателей не требуется. Нам придется попытаться разобраться с понятиями логики первого порядка, которая лежит в основе Пролога; они обычно изучаются в курсе математической логики. Конечно, для того чтобы изучить даже самые начала математической логики, одной лекции недостаточно. Поэтому мы попытаемся пробежаться только по тому кусочку, который имеет отношение к языку Пролог. Часть используемых нами понятий все-таки останется «за кадром».

Говорят, что задана некая формальная система F, если определены:

  1. алфавит системы — счетное множество символов;
  2. формулы системы — некоторое подмножество всех слов, которые можно образовать из символов, входящих в алфавит (обычно задается процедура, позволяющая составлять формулы из символов алфавита системы);
  3. аксиомы системы — выделенное множество формул системы;
  4. правила вывода системы — конечное множество отношений между формулами системы.

Зададим логику первого порядка (или логику предикатов), на которой основывается Пролог. Язык логики предикатов — один из формальных языков, наиболее приближенных к человеческому языку.

Алфавит логики первого порядка составляют следующие символы:

  1. переменные (будем обозначать их последними буквами английского алфавита u, v, x, y, z);
  2. константы (будем обозначать их первыми буквами английского алфавита a, b, c, d);
  3. функциональные символы (используем для их обозначения ближние буквы f и g);
  4. предикатные символы (обозначим их дальними буквами p, q и r);
  5. пропозициональные константы истина и ложь (true и false);
  6. логические связки ¬ (отрицание), (конъюнкция), (дизъюнкция), (импликация);
  7. кванторы: (существования), (всеобщности);
  8. вспомогательные символы (, ), ,.

Всякий предикатный и функциональный символ имеет определенное число аргументов. Если предикатный (функциональный) символ имеет n аргументов, он называется n-местным предикатным (функциональным) символом.

Термом будем называть выражение, образованное из переменных и констант, возможно, с применением функций, а точнее:

  1. всякая переменная или константа есть терм;
  2. если t1,...,tn — термы, а fn-местный функциональный символ,то f(t1,...,tn) — терм;
  3. других термов нет.

По сути дела, все объекты в программе на Прологе представляются именно в виде термов.

Если терм не содержит переменных, то он называется основным или константным термом.

Атомная или элементарная формула получается путем применения предиката к термам, точнее, это выражение p(t1,...,tn), где p — n-местный предикатный символ, а t1,...,tn — термы.

Формулы логики первого порядка получаются следующим образом:

  1. всякая атомная формула есть формула;
  2. если A и B — формулы, а x — переменная, то выражения ¬A (читается «не A» или «отрицание A»), A ∧ B (читается «A и B»), A ∨ B (читается «A или B»), A → B (читается «A влечет B»), ∃хA (читается «для некоторого x» или «существует x») и ∀xA (читается «для любого x» или «для всякого x»)– формулы;
  3. других формул нет.

В случае если формула имеет вид ∀xA или ∃хA, ее подформула A называется областью действия квантора ∀x или ∃х соответственно. Если вхождение переменной x в формулу находится в области действия квантора ∀ x или ∃х, то оно называется связанным вхождением. В противном случае вхождение переменной в формулу называется свободным.

Чтобы не увеличивать чрезмерно объем лекции, мы не будем рассматривать полный список аксиом и правил вывода логики первого порядка.Те из них, которые пригодятся нам в дальнейшем, будут приведены в соответствующих местах.

Литералом будем называть атомную формулу или отрицание атомной формулы. Атом называется положительным литералом, а его отрицание — отрицательным литералом.

Дизъюнкт — это дизъюнкция конечного числа литералов. Если дизъюнкт не содержит литералов, его называют пустым дизъюнктом и обозначают посредством символа ℵ.

Давайте посмотрим, как можно привести любую формулу к множеству дизъюнктов, с которым работает метод резолюций. Для этого нам понадобятся некоторые определения нормальных форм.

Говорят, что формула находится в конъюнктивной нормальной форме,если это конъюнкция конечного числа дизъюнктов. Имеет место теорема о том, что для любой бескванторной формулы существует формула, логически эквивалентная исходной и находящаяся в конъюнктивной нормальной форме.

Формула находится в предваренной (или пренексной) нормальной форме, если она представлена в виде Q1x1,...,QnxnA, где Qi — это квантор или , а формула A не содержит кванторов. Выражение Q1x1,...,Qnxn называют префиксом, а формулу Aматрицей.

Формула находится в сколемовской нормальной форме, если она находится в предваренной нормальной форме и не содержит кванторов существования.

Алгоритм приведения произвольной формулы исчисления предикатов к множеству дизъюнктов

Первый шаг. Приводим исходную формулу к предваренной нормальной форме. Для этого:

  1. пользуясь эквивалентностью A → B ≡ ¬A ∨ B исключим импликацию;
  2. перенесем все отрицания внутрь формулы, чтобы они стояли только перед атомными формулами, используя следующие эквивалентности:
    ¬(A ∨ B) ≡ ¬A ∧ ¬B
    ¬(A ∧ B) ≡ ¬A ∨ ¬B
    ¬(∃xA) ≡ ∀x¬A
    ¬(∀xA) ≡ ∃x¬A
    ¬¬A ≡ A
    
    
  3. переименовываем связанные переменные так, чтобы ни одна переменная не входила в нашу формулу одновременно связанно и свободно.
  4. выносим кванторы в начало формулы, используя эквивалентности:

    QxA(x) ∨ B ≡ Qx(A(x) ∨ B), если B не содержит переменной x, а Q ∈ {∀, ∃}

    QxA(x) ∧ B ≡ Qx(A(x) ∧ B), если B не содержит переменной x, а Q ∈ {∀, ∃}

    ∀xA(x) ∧ ∀xB(x) ≡ ∀x(A(x) ∧ B(x))
    ∃xA(x) ∨ ∃xB(x) ≡ ∃x(A(x) ∨ B(x))
    

    Q1xA(x) ∨ Q2xB ≡ Q1xQ2y(A(x) ∨ B(y)), где Q ∈ {∀, ∃}

    Q1xA(x) ∧ Q2xB ≡ Q1xQ2y(A(x) ∧ B(y)), где Q ∈ {∀, ∃}

Второй шаг. Проведем сколемизацию, т.е. элиминируем в формуле кванторы существования. Для этого для каждого квантора существования выполним следующий алгоритм.

Если устраняемый квантор существования — самый левый квантор в префиксе формулы, заменим все вхождения в формулу переменной, связанной этим квантором, на новую константу и вычеркнем квантор из префикса формулы.

Если левее этого квантора существования имеются кванторы всеобщности, заменим все вхождения в формулу переменной, связанной этим квантором, на новый функциональный символ от переменных, которые связаны левее стоящими кванторами всеобщности, и вычеркнем квантор из префикса формулы.

Проведя этот процесс для всех кванторов существования, получим формулу, находящуюся в сколемовской нормальной форме. Алгоритм устранения кванторов существования придумал Сколем в 1927 году.

Имеет место теорема о том, что формула и ее сколемизация эквивалентны в смысле выполнимости.

Третий шаг. Элиминируем кванторы всеобщности. Полученная формула будет бескванторной и эквивалентной исходной в смысле выполнимости.

Четвертый шаг. Приведем формулу к конъюнктивной нормальной форме, для чего воспользуемся эквивалентностями, выражающими дистрибутивность:

A ∨ (B ∧ C) ≡ (A ∨ B) ∧ (A ∨ C)
A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C)

Пятый шаг. Элиминируем конъюнкции, представляя формулу в виде множества дизъюнктов.

Получаем множество дизъюнктов, эквивалентное исходной формуле в том смысле, который дает нам следующая теорема.

Теорема. Формула является тождественно ложной тогда и только тогда, когда множество дизъюнктов, полученных из нее, является невыполнимым.

Напомним, что множество формул называется невыполнимым, если не существует такого означивания переменных, чтобы все формулы из этого множества были бы истинными.

Пример. Превратим формулу ∀x(P(x) → ∃y(P(y) ∨ ¬Q(x,y))) в эквивалентное ей множество дизъюнктов.

Первый шаг. Приведем исходную формулу к предваренной нормальной форме. Элиминировав импликацию, получим формулу ∀x(¬P(x) ∨ ∃y(P(y) ∨ ¬Q(x,y))). Вынесем переменную y за скобки: ∀x∃y(¬P(x) ∨ (P(y) ∨ ¬Q(x,y))). Это можно сделать, потому что формула ¬P(x) не зависит от переменной y. Если бы она зависела, то можно было бы переименовать связанную переменную y.

Второй шаг. Проведем сколемизацию полученной формулы. Левее квантора существования стоит квантор всеобщности, значит, нужно заменить все вхождения переменной y новым унарным функциональным символом, зависящим от x. Получим формулу, находящуюся в сколемовской нормальной форме: ∀x(¬P(x) ∨ (P(f(x) ∨ ¬Q(x,f(x)))).

Третий шаг. Элиминируем квантор всеобщности: ¬P(x) ∨ (P(f(x)) ∨ ¬Q(x,f(x))).

В четвертом и пятом шагах необходимости нет, поскольку формула уже представляет собой дизъюнкт: ¬P(x) ∨ P(f(x)) ∨ ¬Q(x,f(x)).

Следующая техника, лежащая в основе Пролога, с которой мы попробуем разобраться, — это унификация. Унификация позволяет отождествлять формулы логики первого порядка путем замены свободных переменных на термы.

Подстановка — это множество вида {x1/t1,..., xn/tn}, где для всех i, xi — переменная, а ti — терм, причем xi≠ti (отображение переменных в термы). При этом все переменные, входящие в подстановку, различны (для любого i≠j xi≠xj).

Символом ε будем обозначать пустую подстановку.

Подстановка, в которой все термы основные, называется основной подстановкой.

Простое выражение — это терм или атомная формула.

Если A — простое выражение, а θ — подстановка, то получается путем одновременной замены всех вхождений каждой переменной из θA соответствующим термом. называется частным случаем (примером) выражения A. Содержательно подстановка заменяет каждое вхождение переменной xi на терм ti.

Пусть θ и η — подстановки, θ={x1/t1,..., xn/tn}, η={y1/s1,...,yn/sn}. Композиция θη получается из множества {x1/t1η,...,xn/tn(,y1/s1,..., yn/sn} удалением пар xi/tiη, где xi≠tiη и пар yi/si, где yi совпадает с одним из xj.

Пример. Пусть θ={x/f(y),y/z}, η={x/a,y/b,z/y}. Построим θη. Для этого возьмем множество {x/f(b),y/y,x/a,y/b,z/y} и выбросим из него пары y/y (потому что заменяемая переменная совпадает с термом), ,x/a,y/b (потому что заменяемая переменная из подстановки η совпадает с заменяемой переменной из подстановки θ). Получим ответ: θη={x/f(b),z/y}.

Подстановка θ называется более общей, чем подстановка η, если существует такая подстановка γ, что η=θ γ.

Подстановка θ называется унификатором простых выражений A и B, если Aθ=Bθ. Про A и B в такой ситуации говорят, что они унифицируемы. Унификация используется в Прологе для композиции и декомпозиции структур данных.

Пример. A=p(f(x),z) и B=p(y,a) унифицируемы. Можно взять в качестве их унификатора подстановку {y/f(x),z/a} или подстановку {y/f(a),x/a,z/a}.

Вообще говоря, две формулы могут иметь бесконечно много унификаторов. Унификатор θ называют наиболее общим (или простейшим) унификатором простых выражений A и B, если он является более общей подстановкой, чем все другие унификаторы простых выражений A и B.

Пример. В рассмотренном выше примере наиболее общим унификатором является подстановка {y/f(a),z/a}.

Пусть S — конечное множество простых выражений. Определим множество d(S) разногласий (рассогласований). Зафиксируем самую левую позицию, на которой не во всех выражениях из S стоит один и тот же символ. Занесем в d(S) подвыражения выражений из S, начинающиеся с этой позиции.

Пример. Пусть S={p(f(x),h(y),a),p(f(x),z,a),p(f(x),h(y),b)}. Множество рассогласований для S d(S)={h(y),z}.

Алгоритм унификации

Дадим алгоритм поиска наиболее общего унификатора для конечного множества простых выражений S. В том случае, если это множество не унифицируемо, алгоритм должен обнаруживать эту ситуацию.

Шаг 1. Полагаем k=0, δ 0.

Шаг 2. Если k — одноэлементное множество, останавливаем алгоритм, δk — наиболее общий унификатор для S. В противном случае строим множество рассогласований d(Sδk) и переходим к третьему шагу.

Шаг 3. Если в d(Sδk) существуют переменная x и терм t такие, что x не входит в t, то полагаем что δk+1k{x/t}. Увеличиваем на единицу k, переходим ко второму шагу. Иначе останавливаем алгоритм, множество S не унифицируемо.

Обратите внимание, что алгоритм унификации заканчивает свою работу за конечное число шагов для любого конечного множества простых выражений, потому что на каждом проходе мы уменьшаем количество переменных. Так как множество простых выражений было конечным, то и множество различных переменных в нем конечно, и, значит, через число шагов, не превышающее количества различных переменных, алгоритм завершится.

Утверждение о том, что для любого унифицируемого конечного множества простых выражений S алгоритм унификации закончит свою работу и выдаст наиболее общий унификатор для S, называется теоремой унификации.

Теперь можно перейти к рассмотрению метода резолюций.

В чем вообще заключается задача? Мы хотим построить алгоритм, который позволял бы нам автоматически давать ответ на вопрос, может ли быть выведено некоторое заключение из множества имеющихся посылок. Известно, что в общем случае даже для логики первого порядка такой алгоритм невозможен. Как правило, формальные системы, для которых можно построить подобный разрешающий алгоритм, обладают небольшой выразительной силой. К ним, например, относится логика высказываний и логика одноместных предикатов.

Однако Робинсон решил, что правила вывода, используемые компьютером при автоматическом выводе, не обязательно должны совпадать с правилами вывода, используемыми при «человеческом» выводе. В частности, он предложил вместо правила вывода «modus ponens», которое утверждает, что из A и A → B выводится B, использовать его обобщение, правило резолюции, которое сложнее понимается человеком, но эффективно реализуется на компьютере. Давайте попробуем разобраться с этим правилом.

Правило резолюции для логики высказываний можно сформулировать следующим образом.

Если для двух дизъюнктов существует атомная формула, которая в один дизъюнкт входит положительно, а в другой отрицательно, то, вычеркнув соответственно из одного дизъюнкта положительное вхождение атомной формулы, а из другого — отрицательное, и объединив эти дизъюнкты, мы получим дизъюнкт, называемый резольвентой. Исходные дизъюнкты в таком случае называются родительскими или резольвируемыми, а вычеркнутые формулы — контрарными литералами. Другими словами, резольвента — это дизъюнкт, полученный из объединения родительских дизъюнктов вычеркиванием контрарных литералов.

Графически это правило можно изобразить так:

(A ∨B, P ∨ ¬P)/A ∨ B

Здесь A ∨ P и B ∨ ¬P — родительские дизъюнкты, P и ¬P — контрарные литералы, A ∨ B — резольвента.

Если родительские дизъюнкты состояли только из контрарных литералов, то резольвентой будет пустой дизъюнкт.

Пример. Правило вывода «modus ponens» получается из правила резолюции, если взять в качестве родительских дизъюнктов C1=A, C2=¬A ∨ B(≡ A → B). Контрарными литералами в применении этого правила будут A и ¬A, резольвентой — формула B.

Сформулируем правило резолюции для логики первого порядка.

Пусть имеется два дизъюнкта C1 и C2, у которых нет общих переменных, L1 — литерал, входящий в дизъюнкт C1, L2 — литерал, входящий в дизъюнкт C2. Если литералы имеют наибольший общий унификатор θ, то дизъюнкт (C1θ–L1θ)∪(C2θ–L2θ) называется резольвентой дизъюнктов C1 и C2. Литералы L1 и L2 называются контрарными литералами. То же правило записывается в графическом виде как

(A ∨ P2, B ∨ ¬P2)/(A ∨ B)θ

Здесь P1 и P2 — контрарные литералы, (A ∨ B)θ — резольвента, полученная из дизъюнкта (A ∨B) применением унификатора θ, A ∨ P1 и B ∨ P2 — родительские дизъюнкты, а θ — наибольший общий унификатор P1 и P2.

Метод резолюций является обобщением метода «доказательства от противного». Вместо того чтобы пытаться вывести некоторую формулу-гипотезу из имеющегося непротиворечивого множества аксиом, мы добавляем отрицание нашей формулы к множеству аксиом и пытаемся вывести из него противоречие. Если нам удается это сделать, мы приходим к выводу (пользуясь законом исключенного третьего), что исходная формула была выводима из множества аксиом. Опишем более подробно.

Добавим отрицание исходной формулы к множеству посылок, преобразуем каждую из этих формул во множество дизъюнктов, объединим получившиеся множества дизъюнктов и попытаемся вывести из этого множества дизъюнктов противоречие (пустой дизъюнкт ). Для этого будем выбирать из нашего множества дизъюнкты, содержащие унифицируемые контрарные литералы, вычислять их резольвенту по правилу резолюции, добавлять ее к исследуемому множеству дизъюнктов. Этот процесс будем продолжать до тех пор, пока не выведем пустой дизъюнкт.

Возможны, вообще говоря, три случая:

  1. Этот процесс никогда не завершается.
  2. Среди текущего множества дизъюнктов не окажется таких, к которым можно применить правило резолюции. Это означает, что множество дизъюнктов выполнимо, и, значит, исходная формула не выводима.
  3. На очередном шаге получена пустая резольвента. Это означает, что множество дизъюнктов невыполнимо и, следовательно, начальная формула выводима.

Имеет место теорема, утверждающая, что описанный выше процесс обязательно завершится за конечное число шагов, если множество дизъюнктов было невыполнимым.

С другой стороны, мы опираемся на результат, что формула выводима из некоторого множества формул тогда и только тогда, когда описанное множество дизъюнктов невыполнимо. А также на то, что множество дизъюнктов невыполнимо тогда и только тогда, когда из него применением правила резолюции можно вывести пустой дизъюнкт.

В сущности, метод резолюций несовершенен и приводит к «комбинаторному взрыву». Однако некоторые его разновидности (или стратегии) довольно эффективны. Одной из самых удачных стратегий является линейная или SLD-резолюция для хорновских дизъюнктов (Linear resolution with Selection function for Definition clauses), то есть дизъюнктов, содержащих не более одного положительного литерала. Их называют предложениями или клозами.

Если дизъюнкт состоит только из одного положительного литерала, он называется фактом. Дизъюнкт, состоящий только из отрицательных литералов, называется вопросом (или целью или запросом). Если дизъюнкт содержит и позитивный, и негативные литералы, он называется прави- лом. Правило вывода выглядит примерно следующим образом ¬A1 ∨ ¬A2...¬An ∨ B. Это эквивалентно формуле A1 ∧ A2... ∧An → B, которая на Прологе записывается в виде

B:–A1,A2,...,An.

Логической программой называется конечное непустое множество хорновских дизъюнктов (фактов и правил).

При выполнении программы к множеству фактов и правил добавляется отрицание вопроса, после чего используется линейная резолюция. Ее специфика в том, что правило резолюции применяется не к произвольным дизъюнктам из программы. Берется самый левый литерал цели (подцель) и первый унифицируемый с ним дизъюнкт. К ним применяется правило резолюции. Полученная резольвента добавляется в программу в качестве нового вопроса. И так до тех пор, пока не будет получен пустой дизъюнкт, что будет означать успех, или до тех пор, пока очередную подцель будет невозможно унифицировать ни с одним дизъюнктом программы, что будет означать неудачу.

В последнем случае включается так называемый бэктрекинг — механизм возврата, который осуществляет откат программы к той точке, в которой выбирался унифицирующийся с последней подцелью дизъюнкт. Для этого точка, где выбирался один из возможных унифицируемых с подцелью дизъюнктов, запоминается в специальном стеке, для последующего возврата к ней и выбора альтернативы в случае неудачи. При откате все переменные, которые были означены в результате унификации после этой точки, опять становятся свободными.

В итоге выполнение программы может завершиться неудачей, если одну из подцелей не удалось унифицировать ни с одним дизъюнктом программы, и может завершиться успешно, если был выведен пустой дизъюнкт, а может и просто зациклиться.

Подписка на новости IT-портала CITForum.ru
(библиотека, CITKIT.ru, CitCity)

Новые публикации:

24 декабря

CITKIT.ru:

  • Новогодние поздравления
  • Сергей Кузнецов. Цикл Операционные системы: Ностальгия по будущему:

  • Алексей Федорчук. OpenSolaris 2008.11 Release

  • Сергей Голубев:

  • Евгений Чайкин aka StraNNik (Блогометки):

    17 декабря

  • С.Д.Кузнецов. Базы данных. Вводный курс

    10 декабря

    CITKIT.ru:

  • OpenSolaris 2008.11 Release

  • Альтернативные ОС: две грустные истории (С.Кузнецов)
  • Nokia N810 — доведение до ума
  • CitCity:

  • Платформа 2009: заоблачные перспективы Microsoft

    4 декабря

  • Лекция С.Д.Кузнецова Понятие модели данных. Обзор разновидностей моделей данных

    CITKIT.ru:

  • OpenSolaris 2008.11 Release. Первые впечатления

  • Linux vs FreeBSD: продолжим "Священные войны"?

  • Nokia N810 as is

  • Индульгенция для FOSS

  • Друзья СПО'2008

    26 ноября

  • Нечеткое сравнение коллекций: семантический и алгоритмический аспекты

    CitCity:

    CITKIT.ru:

  • Глава из книги А.Федорчука
    Сага о FreeBSD:
  • 19 ноября

  • Проблемы экономики производства крупных программных продуктов

  • Язык модификации данных формата XML функциональными методами

    CITKIT.ru:

  • Главы из книги А.Федорчука
    Сага о FreeBSD:

    Заметки к книге:

  • FreeBSD: монтирование сменных устройств и механизм HAL
  • Текстовый редактор ee

    12 ноября

  • Правило пяти минут двадцать лет спустя, и как флэш-память изменяет правила (Гоц Грейф, перевод: Сергей Кузнецов)

    CITKIT.ru:

  • Главы из книги А.Федорчука
    Сага о FreeBSD:
  • OSS в России: взгляд правоведа (В.Житомирский)

  • Новая статья из цикла С.Голубева "Железный марш":

    29 октября

  • О некоторых задачах обратной инженерии

  • Веб-сервисы и Ruby

  • Тестирование web-приложений с помощью Ruby

    CITKIT.ru:

  • Главы из книги А.Федорчука
    Сага о FreeBSD:

  • PuppyRus Linux - беседа с разработчиком (С.Голубев)

  • Сергей Кузнецов. Заметка не про Linux

    22 октября

  • Обзор методов описания встраиваемой аппаратуры и построения инструментария кросс-разработки

    CITKIT.ru:

  • Сергей Кузнецов. Почему я равнодушен к Linux

  • Глава из книги А.Федорчука
    Сага о FreeBSD:
  • Что надо иметь
    3. Базовые познания

    CitCity:

  • Управление IT-инфраструктурой на основе продуктов Microsoft

    15 октября

  • Методы бикластеризации для анализа интернет-данных

    CitCity:

  • Разъемы на ноутбуках: что они дают и зачем их так много?
  • AMD Puma и Intel Centrino 2: кто лучше?

    CITKIT.ru:

  • Новый цикл статей С.Голубева
    Железный марш:

  • Главы из книги А.Федорчука
    Сага о FreeBSD:

    8 октября

  • Автоматизация тестирования web-приложений, основанных на скриптовых языках
  • Опыт применения технологии Azov для тестирования библиотеки Qt3

    Обзоры журнала Computer:

  • SOA с гарантией качества
  • Пикоджоуль ватт бережет
  • ICT и всемирное развитие

    CitCity:

  • Пиррова победа корпорации Microsoft

    CITKIT.ru:

  • Главы из книги А.Федорчука
    Сага о FreeBSD:

    Статья из архива:

  • Я живу в FreeBSD (Вадим Колонцов)

    Новые Блогометки:

  • Перекройка шаблона Blogger или N шагов к настоящему
  • Blogger. Comment style
  • Screenie или глянцевый снимок экрана

    2 октября

    CITKIT.ru:

  • Сага о FreeBSD (А. Федорчук)

    Zenwalk: пакет недели

  • Банинг — интеллектуальное развлечение (С.Голубев)

    CitCity:

    25 сентября

  • Клермонтский отчет об исследованиях в области баз данных

    CITKIT.ru:

  • Пользователям просьба не беспокоиться... (В.Попов)

  • Снова про ZFS: диск хорошо, а два лучше
  • Командная оболочка tcsh (А.Федорчук)

    Zenwalk: пакет недели

    17 сентября

  • T2C: технология автоматизированной разработки тестов базовой функциональности программных интерфейсов
  • Технология Azov автоматизации массового создания тестов работоспособности

    CITKIT.ru:

  • FreeBSD: ZFS vs UFS, и обе-две — против всех (А.Федорчук)

    Zenwalk: пакет недели

  • Дачнет — практика без теории (С.Голубев)

    10 сентября

  • За чем следить и чем управлять при работе приложений с Oracle
  • Планировщик заданий в Oracle
    (В.Пржиялковский)

    CITKIT.ru:

  • Microsoft: ответный "боян" (С.Голубев)

  • Причуды симбиоза, или снова "сделай сам" (В.Попов)

  • Файловые системы современного Linux'а: последнее тестирование
  • Zsh. Введение и обзор возможностей
    (А.Федорчук)

    Описания пакетов Zenwalk: Zsh, Thunar, Thunar-bulk-rename, Xfce4-places-plugin, Xfce4-fsguard-plugin

    Блогометки:

  • Google Chrome
  • Лончер для ASUS Eee PC 701

    3 сентября

    CITKIT.ru:

  • Заметки о ядре (А.Федорчук):

    Добавлены описания пакетов Zenwalk: Galculator, Screenshot, Gnumeric, Pidgin

    В дискуссинном клубе:

  • И еще о Википедии и Google Knol

  • Лекция для начинающего линуксоида (С.Голубев)

    26 августа

  • Транзакционная память (Пересказ: С. Кузнецов)

    CITKIT.ru:

  • Открыт новый проект Zenwalk: пакет недели

  • Статья Текстовые процессоры и их быстродействие: конец еще одной легенды?

    21 августа

    CITKIT.ru:

  • Почему школам следует использовать только свободные программы (Ричард Столлман)
  • Беседа Сергея Голубева с учителем В.В.Михайловым

  • Википедия или Гуглезнание? Приглашение к обсуждению (Алексей Федорчук)
  • Народная энциклопедия от Google (StraNNik)

  • Обзор Mandriva 2009.0 Beta 1 Thornicrofti
  • Новичок в Линукс: Оптимизируем Mandriva 2008.1

  • Книга Zenwalk. Приобщение к Linux:

    13 августа

    CitCity:

  • Мирный Atom на службе человеку. Обзор платы Intel D945GCLF с интегрированным процессором
  • Обзор процессоров Intel Atom 230 на ядре Diamondville

  • iPhone - год спустя. Скоро и в России?

    CITKIT.ru:

  • Интермедия 3.4. GRUB: установка и настройка (из книги Zenwalk. Приобщение к Linux)

    6 августа

  • СУБД с хранением данных по столбцами и по строкам: насколько они отличаются в действительности? (Пересказ: С. Кузнецов)

    CITKIT.ru:

  • Интермедия 2.2. Что неплохо знать для начала (из книги Zenwalk. Приобщение к Linux)

  • И снова про шрифты в Иксах (А.Федорчук)

  • 20 самых быстрых и простых оконных менеджеров для Linux

  • Дело о трех миллиардах (С.Голубев)

    30 июля

  • OLTP в Зазеркалье (Пересказ: С. Кузнецов)

    CitCity:

  • Будущее BI в облаках?
  • Тиражные приложения и заказная разработка. Преимущества для заказчика
  • Дискуссия со сторонниками заказной разработки

    CITKIT.ru:

  • Новые главы книги Zenwalk. Приобщение к Linux:
  • Глава 8. Пакеты: средства установки, системы управления, системы построения
  • Глава 9. Zenwalk: репозитории, пакеты, методы установки

    23 июля

    CITKIT.ru:

  • Все против всех. 64 vs 32, Intel vs AMD, tmpfs vs ext3
  • Две головы от Intel

  • Zenwalk: обзор штатных приложений (глава из книги "Zenwalk. Приобщение к Linux")

  • Нормально, Григорий...

    16 июля

    Обзоры журнала Computer:

  • Перспективы и проблемы программной инженерии в XXI веке
  • Большие хлопоты с большими объемами данных
  • Перспективы наноэлектроники

    CITKIT.ru:

  • Интермедия о лицензиях (А.Федорчук. "Zenwalk. Приобщение к Linux")

  • Есть ли будущее у KDE?

  • Linux в школе: альтернативный вариант в задачах

  • Шифр (приключения агента Никодима)

    10 июля

    CITKIT.ru:

  • Новые разделы книги А. Федорчука Zenwalk. Приобщение к Linux:
  • Интермедия вступительная. Linux или GNU/Linux? Как вас теперь называть?
  • Глава 5. Среда Xfce
  • Глава 6. Xfce: приложения и плагины

  • ZUR (Zenwalk User Repository) FAQ

    2 июля

  • Персистентность данных в объектно-ориентированных приложениях (С. Кузнецов)

    CITKIT.ru:

  • Новые разделы книги А. Федорчука Zenwalk. Приобщение к Linux:
  • Интермедия 1.2. Дорога к Zenwalk'у. Период бури и натиска
  • Интермедия 3.3. Немного о Linux'е и "железе"
  • Глава 4. Настройка: инструментами и руками
  • Интермедия 4.1. Zenpanel и конфиги: поиски корреляции

  • Интервью с Жан-Филиппом Гийоменом, создателем дистрибутива Zenwalk

  • Linux в школе: первые итоги (С. Голубев)

    25 июня

    CITKIT.ru:

  • Zenwalk. Приобщение к Linux (А. Федорчук)

  • Логика и риторика (С.Голубев)

  • Технология Tru64 AdvFS

  • Ханс Райзер предлагает отвести полицейских к телу Нины

    18 июня

  • Проекты по управлению данными в Google (Пересказ: С. Кузнецов)

    CITKIT.ru:

  • ОС и поддержка "железа": мифы и реальность (А. Федорчук)

  • Linux в школе: другие дистрибутивы

  • Пинок (С. Голубев)

    4 июня

  • Ландшафт области управления данными: аналитический обзор (С. Кузнецов)

    CITKIT.ru:

  • Linux в школе: слово заинтересованным лицам

  • SlackBuild: пакеты своими руками

  • Linux от компании Novell. Установка и обзор openSUSE Linux

    Все публикации >>>




  • IT-консалтинг Software Engineering Программирование СУБД Безопасность Internet Сети Операционные системы Hardware

    Информация для рекламодателей Пресс-релизы — pr@citcity.ru
    Послать комментарий
    Информация для авторов
    Rambler's Top100 This Web server launched on February 24, 1997
    Copyright © 1997-2017 CIT, © 2001-2017 CIT Forum
    Внимание! Любой из материалов, опубликованных на этом сервере, не может быть воспроизведен в какой бы то ни было форме и какими бы то ни было средствами без письменного разрешения владельцев авторских прав. Подробнее...