Многосортная логика кратко

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

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

Существуют различные способы формализации вышеупомянутого намерения; многосортная логика — это любой пакет информации, который его реализует. В большинстве случаев приводятся следующие варианты:

• набор видов, S
• соответствующее обобщение понятия сигнатуры , позволяющее обрабатывать дополнительную информацию, поступающую с сортировками.

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

Рассуждая о биологических организмах, полезно различать два вида и . В то время как функция имеет смысл, подобная функция Обычно нет. Многосортная логика допускает такие термины, как , но отказаться от терминов типа как синтаксически неправильно сформированное.

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

Пример иерархии сортировки

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

собака⊆плотоядное животное ,

собака⊆млекопитающее ,

плотоядное животное⊆животное ,

млекопитающее⊆животное ,

животное⊆организ м,

растение⊆организ м,

и т. Об этом говорит сайт https://intellect.icu . д.; см. рисунок.

Везде, где используется какой-либо терминстребуется, термин любого подвидасВместо этого можно использовать принцип подстановки Лисков . Например, если функция объявлена , и постоянное объявление , термин )совершенно допустимо и имеет вид Чтобы предоставить информацию о том, что мать собаки, в свою очередь, тоже собака, необходимо сделать еще одно заявление. может быть выдан; это называется перегрузкой функций , аналогично перегрузке в языках программирования .

Логику сортировки по порядку можно перевести в несортированную логику, используя унарный предикатп для каждого сортася, и аксиома для каждого объявления подсортировки Обратный подход оказался успешным в автоматизированном доказательстве теорем: в 1985 году Кристоф Вальтер смог решить тогдашнюю эталонную задачу, переведя ее в логику с упорядоченной сортировкой, тем самым снизив ее на порядок, поскольку многие унарные предикаты превратились в сортировки.

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

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

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

• Категорическая логика
• Логика первого порядка § Многосортная логика
• категорическая логика ,

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