Ваша «вторая аксиома ... только для того, чтобы сделать списки неупорядоченными» выглядит подозрительно.
Примечание [x,y] является двухэлементным списком. Итак, ваша аксиома вообще ничего не говорит о списках. Ваши «сложные» примеры по-прежнему представляют собой 2-элементные списки. Так что не очень сложно. Я думаю, что вы не сможете доказать member(A, [C, B, A])
Контраст [x:y] в вашей первой аксиоме - это список из 1 или более элементов. y может быть nil или может быть любым количеством элементов. IOW y - это список, тогда как в [x,y], y является элементом списка.
См. http://www.cs.unm.edu/~mccune/prover9/manual/2009-11A/, 'Статьи & Формулы' в 'списке обозначений'.
я бы:
member(x, [x:y]).
member(x, z) -> member(x, [y:z]).
(Но что определяет мешок, а не множество.)
Я думаю, что квантификация переменных является отвлекающим маневром.
Редактировать: Errk. Я не прав. Так что я не знаю, почему я получил этот результат:
Пример, который указывает на @Doug не нужно Quant z «внутри» ОРЗ эквивалентности. Вы можете просто удалить всю явную количественную оценку , и доказательство все еще работает.
OK. Применим правила перезаписи согласно «Правилам» & «Формулы» в «Если введены неклассические формулы ...».
Это определение подмножества является эквивалентностью (aka bi-implication); переписать как две отдельные аксиомы: «вперед» и «назад»; переписывайте каждый из них, используя p -> q ==>-p | q.
В направлении «упреждающих» мы получаем:
-subset(x, y) | (member(z, x) -> member(z, y)).
Не имеет значения, является ли z количественно узкий или широкий.
В «обратном» направлении:
-(member(z, x) -> member(z, y)) | subset(x, y).
Вот если мы количественно z узко вокруг импликации, что внутри сферы отрицания; и так отличается от количественной оценки по всей формуле.
Вывод: оба определения member() и subset() являются неправильными.
BTW Вы уверены, что вам нужно определить member? Доказательство @Doug указывает на простоту member(x,y) как примитивный.
Я не знаком с Prover9, но если это похоже на логический язык, то член '(z, x) -> (z, y)' истинен, если z не является членом x. Ваше подмножество rule * (x, y) <-> (член (z, x) -> member (z, y)) 'может быть интерпретировано как« подмножество (x, y) тогда и только тогда, когда существует az такое, что член (z , x) -> member (z, y) "вместо того, что вы намеревались:" subset (x, y) тогда и только тогда, когда для всех z, member (z, x) -> member (z, y) ". –
hmm ... Я понимаю, что член (z, y) был бы истинным, если z не является членом x (поскольку False влечет за собой что-либо), но почему вы говорите, что весь член 'member (z, x) -> член (z, y) 'был бы правдой? – Ziofil
Я не знаю, обрабатывает ли prover9 несвязанные переменные с правой стороны как универсальные или экзистенциальные. Если он рассматривает их как экзистенциальные, то это может объяснить вашу проблему. –