Доказательство того, что H пересекает K — подгруппу в Прологе (H и K — подгруппы)

Я разрабатываю доказательство теории групп. Сейчас меня интересует доказательство того, что если H и K — подгруппы, то H пересекает K — подгруппу. Я основываю свое доказательство на построении отношения (==H) такого, что

h (==H) g тогда и только тогда, когда hg^{-1} принадлежит H. Доказательство того, что это отношение эквивалентности (рефлексивное, симметричное, транзитивное), эквивалентно доказательству того, что H является подгруппой.

Я сделал следующий код, и когда я пытаюсь доказать, что H пересекает K, это подгруппа, я терплю неудачу. Я новичок в Прологе, поэтому, возможно, я ошибаюсь в чем-то основном. В математическом доказательстве не требуется указывать явный вид отношения эквивалентности, поэтому я его опустил.

В программе я обозначаю hg и kg как H и K. H пересекает K и равен hkg.

inside(X,H) :- equals(H,X,e).



equals(hkg,e,e).
equals(hkg,x,e).
equals(hkg,y,e).
equals(hkg,z,e).
equals(hkg,X,Y) :- equals(hg,X,Y),equals(kg,X,Y).


reflexive(H) :- forall(inside(X,H),equals(H,X,X)).


symmetric(H) :- forall(equals(H,X,Y),equals(H,Y,X)).


transitive(H) :- forall(equals(H,X,Y),equals(H,Y,Z),equals(H,X,Z)).


subgroup(H) :- reflexive(H),symmetric(H),transitive(H).
subgroup(hg).
subgroup(kg).

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


prolog equivalence-classes finite-group-theory
person Cezar98    schedule 06.04.2020    source источник
comment
Эти 2 рекурсивных вызова ... :- equals(hg,X,Y),equals(kg,X,Y). обречены на неудачу, поскольку не существует факта, «помеченного» hg или kg. Я недостаточно понимаю ваши обозначения, чтобы предложить лучший подход, извините.   -  person CapelliC    schedule 06.04.2020
comment
Действительно, когда я его отслеживаю, вызов equals(hg,x,x) не выполняется. Разве «:-» не означает тогда и только тогда, когда в этом случае? Если да, то почему программа не пытается доказать равенство (hg, x, x) и просто сдается, потому что не видит этого отношения?   -  person Cezar98    schedule 06.04.2020
comment
Если бы это была моя проблема, я бы использовал Coq. См.: Библиотека Coq.Classes.Equivalence   -  person Guy Coder    schedule 06.04.2020
comment
Насколько я понимаю, Coq — это помощник по доказательствам, который проверяет правильность вашего доказательства. Это не генерирует ваше доказательство. Меня интересует генерация доказательств подгрупп с использованием отношения эквивалентности. Я просто вставляю отношение эквивалентности (равно), и программа должна сгенерировать для меня доказательство, если оно правильное.   -  person Cezar98    schedule 06.04.2020
comment
@ Cezar98 Cezar98 AFAIK, Coq помогает вам построить доказательство в интерактивном режиме, избавив вас от утомительной работы с деталями. Он также сильно отличается от Пролога, так как основан на конструктивном исчислении, о котором я мало что знаю, кроме того, что он основан на иерархиях типов из теории типов Мартина-Лёфа (т.е. он использует другой подход из теории множеств Цермело-Френкеля для множества до математики). Нет, это действительно не для меня. Может быть в другой жизни.   -  person David Tonhofer    schedule 06.04.2020
comment
И есть ли версия The Little Prover на Prolog, а не на Scheme/Racket? , который о доказательстве теоремы о вашем программном обеспечении. Если нет, то почему бы и нет!   -  person David Tonhofer    schedule 06.04.2020

Ответы (1)


arrow_upward
1
arrow_downward

Пролог не так уж хорош для доказательства теорем. То, как он вызывает предикаты в логической программе, основано на доказательстве резольвентной теоремы (и, таким образом, ограничено предложениями Хорна), но это не означает, что язык позволяет вам особенно хорошо моделировать задачи и методы доказательства теорем. В частности, потому, что Пролог работает с целями p(X,Y), для которых он пытается найти кортежи (x,y), которые делают эти цели ИСТИННЫМИ, как определено логической программой, а не работает с предложениями S, которые переписываются в соответствии с каким-либо дедуктивным подходом (естественная дедукция, последовательное исчисление) для некоторую логику (классическую, интуитивистскую и т. д.), пока не будет получено окончательное S'. Обратите внимание, в частности, что квантификаторов нигде не видно, потому что никто не пишет S, которым они могут понадобиться. Это не означает, что на Прологе нельзя построить средство доказательства теорем, но это можно сделать.

В этом случае для

reflexive(H) :- forall(inside(X,H),equals(H,X,X)).

у вас уже проблемы, потому что проверка Пролога reflexive(hg) означает

На самом деле идите и найдите любое X такое, что inside(X,hg)

inside(X,hg) :- equals(hg,X,e).

На самом деле идите и найдите любое X такое, что equals(hg,X,e)

потому что мне нужно убедиться, что inside(X,hg) (и оператор ∀X: equals(hg,X,e) =›inside(X,hg) позволит мне это сделать)

... и их нет в этой логической программе.

Рефлексивность должна быть бессодержательно истинной

?- reflexive(hg).
true.

Красиво, но бесполезно.

person David Tonhofer    schedule 06.04.2020