Как выразить отношение между предикатами в логике первого порядка?

@nbd · Регистрация: 17.07.2014

Author24 — интернет-сервис помощи студентам

Здравствуйте,
изучаю известный доказыватель теорем 'E Prover', который работает с логикой первого порядка. Не могу понять возможно ли адаптировать к ЛПП (логике первого порядка) некоторые отношения между свойствами переменных, а не между переменными.

Например, имеем список людей. У каждого человека имеется несколько предикатов, один из предикатов, например, "Город проживания". И, имеется теорема, для доказательства которой необходимо использовать предикат "Земляки", смысл которого примерно такой:

Prolog

1	земляки(X,Y) :- город(X) == город(Y).

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

Prolog

1	земляки(X,Y) :- ( город(X, "Москва"), город(Y, "Москва") ) ; ( город(X, "Новгород"), город(Y, "Новгород") ) ; ... .

А имеется ли возможность выразить предикат "Земляки" без такого перечисления каждого города? (В Прологе, такое, кажется, возможно через использование функции apply. Но E prover, хотя может использовать сходный с Прологом синтакс, функции apply вроде бы не имеет.)

Спасибо.

@vchc · 03.03.2017, 15:17

Не совсем понятно в чём вопрос. Зачем вам выражать предикат "Земляки" через другие предикаты?
Отображение из предметной области в область определения ЛПП, то есть количество и смысл предикатов, определяется исключительно задачей которую вы решаете.

Если же вы спрашиваете как задать в E Prover сложный предикат, то читайте документацию на E Prover.

@nbd · 03.03.2017, 16:13 **[ТС]**

> Зачем вам выражать предикат "Земляки" через другие предикаты?

Не совсем понял вопрос. Смысл предиката "Земляки" и есть в том, чтобы оценивать, в данном случае проверять на равенство, другие предикаты: значения предиката "город" у предметных переменных. Предикат "земляки" получает две переменные (два представителя из списка людей) и возвращает "истина" если значения предиката "город" для них в базе знаний - одинаковые.

Попробую сформулировать вопрос с другим примером. Допустим, имеется предикат parity/1 возвращаюший "истина" если аргумент - четное число, и "ложь" - в противном случае. Нужно написать предикат sum_even/2, проверяющий четна ли сумма двух чисел. Сумма двух чисел x и y четна либо если оба числа четны, либо если оба числа нечетны. То есть если parity(x) == parity(y).

Псевдокод:

Prolog

1	sum_even(X,Y) :- equal(parity(X), parity(Y)).

Как правильно должен выглядеть предикат sum_even в ЛПП без расписывания отдельных специализаций для odd и even? :

Prolog

1	sum_even(X,Y) :- (even(X),even(Y)) ; (odd(X), odd(Y)).

@vchc · 03.03.2017, 16:42

Вы немного путаете ЛПП и средства, которые её реализуют.

В ЛПП предикат это функция, возвращающая 0 или 1 от некоторых переменных. Как вы её зададите уже не имеет отношения к ЛПП. Вы можете задать её на прологе, с++, .. или в самой ЛПП как формулу.

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

В вашем примере откуда взялся предикат parity? Вот оттуда же может взяться и предикат "земляки".

@nbd · 03.03.2017, 16:58 **[ТС]**

Сообщение от vchc

Вы можете задать её на прологе, с++, .. или в самой ЛПП как формулу.

Вот. Я именно об этом. Как может быть в ЛПП выражена формула sum_even? То есть, как может быть переведено в синтаксис ЛПП естественноязыковое высказывание:

для всех x, y, если parity x равна parity y, то сумма x и y четна.

@vchc · 03.03.2017, 17:34

Так же как и в прологе.

Sum_even(X,Y) := (parity(x) = parity(y)) или Sum_even(X,Y) := (not parity(x) and not parity(y)) or (parity(x) and parity(y)))

Все символы справа от := определены в ЛПП, значит формула корректна. Сам предикат parity уже подразумевает, что x принадлежит X - множеству на котором определ предикат parity. Я вам рекомендую ещё раз прочитать что такое ЛПП и как там задаются переменные, предикаты и формулы. Без понимания этого дальнейшая дейтельность эквивалентна методу тыка.

