<\a>Введение в реляционную логику   М.А.Малков . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4
Реляционная логика есть интеграция классической и компьютерной логик. В классической логике неестественная (NBG) теория множеств заменена естественной. В доказательстве теорем компьютерной логики, предложения в A-предваренной форме с функциями Сколема заменены предложениями в AE-предваренной форме без неестественных функций (A - символ квантора всеобщности, E - символ квантора существования). Это позволило заменить индукцию компьютерно-ориентированным правилом конечного спуска. Удален побочный эффект в логическом программировании средствами компьтерной логики. Это позволило решить проблему отрицания.

Термин "Реляционная логика" возник из термина "Реляционное исчисление", введенного Е. Коддом. Его термин отличается от термина "Исчисление предиктов" представлением функций в форме отношений, т.к. отношения проще для компьютерной обработки чем функции.
Но это означает, что термы отсутствуют и любой атом (атомарная формула) представлен синтаксически в виде символа отношения с аргументными местами, заполненными символами переменных.
Использование атомов без термов усложняет логические формулы. Поэтому термы все же вводятся, но только для сокращенной записи формул. При этом оказалось, что термами могут быть не только функции, но и предикаты тоже (под предикатами в данном случае подразумеваются отношения, не содержащие функциональные зависимости между переменными).
Термин "Компьютерная логика" был введен Дж. А. Робинсоном. Одна из проблем этой логики есть доказательство теорем. Все формулы этой логики должны быть представлены в виде дизъюнктивных предложений, в форме Сколема без кванторов. Общезначимые формулы должны отсутствовать в этой форме. Любое подмножество формул, представленных в виде дизъюнктивных предложений, является множеством аксиом некоторой теории. Эти аксиомы могут включать теоремы и определения. Основными правилами вывода являются резолюция (компьютерный аналог modus ponens) и парамодуляция (компьютерный аналог аксиом равенства).
В настоящее время вместо дизъюнктивных предложений используются обобщенные предложения. Они состоят из одного (или ниодного) дизъюнктивного предложения и нескольких конъюнктивных предложений. Все эти предложения соединены дизъюнкциями. Элементы конъюнктивных предложений соединены конъюнкциями и включают переменные, связанные кванторами существования. Эти кванторы являются неявными и подразумеваются в начале каждого конъюнктивного предложения. Существуют конъюнктивные предложения, состоящие из одной литеры (литера есть атом с или без отрицания).
Обобщенные предложения образуются из AE-предваренных форм без Сколемовских функций. Кванторы отсутсвуют в обобщенном предложении, т.к. переменные, связанные квантороми всеобщности, обозначаются x_i (i - натуральное число), а переменные, связанные кванторами существования обозначаются a_i.
Как исключение, обощенные предложения могут быть EA-предваренными, тогда переменные, связанные кванторами существования обозначаются c_i.
Обобщенные предложения используются при доказательстве теорем и образуют первую нормальную форму для логических формул. Правила вывода для обобщенных предложений называются обобщенной резолюцией и обобщенной парамодуляцией.
Обобщенные предложения незаменимы для применения индукции. Компьютерный аналог индукции называется конечным спуском и компьютерный аналог бесконечного спуска называется обобщенным конечным спуском.
Другая часть компьютерной логики есть логическое программирование, созданное A. Colmerauer. Одна из проблем этого программирования есть построение моделей для теорий.
В этой части логики все формулы должны быть положительными определениями математических понятий в AE-предваренной форме. Эти определения образуют вторую нормальную форму для логических формул.
Вторая нормальная форма включает обратную импликацию "<-" с определяемым атомом в левой части этой импликации и с определяющей формулой в правой части. Определяющая формула представляется конюнктивным предложением, т.е. множеством литер, соединенных конъюнкциями. Определяющая формула не должна быть общезначимой.
Еще одной проблемой является конструирование всех моделей, т.е. использование теории множеств. Считается, что все модели являются числовыми и могут быть получены из множества натуральных чисел и конечного числа операций прямого произведения и множества всех подмножеств. Эта теория непротиворечива.
Последняя часть компьютерной логики есть финитная логика. Эта логика предназначена для конструирования теорий (баз знаний) и их конструктивных моделей (баз данных) с помощью компьтерных вычислений. Для немонотонных вычислений используется стандартная 4-значная логика, и эта логика позволяет решить проблему отрицания. Стандартная 4-значная логика используется только в момент вычислений. По окончании вычислений осуществляется возврат к 2-значной логике.
Основной проблемой финитной логики является высокая эффектиность вычислений.
Интеграция классической и компьютерной логик позволяет улучшить последнюю. Т.е. интеграция классической и компьютерной логик позволяет устранить довольно обширные исследования, которые являются ошибочными или ненужными.

