доказательство теоремы с доказательством 9 - противоречивый результат - PullRequest
Новая
       7

доказательство теоремы с доказательством 9 - противоречивый результат

0 голосов
/ 14 октября 2018

Я использую prover9 для доказательства теорем первого порядка с интерфейсом nltk python.

Я получаю разные результаты для двух эквивалентных формул (без предположений):
Пусть p1: 

-exists x0.(-exists x3 x1.(R0(x3,x0) & R0(x1,x1)) & exists x1 x2.(R0(x1,x2) & R0(x1,x0)))

И p2: 

-exists x3.(-exists x0 x2.(R0(x2,x2) & R0(x0,x3)) & exists x1 x0.(R0(x1,x0) & R0(x1,x3)))

Использование следующего Pythonкод: 

import nltk as nk
read_expr = nk.sem.Expression.fromstring

prove_command1 = nk.Prover9Command(goal=read_expr(p1),timeout=20, prover=nk.Prover9())
prove_command2 = nk.Prover9Command(goal=read_expr(p2),timeout=20, prover=nk.Prover9())
print(prove_command1.prove()) # False
print(prove_command2.prove()) # True

Теперь странно то, что когда я печатаю доказательство для каждого из них, цель эквивалентна в обоих: 

-(exists x (-(exists y exists z (R0(y,x) & R0(z,z))) & (exists z exists u (R0(z,u) & R0(z,x))))).

Правильный ответ для p1 иp2 Неверно, и я не понимаю, как это возможно, что два выражения переведены в одну и ту же цель, но ответ различен.

любой совет?

...