Содержание. Аннотации.

Реляционная логика является расширением классической. Особая часть реляционной логики называется естественной реляционной логикой. Изящная, но неестественная классическая теория множеств заменена наиболее естественной (натуральной) теорией множеств. В натуральной теории множеств семейство всех счетных ординалов счетно.

<\a>Реляционная логика и арифметика действительных чисел. Нестандартный анализ.    М.А.Малков . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
Арифметика действительных чисел построена на основе модели Кантора. Непрерывность определена на основе реляционной логики. Арифметика гипердействительных чисел тоже построена на основе модели Кантора. Реляционная логика используется для определения гиперпродолжения, приращения и дифференциала. Принцип переноса, оценка неопределенностей, интегралы, ряд Тейлора и замена суммы интегралом излагаются более естественно.
Действительные числа определены как левые полубесконечные интервалы рациональных чисел. Множество этих интервалов есть стандартная модель действительных чисел. Это расширение модели Кантора для действительных чисел. Операции суммы и умножения, константы 0 и 1 определяются. Показано выполнение всех аксиом поля действительных чисел. Определено вложение натуральных и рациональных чисел в это поле.
Дано определение непрерывных отношений на основе топологии в Евклидовом пространстве Rⁿ. Отношения рассматриваются как многообразие, карты которого являются функциональными зависимостями.
Далее, гиперрациональные числа представлены как расширение поля рациональных чисел при добавлении нового рационального числа delta, бесконечно близкого к 0. Такое расширение есть поле рациональных функций от delta. Бесконечно малые гипердействительные числа определены как левые интервалы бесконечно малых гиперрациональных чисел. Положительные бесконечные гиперреальные числа определены как левые интервалы положительных бесконечных гиперрациональных чисел. Это позволяет определить все остальные гипердействительные числа. Показано, что стандартная модель гиперрациональных чисел есть подмножество для N² P (N⁵). Определены внешние гипердействительные числа. Множество их несчетно и между двумя произвольными гипердействительными числами есть внешние числа. Ассоциативный закон для внешних чисел не действует, и эти числа удалены из гипердействительной оси. Натуральные и рациональные числа вложены в поле гипердействительных чисел. Константы 0, 1, delta, арифметические действия и отношение порядка определены для гипердействительных чисел. Все аксиомы поля рациональных чисел выполняются, кроме аксиомы непрерывности для гипердействительной оси. Но принцип Архимеда выполняется, если натуральные числа дополнить гипернатуральными.
Вводится отношение близости. Это отношение формирует классы эквивалентности. Кроме двух классов, каждый класс эквивалентности содержит одно действительное число и все гипердействительные числа вблизи него. Два класса содержат все бесконечные гипердействительные числа. Один класс содержит числа вблизи -infty, другой класс содержит числа вблизи +infty. Этот более удобно по сравнению с теорией Робинсона.
Определено гиперрасширение действительных отношений. Каждая изолированная точка в отношении остается без изменений, каждая точка, являющаяся пределом в данном направлении Евклидова пространства, дополнена таким интервалом гиперреальной оси, который помещен в данном направлении и содержит соответствующую часть эквивалентного класса для этой точки. Все это обеспечивает единственность гиперрасширения. Кроме того, гиперрасширение есть оператор, и для него существует обратный оператор "стандартной части".
Исследован принцип переноса: те же самые логические формулы выполняются в арифметиках действительных и гипердействительных чисел, если все определения правильны. В частности, обычное определение непрерывности не является правильным в арифметике гипердействительных чисел, т.к. гиперрасширение некоторых функций может быть непрерывно, хотя эти функции разрывны. Функция Дирехле перестает быть функцией при гиперрасширении. Так что принцип переноса должен использоваться очень аккуратно.
Раскрытие неопределенностей, т.е. термов, которые становится невычисленными в некоторых точках, осуществляется заменой 0 бесконечно малым числом delta, преобразованиями и взятием стандартной части, в результате терм становится вычислимым.
Далее, бесконечно малая константа delta определена как проекция на независимую ось бесконечно малых векторов. Бесконечно малые векторы используются для определения направлений. Направления рассматриваются как векторы нулевой длины, не имеющие проекций. Если рассматривать направления как векторы бесконечно малой длины, то проекции существуют и тоже являются бесконечно малыми.
Определены приращения и дифференциалы для отношений. Приращения рассматриваются как вектор, который начинает и заканчивается в точках отношения. Этот вектор имеет независимые и зависимые проекции. Когда независимые проекции стремятся к delta, зависимые компоненты становятся гипердействительными числами. Независимые проекции становятся дифференциалом относительно независимой оси, линейная часть зависимых приращений становится дифференциалом относительно зависимой оси. То есть, независимый дифференциал постоянен и равен delta.
Если отношения представить как мнообразия с картами, тогда можно рассматривать приращения и дифференциалы для функций. Дифференциалы функций заменяют зависимые дифференциалы.
Определенные интегралы определены как бесконечная сумма произведений delta и подинтегрального выражения в каждой точке. Это расширяет определение Лебега для гипердействительных значений.
Нестандартные методы анализа, развитые Лейбницем и используемые Тейлором, применяются к построению бесконечных рядов Тейлора, формул Эйлера-Маклорена, бесконечных сумм, O и o-оценок, методов раскрытия неопределенностей и т.д.

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