@nbd · 04.03.2017, 15:11 **[ТС]**

А нет ли кого-нибудь на форуме, кто использует TPTP язык? Так как fof формулы (first-order formules) этого языка - практически точное отображение ЛПП, то все что можно сказать про синтаксис ЛПП, можно относить и к этому языку.

Вот это рабочий код (успешно работает в E prover) для вышеозначенной задачи определения четности суммы двух слагаемых :

Код

fof(sum,axiom, ( ! [X,Y] : ( 
	( ( is(X,odd) & is(Y,odd) ) | ( is(X,even) & is(Y,even) ) ) <=> 
	sum_even(X,Y) ) ) ).
fof(prove_even, conjecture, ( (is(a,odd) & is(b,odd) ) => sum_even(a,b) )).

Не знает ли кто-нибудь можно ли в этом коде реализовать проверку четности суммы без специализации для каждого случая? То есть выразить sum_even не как

Код

( is(X,odd) & is(Y,odd) ) | ( is(X,even) & is(Y,even) )

а что-то вроде

Код

parity(X) = parity(Y)

(В мануале для языка такие вопросы отдельно не описываются, т.к. синтаксис fof формул это фактически синтаксис ЛПП.)

@NO_ · 07.03.2017, 01:36

город(X) это не предикат, а функция, возвращая значение города,
а предикат это как бы функция, выдающая только истину/ложь, он только проверяет состоят ли аргументы в нужном отношении
правильный предикат может быть например проживает(X,Y)
тогда земляки(X,Y) :- проживает(X,G), проживает(Y,G).
он унифицируется когда найдется такое значение G, при котором выполняются оба предиката проживает()
если такое G находится решателем, оно потом теряется, а предикат земляки тоже выдает только истину

предикаты над предикатами это уже логика 2 порядка, для неё нет решателя

Добавлено через 7 минут
в Прологе город(X) означает, что X является городом

@~~oopguru~~ · 13.03.2017, 22:32

Странно, что кто-то ковыряется с логическим программированием и испытывает затруднения в решении задач, которые средствами ООП решаются более чем тривиально

Зачем это все вообще?

@NO_ · 15.03.2017, 03:16

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

@~~oopguru~~ · 15.03.2017, 03:35

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

@NO_ · 15.03.2017, 04:52

Только что говорил, что всё такое решается на ООП более чем тривиально,
а теперь, что если бы было всё так просто, бы бы в раю жили.
Сам с собой поссорился?

@~~oopguru~~ · 15.03.2017, 13:39

NO_, я сакзал, что конкретно та задача, которую озвучил ТС, на ООП решается более чем тривиально. Потому, я выразил недоумение по поводу того, что для логического языка тут возникают какие то трудности. Мне именно вот это интересно.

Сообщение от NO_

Сам с собой поссорился?

Я вообще не понял, к чему Вы это сказали

@NO_ 120 / 40 / 9 Регистрация: 29.10.2016 Сообщений: 243
	15.03.2017, 03:16	10
	Для математики. Программы нужны не только чтобы нарисованные танчики обменивались выстрелами. А ещё и чтобы управлять атомными электростанциями, поездами и кораблями где ошибка может стоит жизнь тысячам людей, спутниками, которые работают в миллионах километров от Земли, создавать новые лекарства, просчитывать реальную войну с настоящими танками и морем реальной крови, выполнять межбанковские платежи на триллионы долларов в день. 0

@NO_ 120 / 40 / 9 Регистрация: 29.10.2016 Сообщений: 243
	15.03.2017, 04:52	12
	Только что говорил, что всё такое решается на ООП более чем тривиально, а теперь, что если бы было всё так просто, бы бы в раю жили. Сам с собой поссорился? 0