<\a>Реляционная логика высказываний  М.А.Малков. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
Логика высказываний включает исчисление теорий, т.е. конструирование всех теорий первого порядка, и исчисление аксиом, т.е. конструирование всех аксиом любой теории. Но эти исчисления сами являются теориями и принадлежат множеству теорий первого порядка.

Все теории первого порядка и их аксиомы представлены дизъюнктивными предложениями. Эти предложения выводятся из конъюнктивной нормальной формы. Общезначимые формулы отсутствуют.
В первом из упомянутых исчислений все непротиворечивые теории конструируются из 5 атомов. Число этих теорий равно 4 10⁹, но неавтоморфных теорий (над множеством литералов) только 10⁶. Далее дана классификация этих теорий.
Во втором исчислении решаются 3 проблемы: выявление противоречивых теорий (для доказательства теорем), замыкание теорий и конструирование всех систем независимых аксиом для заданной теории.
Все правила (алгоритмы) решения этих проблем в обоих исчислениях имеют эффективность, не сравнимую с существующими правилами.

<\a>Реляционная логика и арифметика.   М.А.Малков. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
Представлены 4 аксиомы для натуральных чисел: функция следования инъективна, 0 не следует ни за каким числом, существует естественный порядок и не существует число, промежуточное между любым другим числом и следующим за ним. Общезначимые формулы не включены в аксиомы. Правило индукции заменено конечным спуском.
Остальные числа, не являющиеся натуральными, конструируются путем инверсии быстрорастущих функций порядка n. Целые числа конструируются путем инверсии быстрорастущих функций порядка 1. Рациональные числа конструируются путем инверсии быстрорастущих функций порядка 2. Быстрорастущие функции порядка три имеют две инверсные функции, которые используются для конструирования чисел, называемых радикалами и логарифмами. Существуют арифметические числа порядка 4 и выше.

<\a>Аксиомы классической теории множеств  М.А.Малков. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80
Аксиомы классической теории множеств NBG разделены на аксиомы для одноместных множеств и аксиомы для многоместных множеств. Эти аксиомы представлены в первой нормальной форме тоже, т.е. становятся программами, готовыми к выполнению.

<\a>Функциональное расширение языка C++. I. IF и BREAK предложения. VOID и CLASS типы  М.А.Малков. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
Расширение синтаксиса языка C++ заключается в сведении предложений этого языка к операциям. Расширенны условные операции, перегружено предложение "break". Это позволило исключить предложения "if", "for", "while", "do", "go to", "try", "throw" и "catch". Как правило, операции с аргументом "void" имеют значение "void".

Расширено множество постфиксных операций присвоения. Любая операция в префиксной форме может быть использована в постфиксной форме тоже. В частности, операция сложения может быть использована в двух формах "+=" и "=+".
Расширены синтаксис и семантика типа "class". Этот тип может инкапсулировать не только функции, но и все типы данных, обрабатываемые этими функциями. Это позволило исключить спецификатор "friend" и указатель "this".

<\a>Реляционное программирование.  М.А.Малков. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89
Реляционные программы целиком состоят из процедур (отношений). Функции используются только для вычисления значений аргументов (актуальных параметров). Эти функции принадлежат фиксированному множеству и используются для конструирования термов. Отношения используются для конструирования логических формул. Программа определяется как множество логических формул. Это множество может быть использовано для конструирования теорий (баз знаний, если каждое знание формализовать в виде логических формул) или модели (базы данных) этих теорий.

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