9 / 9 / 0
Регистрация: 17.07.2014
Сообщений: 163
1

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

03.03.2017, 04:57. Показов 817. Ответов 12
Метки нет (Все метки)

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

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

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

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

Спасибо.
0
Programming
Эксперт
94731 / 64177 / 26122
Регистрация: 12.04.2006
Сообщений: 116,782
03.03.2017, 04:57
Ответы с готовыми решениями:

Выразить формулу второго порядка через формулу первого порядка
Здравствуйте, для автоматического доказывателя теорем E Prover нужно сформулировать логическую...

Докажите что отношение делимости на множестве натуральных чисел есть отношение нестрогого порядка
Докажите что отношение делимости на множестве натуральных чисел есть отношение нестрогого порядка.

Отношение эквивалентности, отношение частичного, строгого, линейного порядка,
Помогите пожалуйста решить! На множестве M={1,3,4,8} задано отношение R =...

Отношение эквивалентности, отношение частичного, строгого, линейного порядка,
Помогите пожалуйста решить! На множестве M={3,5,6,8} задано отношение R =...

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

Если же вы спрашиваете как задать в E Prover сложный предикат, то читайте документацию на E Prover.
0
9 / 9 / 0
Регистрация: 17.07.2014
Сообщений: 163
03.03.2017, 16:13  [ТС] 3
> Зачем вам выражать предикат "Земляки" через другие предикаты?

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

Попробую сформулировать вопрос с другим примером. Допустим, имеется предикат 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)).
0
28 / 28 / 5
Регистрация: 27.10.2015
Сообщений: 89
03.03.2017, 16:42 4
Вы немного путаете ЛПП и средства, которые её реализуют.

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

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

В вашем примере откуда взялся предикат parity? Вот оттуда же может взяться и предикат "земляки".
0
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
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
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
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
Заблокирован
13.03.2017, 22:32 9
Странно, что кто-то ковыряется с логическим программированием и испытывает затруднения в решении задач, которые средствами ООП решаются более чем тривиально Зачем это все вообще?
0
120 / 40 / 9
Регистрация: 29.10.2016
Сообщений: 243
15.03.2017, 03:16 10
Для математики.
Программы нужны не только чтобы нарисованные танчики обменивались выстрелами. А ещё и чтобы управлять атомными электростанциями, поездами и кораблями где ошибка может стоит жизнь тысячам людей, спутниками, которые работают в миллионах километров от Земли, создавать новые лекарства, просчитывать реальную войну с настоящими танками и морем реальной крови, выполнять межбанковские платежи на триллионы долларов в день.
0
Заблокирован
15.03.2017, 03:35 11
NO_, можно подумать, что математика в этих задачах может как то помочь, lol
типа, абстрактных коней в вакууме погонял, и атомные станции перестали взрываться. ну-ну.
Если бы было все так просто, бы бы в раю жили. Математиков все больше с каждым годом, и спутники все чаще падают.
0
120 / 40 / 9
Регистрация: 29.10.2016
Сообщений: 243
15.03.2017, 04:52 12
Только что говорил, что всё такое решается на ООП более чем тривиально,
а теперь, что если бы было всё так просто, бы бы в раю жили.
Сам с собой поссорился?
0
Заблокирован
15.03.2017, 13:39 13
NO_, я сакзал, что конкретно та задача, которую озвучил ТС, на ООП решается более чем тривиально. Потому, я выразил недоумение по поводу того, что для логического языка тут возникают какие то трудности. Мне именно вот это интересно.
Цитата Сообщение от NO_ Посмотреть сообщение
Сам с собой поссорился?
Я вообще не понял, к чему Вы это сказали
0
IT_Exp
Эксперт
87844 / 49110 / 22898
Регистрация: 17.06.2006
Сообщений: 92,604
15.03.2017, 13:39
Помогаю со студенческими работами здесь

Найти расстояние между главными максимумами первого порядка
Помогите пожалуйста с задачей: Свет с длиной волны λ = 0,60 мкм падает нормально на дифракционную...

Свести дифференциальное уравнение 4-го порядка к системе из 4 уравнений первого порядка
Вот уравнение: y''''+a1*y'''+a2*y''+a3*Y'+a4*y=А*sin(ω*t+Φ) a1-a4 - переменные вот какая...

Дифференцированное уравнение второго порядка представить в виде системы уравнений первого порядка
Как представить это уравнение x'' - (\lambda + k{x}^{2}-{x}^{4})*x'+x = 0 в систему уравнений...

Приведение диффура 2 порядка к системе уравнений первого порядка
Дано уравнение второго порядка x'' + x = 1 +e^t, нужно привести к системе уравнений первого...

Уравнение первого порядка, и два уравнения второго порядка
помогите пожалуйста решить 3 уравнения 1)y'*ctg(x)+y=2 (y(0)=1) 2) x2*y''+x*y'+1=0 3)...

Отношение Порядка
Ребят,кто разбиреться в дискретной,решите пожалуйста.. :) Заранее спасибо :) Задание: На...


Искать еще темы с ответами

Или воспользуйтесь поиском по форуму:
13
Ответ Создать тему
Опции темы

КиберФорум - форум программистов, компьютерный форум, программирование
Powered by vBulletin
Copyright ©2000 - 2024, CyberForum.ru