Новые блоги и статьи
Введение в модели и алгоритмы машинного обучения InfoMaster 12.01.2025 Машинное обучение представляет собой одну из наиболее динамично развивающихся областей искусственного интеллекта, которая фокусируется на разработке алгоритмов и методов, позволяющих компьютерам. . .	Как на Python создать нейросеть для решения задач InfoMaster 12.01.2025 В контексте стремительного развития современных технологий особое внимание уделяется таким инструментам, как нейросети. Эти структуры, вдохновленные биологическими нейронными сетями, используются для. . .	Как создать нейросеть для генерации картинок на Python InfoMaster 12.01.2025 Генерация изображений с помощью искусственных нейронных сетей стала одним из наиболее захватывающих направлений в области компьютерного зрения и машинного обучения. В этой статье мы рассмотрим. . .	Создание нейросети для генерации текста на Python InfoMaster 12.01.2025 Нейросети, или искусственные нейронные сети, представляют собой модели машинного обучения, вдохновленные работой человеческого мозга. Они состоят из множества взаимосвязанных узлов, или "нейронов",. . .	Как создать нейросеть распознавания изображений на Python InfoMaster 12.01.2025 Введение в распознавание изображений с помощью нейросетей Распознавание изображений с помощью нейронных сетей стало одним из самых впечатляющих достижений в области искусственного интеллекта. Эта. . .	Основы искуственного интеллекта InfoMaster 12.01.2025 Искусственный интеллект (ИИ) представляет собой одну из наиболее динамично развивающихся областей современной науки и технологий. В широком смысле под искусственным интеллектом понимается способность. . .
Python и нейросети InfoMaster 12.01.2025 Искусственные нейронные сети стали неотъемлемой частью современных технологий, революционизировав множество областей - от медицинской диагностики до автономных транспортных средств. Python, благодаря. . .	Python в машинном обучении InfoMaster 12.01.2025 Python стал неотъемлемой частью современного машинного обучения, завоевав позицию ведущего языка программирования в этой области. Его популярность обусловлена несколькими ключевыми факторами, которые. . .	Создание UI на Python с TKinter InfoMaster 12.01.2025 TKinter — это одна из наиболее популярных библиотек для создания графических интерфейсов пользователей (GUI) в языке программирования Python. TKinter входит в стандартную библиотеку Python, что. . .	HTML5 в разработке мобильных приложений InfoMaster 12.01.2025 Введение: Обзор роли HTML5 в мобильной разработке В современном мире мобильных технологий HTML5 стал ключевым инструментом для разработки кроссплатформенных приложений. Эта технология произвела. . .	Как создавать приложения для iOS/iPhone InfoMaster 12.01.2025 Введение в разработку iOS-приложений Разработка приложений для iOS открывает огромные возможности в мире мобильных технологий. С каждым годом количество пользователей iPhone и iPad растет,. . .	Как использовать Kotlin в Android разработке InfoMaster 12.01.2025 Язык программирования Kotlin, разработанный компанией JetBrains, стал неотъемлемой частью современного мира Android-разработки. Первоначально представленный в 2011 году, Kotlin был официально. . .

@vchc 28 / 28 / 5 Регистрация: 27.10.2015 Сообщений: 89
	03.03.2017, 15:17	2
	Не совсем понятно в чём вопрос. Зачем вам выражать предикат "Земляки" через другие предикаты? Отображение из предметной области в область определения ЛПП, то есть количество и смысл предикатов, определяется исключительно задачей которую вы решаете. Если же вы спрашиваете как задать в E Prover сложный предикат, то читайте документацию на E Prover. 0

@vchc 28 / 28 / 5 Регистрация: 27.10.2015 Сообщений: 89
	03.03.2017, 16:42	4
	Вы немного путаете ЛПП и средства, которые её реализуют. В ЛПП предикат это функция, возвращающая 0 или 1 от некоторых переменных. Как вы её зададите уже не имеет отношения к ЛПП. Вы можете задать её на прологе, с++, .. или в самой ЛПП как формулу. Способ задания определяется тем средством реализации ЛПП, которое вы используете и вашими потребностями и задачами. Если у вас есть задача выразить один предикат через другие предикаты средствами ЛПП, то это обычная задача программирования. Читайте документацию на средство реализации ЛПП и делайте. Некоторые предикаты могут быть невыразимы через уже имеющиеся в рамках ЛПП (выразимость определяется не ЛПП, а предметной областью задачи). Тогда они задаются не формулой ЛПП, а каким-либо внешним описанием (на другом языке). В вашем примере откуда взялся предикат parity? Вот оттуда же может взяться и предикат "земляки". 0

