Проверка тавтологии для GNU Prolog

Я ищу реализации проверок тавтологии с открытым исходным кодом, написанных на GNU Prolog (реализация для SWI-Prolog также приемлема, но GNU Prolog предпочтительнее).

Я хотел бы скормить ввод программы с помощью таких запросов:

A and (B or C) iff (A or B) and (A or C).

или же

3^2 * (X + 2) == (9 * X) + 18.

конечно, обозначения могут быть разными, например:

(3 power 2) mul (X plus 2) equals (9 mul X) plus 18.

В результате я ожидаю логического ответа, такого как "Да / Нет", "Равно / Разное", "Доказано, найдено / Не удалось найти, доказать" или аналогичного.

Я нашел средство проверки тавтологии для GNU-Prolog на ftp://ftp.cs.yorku.ca/pub/peter/SVT/GNU/, но лицензия не прикреплена и не знаю, как применять арифметические ограничения Gnu Prolog и возможности арифметики для того, чтобы расширить только логическую модель с арифметикой.

  • Какие-нибудь другие схожие решения?
  • Некоторые примеры того, как арифметические возможности могут быть использованы для расширения модели.

Спасибо, Грег.

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

PPS Как заметил @larsmans, в соответствии с теоремами Гёделя о неполноте невозможно доказать "все" формулы. Вот почему я ищу что-то, что доказывает то, что может быть доказано из данного набора аксиом и правил, так как я ищу программу Gnu Prolog, я ищу примеры таких наборов аксиом и правил;). Конечно, проверка может дать сбой - я ожидаю, что она будет работать в "некоторых" случаях:). - С другой стороны, есть теорема Гёделя о полноте;).

Источник

3 ответа

Решение

Если вам нужен расширяемый инструмент для доказательства теорем в Прологе, посмотрите семейство инструментов для доказательства теорем Lean, основным представителем которых является leanCOP; он обрабатывает классическую логику первого порядка в 555 байтах Пролога.

Версия 1.0 - это следующая программа:

prove(M,I) :- append(Q,[C|R],M), \+member(-_,C),
 append(Q,R,S), prove([!],[[-!|C]|S],[],I).
prove([],_,_,_).
prove([L|C],M,P,I) :- (-N=L; -L=N) -> (member(N,P);
 append(Q,[D|R],M), copy_term(D,E), append(A,[N|B],E),
 append(A,B,F), (D==E -> append(R,Q,S); length(P,K), K<I,
 append(R,[D|Q],S)), prove(F,S,[L|P],I)), prove(C,M,P,I).

Веб-сайт leanCOP имеет более удобочитаемые версии с большим количеством функций. Вы должны будете реализовать равенство и арифметику самостоятельно.

Источник

Я нашел несколько проверок тавтологии в " Математической логике для информатики" Бен-Ари, Мордехай, к сожалению, они охватывают булеву логику. Какое преимущество, его реализации в Прологе, и представляют различные подходы, связанные с автоматическим доказательством, или решение таких уравнений (или, автоматически проверяя доказательства).

Источник

Вы можете использовать программирование логики ограничений для вашей задачи. Равенство дает вам непосредственно результат (например, GNU Prolog):

?- X*X #= 4.
X = 2

Для неравенства вам, как правило, нужно попросить систему генерировать экземпляры после того, как ограничения были установлены. Обычно это делается с помощью директивы по маркировке (например, GNU Prolog):

?- 27 * (X + 2) #\= (9 * X) + 18.
X = _#22(0..14913080)
?- 27 * (X + 2) #\= (9 * X) + 18, fd_labeling(X).
X = 0 ? ;
X = 1 ? ;
X = 2 ? ;
Etc..

Список, который показывает, какие прологи имеют какой тип CLP, можно найти здесь. Просто проверьте мультиколонку CLP.

Обзор систем Prolog, Ульрих Ноймеркель

до свидания

Источник
Другие вопросы по тегам