Что дает метод резолюции?

Ну машинам не слишком очевидно, они нуждаются в наборах формальных правил вывода. Это тебе не круги рисовать.

isTasty = function(apple){apple.hasProperty(red)}

Но это неправда. Неизвестно, существуют ли некрасные вкусные яблоки. Если это непонятно, надо идти учить логику.

Это известно из определения. Если это не известно, никакая логика не поможет, задача неразрешима.

Таки нужно идти учить логику.

Из определения известно что красное яблоко вкусное. Но ничего не сказано о желтом яблоке, а оно тоже может быть вкусным.

выяснять что-либо о вкусе желтого яблока не требуется

На мой взгляд, это доказывается тривиальнейшим образом, методом простой дедукции.

Только когда предикатов мало. А, например, при разработке ПЛИС тривиальнейшим образом могут возникать логические «ашипки», как следствие перехода количества в качество.

Да, но функция, которую ты привёл, неверная.

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

На макфак?

высказывания - это частный случай предикатов. они просто могут быть не определены на всём пространстве. а так принципиально особой разницы нет.

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

не можешь привести пример, только максимально простой?

Пример чего? Таблицы истинности? Или резолюции?

таблицы истинности

Для высказываний?

да

фигня это всё...

Неужели в АИ где-то применяется алгебра предикатов, это же чисто топовая греческая наука, типа Аристотеля. Вспомни топики в инете, в которых бот на основе нейросетей побеждает всех опытных игроков в 3D шутере. Где будут скоро многие классические методы AI? Только в старых книжках, вот где. Не, конечно останутся многие крутые вещи - рекурсия, прямой перебор с проверкой результата, работа с подстановками и сочетаниями, много чего ещё останется что наш нейронный разум (и вероятнее всего и компьютерный электро нейронный тоже) делает хуже чем формализованные системы типа алгебры ЯВУ, классической алгебры с дискретизацией простанства-времени, комбинаторики. Но в основном все будет крутится вокруг нейротехники и классических алгебр, подчеркну алгебр.

А то что там в википедии в доказательстве это не алгебра а Евклид с Аристотелем вместе, раз нету формализации и формального доказательства (а его нету, там вместо формул «представим»,«подумаем»,«возьмём» и «очевидно») то следовательно это и не алгебра. Это ещё Галуа ловко доказал на своих группах и началах абстрактной алгебры. Только тогда это была во многом такая-же болтовня, а сейчас четкий формализм. Ну и уточню что такое формализм,в современной компьютерной машинерии это когда мы дискретизируем некоторую систему отсчета (возможно из реального мира), производим расчёт, потом дискретизируем обратно - ну или в формате зеленых буковок из матрицы оставляем кому как удобнее. Тут вроде все понятно - преобразование через устройства ввода-вывода/предварительные мысленные преобразования/сенсоры. Вот с расчетом хитрее, дело в том что наши ЯВУ(Языки программирования Высокого Уровня) это уже есть конечные доказанные и корректные алгебры, мы прямо в терминах и вражениях этих алгебр и пишем. Но многие задачи решены или решаются в других алгебрах. Соотвественно сооружение программы становится таким:

1. Дискретизация системы отсчета во внешнюю, некомпьютерную алгебру

2. Решение задачи в этой алгебре

3. Дискретизация решения обратно в исходную систему отсчета

4. Перевод конструкций внешней алгебры из пункта 2 в алгебру ЯВУ

5. Тестирование программы из пункта 4, с известными входными и выходными значениями алгебры из пункта 2 (Это я к примеру, меня так учили...)

6. Тестирование программы из пункта 4 на реальных дискретизированных значениях исходной системы отсчета, если не работает ищем баг или в программе из пункта 4, или в решении из пункта 2, или проверяем корректность перевода из алгебры пункта 2 в алгебру ЯВУ

7. Запуск готовой программы в продакшн.

Как ты можешь видеть, мы просто соорудили переход из какой-то математической алгебры в алгебру ЯВУ, и в этой алгебре реализовали аналогичное решение задачи.

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

Это я всё к чему - там в доказательстве одна болтовня, если сможешь формализовать то ты крут, и я подару тебе свою завалявшуюся книжку метафизики Аристотеля, я в ней нифига не понял, а ты значит его поймёшь. Но если ты не охватываешь мыслью доказательства из википедии - то стоит подумать сто раз перед тем как пытаться выучить этот пласт огромной математической культуры, которая от Аристотеля Евклида и Пифагора пришла, многому у них научилась и говорит похоже на них.Просто есть куда других математических методов для построения ИИ, в том числе нейронные сети, а их как известно Бог создал.

математические нейросети имеют весьма далекое отношение к биологическим, если вообще что-то имеют, кроме названия.

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

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

Сама формула логики высказываний есть ФАЛ от скольких-то переменных, где каждое элементарное высказывание - переменная. Это синтаксическая структура, которая вообще не знает ни о каких яблоках. Есть только то, что есть в самом высказывании.

Неизвестно даже что такое красность красноты :) Но ващет, это не важно — никто не мешает притвориться что есть и априори понятно — и плясать от «если А, то B», не вдаваясь в филосопливость кви про кво.

Логика высказываний не предоставляет средств для записывания «красности» яблок. Здесь бы лучше подошли предикаты.

А я что сказал? С т.з. логики неинтересна истинность А и Б :) Предикаты — это чтоб твой собеседник не включил тупари и не встал на ручник «да схуяли А истинно?»