@nbd 9 / 9 / 0 Регистрация: 17.07.2014 Сообщений: 163
	03.03.2017, 16:58 [ТС]	5
	Сообщение от vchc Вы можете задать её на прологе, с++, .. или в самой ЛПП как формулу. Вот. Я именно об этом. Как может быть в ЛПП выражена формула sum_even? То есть, как может быть переведено в синтаксис ЛПП естественноязыковое высказывание: для всех x, y, если parity x равна parity y, то сумма x и y четна. 0

@vchc 28 / 28 / 5 Регистрация: 27.10.2015 Сообщений: 89
	03.03.2017, 17:34	6
	Так же как и в прологе. Sum_even(X,Y) := (parity(x) = parity(y)) или Sum_even(X,Y) := (not parity(x) and not parity(y)) or (parity(x) and parity(y))) Все символы справа от := определены в ЛПП, значит формула корректна. Сам предикат parity уже подразумевает, что x принадлежит X - множеству на котором определ предикат parity. Я вам рекомендую ещё раз прочитать что такое ЛПП и как там задаются переменные, предикаты и формулы. Без понимания этого дальнейшая дейтельность эквивалентна методу тыка. 0

@nbd 9 / 9 / 0 Регистрация: 17.07.2014 Сообщений: 163
	04.03.2017, 15:11 [ТС]	7
	А нет ли кого-нибудь на форуме, кто использует TPTP язык? Так как fof формулы (first-order formules) этого языка - практически точное отображение ЛПП, то все что можно сказать про синтаксис ЛПП, можно относить и к этому языку. Вот это рабочий код (успешно работает в E prover) для вышеозначенной задачи определения четности суммы двух слагаемых : Код fof(sum,axiom, ( ! [X,Y] : ( ( ( is(X,odd) & is(Y,odd) ) \| ( is(X,even) & is(Y,even) ) ) <=> sum_even(X,Y) ) ) ). fof(prove_even, conjecture, ( (is(a,odd) & is(b,odd) ) => sum_even(a,b) )). Не знает ли кто-нибудь можно ли в этом коде реализовать проверку четности суммы без специализации для каждого случая? То есть выразить sum_even не как Код ( is(X,odd) & is(Y,odd) ) \| ( is(X,even) & is(Y,even) ) а что-то вроде Код parity(X) = parity(Y) (В мануале для языка такие вопросы отдельно не описываются, т.к. синтаксис fof формул это фактически синтаксис ЛПП.) 0

@NO_ 120 / 40 / 9 Регистрация: 29.10.2016 Сообщений: 243
	07.03.2017, 01:36	8
	город(X) это не предикат, а функция, возвращая значение города, а предикат это как бы функция, выдающая только истину/ложь, он только проверяет состоят ли аргументы в нужном отношении правильный предикат может быть например проживает(X,Y) тогда земляки(X,Y) :- проживает(X,G), проживает(Y,G). он унифицируется когда найдется такое значение G, при котором выполняются оба предиката проживает() если такое G находится решателем, оно потом теряется, а предикат земляки тоже выдает только истину предикаты над предикатами это уже логика 2 порядка, для неё нет решателя Добавлено через 7 минут в Прологе город(X) означает, что X является городом 0

@~~oopguru~~ Заблокирован
	13.03.2017, 22:32	9
	Странно, что кто-то ковыряется с логическим программированием и испытывает затруднения в решении задач, которые средствами ООП решаются более чем тривиально Зачем это все вообще? 0

@~~oopguru~~ Заблокирован
	15.03.2017, 03:35	11
	NO_, можно подумать, что математика в этих задачах может как то помочь, lol типа, абстрактных коней в вакууме погонял, и атомные станции перестали взрываться. ну-ну. Если бы было все так просто, бы бы в раю жили. Математиков все больше с каждым годом, и спутники все чаще падают. 0

@~~oopguru~~ Заблокирован
	15.03.2017, 13:39	13
	NO_, я сакзал, что конкретно та задача, которую озвучил ТС, на ООП решается более чем тривиально. Потому, я выразил недоумение по поводу того, что для логического языка тут возникают какие то трудности. Мне именно вот это интересно. Сообщение от NO_ Сам с собой поссорился? Я вообще не понял, к чему Вы это сказали 0

Опции темы