Статья состоит из трех частей.
Первая часть посвящена определимости отношений.
Отмечено, что в любой теории есть неопределимые и определимые отношения. Свойства неопределимых отношений установлены основными аксиомами теории, свойства остальных отношений установлены определениями.
Понятие определимо, если оно является отношением, и это отношение есть левая часть определения, а правая часть определения - формула логики любого порядка. Левые и правильные части разделены символом логической эквивалентности.
Каждое определение делится на положительное и отрицательное.
В положительном определении символ логической эквивалентности заменен обратной импликацией в виде стрелки, направленной налево: "<-".
В отрицательном определении символ логической эквивалентности заменен обычной импликацией, или заменен обратной импликацией, но тогда левые и правые части определения дополнены отрицанием.
Положительное определение используется для конструирования моделей теории, отрицательное определение используется для конструирования дополнения этих моделей.
Первая нормальная форма введена для представления положительных и отрицательных определений. Эта форма позволяет устранить неоднозначность определений представлением их в AEКНФ, то есть в предваренной конъюнктивной нормальной форме с кванторами всеобщности, предшествующими кванторам существования. Тогда все кванторы можно удалить.
Первая нормальная форма очень удобна для автоматического доказательства теорем теории.
Вторая часть статьи посвящена вычислимости отношений.
Под вычислимостью подразумевается построение модели теории на абстрактном компьютере с неограниченными ресурсами. Под вычислимостью отношения подразумевается построение множества, интерпретирующего это отношение в данной модели данной теории (на том же самом компьютере).
Отношение вычислимо, даже если соответствующее множество бесконечно. Но бесконечная работа компьютера не допустима. Так что основа вычислимости - приближенные вычисления. Вычислимость состоит из шагов, и каждый новый шаг (или группа шагов) позволяет увеличить точность вычислений. Можно вычислять бесконечные объекты, в частности, бесконечные множества путем приближения конечными множествами. Другие примеры бесконечных объектов - иррациональные числа, интегралы и т.д.
Вычислимость и определимость имеют близкую связь. Определение отношения во второй нормальной форме есть программа, готовая к выполнению на абстрактном компьютере. Это означает, программа не зависит от модели теории. Но результат работы программы зависит от модели.
Определение отношения вычислимо, если вторая нормальная форма содержит только вычислимые отрицания. Если отрицание невычислимо, необходимо искать другое определение отношения или использовать стандартную 4-х значную логику, которая позволяет вычислять даже невычислимое отрицание. Эта логика может использоваться, если отношение вычислимо, то есть существует определение с вычислимым отрицанием, но это определение трудно найти.
Вместо машины Тьюринга используется реляционный компьютер. Этот компьютер выполняет программы в первой и второй нормальной форме. Для второй нормальной формы сформулированы правила вычисления конъюнкций, отрицаний, кванторов существования и обратных импликаций. Вычисление кванторов всеобщности заменено вычислением отрицания кванторов существования. Излагаются побочные эффекты и пути их преодоления. Для немонотонных вычислений реляционный компьютер использует 4-х значную логику.
Третья часть статьи посвящена проблеме слов в полугруппах.
Вводится порядок в полугруппах. Для полугрупп с несколькими определяющими отношениями, любой класс эквивалентности представлен упорядоченной последовательностью подмножеств.
Полугруппы с одним определяющим отношением исследованы в деталях. Показано, что проблема слов разрешима в полугруппах с одним определяющим отношением, если левая часть этого отношения не является самопересекаемой (то есть не имеет одинакового начала и конца).

<\a>Логика высокого порядка.    М.А.Малков . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
Логика второго порядка представлена синтаксическими и табличными средствами. Эта логика отличается от логики первого порядка только присутствием кванторов для переменных, значениями которых являются теории и отношения.

Логика второго порядка предназначена для построения теорий второго порядка и моделей этих теорий. Одна из теорий второго порядка есть логика первого порядка. Эта статья посвящена в основном построению логики первого порядка средствами логики второго порядка. Есть два пути такого построения, один синтаксический, и другой табличный (или в виде отношений).
Синтаксический путь основан на алфавите, буквы которого используются для построения формул в теориях. Есть алфавит для теорий первого порядка и алфавит для теорий второго порядка. Оба алфавита бесконечны и содержат символы сортов.
Сорт есть специальное отношение, интерпретируемое как множество значений соответствующих переменных. Переменная интерпретируется как произвольный элемент этого множества.
Формулы логики второго порядка используют оба алфавита. Для отличия букв этих алфавитов, мы помещаем точку над буквами второго алфавита. Эта точка может отсутствовать только в специально оговоренных случаях.
Построение логики второго порядка немного отличается от построения логики первого порядка. Ос-новное различие касается явных и неявных кванторов второго порядка, в частности, кванторов на множестве отношений первого порядка. В остальном, теории второго порядка подобны теориям первого порядка.
Табличный путь построения теории не имеет ничего общего с синтаксическим путем. Нет никакого алфавита и синтаксиса предложений в этом алфавите. Таблицы состоят из строк и столбцов, элементы таблиц (на пересечении строк и столбцов) есть натуральные числа. В таблицах нет логических символов и разделителей. Все формулы представлены в бесскобочной записи. Поэтому, структура таблиц для теорий первого и второго порядков полностью совпадает. Различие только в имени таблиц. Это различие подобно различию двух алфавитов в синтаксическом варианте, когда буквы алфавитов отмечены или не отмечены точкой над ними.

<\a>Функциональное расширение C++. II.    М.А.Малков . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
Представлен новый язык ^fC++. Этот язык есть функциональное расширение C++. Каждый оператор такого C++ должен иметь значение, возможно, пустое. Добавлен такой новый тип переменных, что значения этих переменных есть типы. Предлагается новая техника автоматического распределения памяти.

Эта статья является продолжением статьи предыдущего номера журнала.
Использование меток строго ограничено. Только break может ссылаться на метки, и эти метки должны быть расположены после break. Помеченные операторы должны быть в одном блоке с break или немедленно после блока, который содержит break или после вызова функции с break в теле этой функции. Таким образом, break реализует произвольное прерывание, в том числе исключения, и программы остаются структурными. Но метки могут быть функциями, и это позволяет передавать информацию при прерываниях. Кроме того, метки могут образовывать множества.
Новый спецификатор var позволяет использовать числа неограниченной длины. Длина данных со спецификатором var переменная: некоторые байты определяют длину данных в байтах, другие байты содержат сами данные.
Типы rational, real и complex представлены для вычислительной алгебры.
Предлагается автоматическое распределение любых структур памяти .
Если объект есть таблица, то специальная переменная добавляется в первом индексе при декларации. Эта переменная всегда равняется числу строк в таблице. Перед инициализацией эта переменная имеет значение 0. Максимальное значение первого индекса может быть указано или нет. Если максимальное значение не указано, то это значение подсчитывается автоматически при первой инициализации. Но в обоих случаях фактическое значение может быть больше максимального. Используя информацию относительно скорости заполнения памяти, компьютер может предсказать реальный объем необходимой памяти и затребовать дополнительную память более реального объема.
Такие структуры не нуждаются ни в каком указателе. В частности, символьная строка должна быть определена как массив символов, то есть, как таблица с одним индексом.
Последовательность операторов тоже имеет значение. Если последовательность заключена в круглые скобки, то значение этой последовательности есть значение последнего оператора. Но круглые скобки перегружены, и есть исключения этого правила. Если последовательность заключена в фигурные скобки, то значение этой последовательности есть последовательность значений каждого оператора.
Если последовательность операторов содержит точку с запятой как разделитель, то эти операторы выполняются строго в их последовательности. Если последовательность операторов содержит запятую как разделитель, то эти операторы выполняются в произвольной последовательности. Это может использоваться для параллельных вычислений.
Предлагается новый тип type для переменных, значения которых сами являются типами.
Тип Report помещен в стандартную библиотеку. Этот тип предназначен для быстрого составления отчета на основе запроса.

<\a>Искусственный интеллект и доказательство теорем    М.А.Малков . . . . . . . . . . . . . . . . . . . . . . 79
Проблемы искусственного интеллекта рассматриваются на примере автоматизированного доказательства теорем.

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

<\a>Автоматичиское доказательство теорем и логическое моделирование   С.В.Попов . . . . . . 91
Логические формулы заменяются программами и поиск доказательств сводится к построению фиксированных точек этих программ. Это означает, что используется операционная семантика вместо синтаксических преобразований.

Описываются несколько подходов к проблеме автоматизации доказательства теорем. Предпринимается попытка выделить различные концепции, возникшие в этом направлении, и сформулировать типичные для каждой из них трудности. Так как проблематика автоматизированного принятия решений является традиционной для искусственного интеллекта, то такой анализ существующих подходов имеет не только теоретическое, но и прикладное значение.
Наиболее традиционный подход в автоматизации доказательств есть синтаксический. Для целей автоматического доказательства использовались различные логические исчисления, правила вывода которых напоминают своим видом содержательные умозаключения. В статье описывается такое исчисление, правила которого легко поддаются содержательной интерпретации. Это исчисление позволяет описать вид вывода, близкий по своей форме к содержательным умозаключениям.
На его примере демонстрируется главная трудность, которую приходится преодолевать при автоматизации рассуждений. Она состоит в том, что формальные средства, какими бы естественными с точки зрения содержательных рассуждений они не казались, всегда позволяют получить большое число формул, не поддающихся однозначной содержательной интерпретации. Типичным примером является формула "из лжи следует все, что угодно", которая верна в классической логике, но в содержательных рассуждениях используется лишь при определенных условиях.
В статье приводится описание некоторого числа стратегий, которые демонстрируются соответствующими примерами.
Как противопоставление синтаксическому подходу при автоматизации доказательств в статье сформулирована семантическая концепция решения той же проблемы. Суть ее состоит в следующем. Каждая задача формулируется в понятийном базисе той предметной области, которой она принадлежит, и поэтому представляет собой логическую формулу, устанавливающую связь между этими понятиями. Если задача имеет решение, то она обладает логической моделью, в которой решение представимо совокупностью отношений (т.е. базисных понятий). Построение такой модели осуществляется с помощью так называемой операционной семантики для логических формул. Последняя формулируется следующим образом. Каждая формула первого порядка при определенной трактовке может выступать в качестве программы для построения своей собственной модели с конечным носителем. Другими словами, каждая формула обладает наряду с логической семантикой и операционной семантикой. Операционная семантика обладает свойством полноты: каждая неподвижная точка формулы как программы есть ее же логическая модель, и с другой стороны, каждая логическая модель формулы есть неподвижная точка программы, построенной по этой формуле.
В результате, преобразовав формулу, которая есть формулировка исходной задачи, в программу, получаем средство решения этой задачи. Но в силу универсальности этот метод обладает всеми недостатками, которые имеются у синтаксических методов, - т.е. большой перебор при нахождении неподвижных точек. Для преодоления этой трудности предлагается не традиционный подход использования разнообразных стратегий поиска, а несколько иной. Он базируется на том, что полученное решение интерпретируется в понятиях предметной области, т.е. является содержательно осмысленным. Поэтому для описания задач предложен формальный язык, достаточно богатый, чтобы описывать сложные задачи, но обладающий конструкциями, естественными с точки зрения содержательных умозаключений. Этот язык описывается в статье, и для него доказывается полнота операционной семантики относительно логической.
Приводится описание реализации системы логического моделирования в виде системы двухуровневого программирования. Первый уровень - логический, служит для описания предметной области, второй - управляющий, используется для формулировки стратегий поиска. Оба уровня реализованы в виде языков программирования, первый - логического, второй - операторного, который служит метаязыком по отношению к первому. Для представления о возможностях системы приводится программа и решение хорошо известной задачи "О восьми ферзях".