Кто-нибудь видел хорошую реализацию Пролога с открытым исходным кодом для доказательства теоремы SATCHMO?

Question

Я видел довольно много работ по проверке теорем SATCHMO, в которых говорится о реализации Пролога.Но единственная реализация исходного кода, которую я нашел до сих пор, была в книге, и она была действительно ограниченной и предназначалась только для того, чтобы дать пример того, как правила оценивались и выполнялись.Кто-нибудь видел хорошую реализацию SATCHMO с открытым исходным кодом в Прологе?

Обратите внимание, я не имею в виду инструмент языка Python для Django под названием Satchmo, поэтому я не включил Satchmo в теги, поскольку именно поэтомуПереполнение стека отображается как доминирующее определение для этого тега.

Answer 1

Первая статья о Satchmo (также перечисленная в упомянутых выше «Вариациях на тему»):

Райнер Манти и Франсуа Брай. SATCHMO: доказатель теоремы, реализованный в Прологе. В материалах 9-й Международной конференции по автоматическому удержанию, стр. 415–434. Springer-Verlag, 1988.

В статье представлено несколько реализаций Satchmo на Прологе и обсуждены их достоинства. Также приведены некоторые примеры. Вот версия Satchmo, которую я использовал в качестве отправной точки моего рассуждения RACE для контролируемого английского языка Attempto:

:- op(1200, xfx, '--->').
:- unknown(_, fail).

satisfiable :-
  setof(Clause, violated_instance(Clause), Clauses),
  !,
  satisfy_all(Clauses),
  satisfiable.
satisfiable.

violated_instance((B ---> H)) :-
  (B ---> H),
  B,
  \+ H.

satisfy_all([]).

satisfy_all([(_B ---> H) | RestClauses]) :-
  H,
  !,
  satisfy_all(RestClauses).
satisfy_all([(_B ---> H) | RestClauses]) :-
  satisfy(H),
  satisfy_all(RestClauses).

/*
satisfy((A,B)) :-
  !,
  satisfy(A),
  satisfy(B).  
*/

satisfy((A;B)) :-
  !,
  (satisfy(A) ; satisfy(B)).  

satisfy(Atom) :-
  \+ Atom = untrue,
  (
    predicate_property(Atom, built_in)
    ->
    call(Atom)
  ;
    assume(Atom)
  ).

assume(Atom) :-
%  nl, write(['Asserting  ': Atom]),
  asserta(Atom).

assume(Atom) :-
%  nl, write(['Retracting ': Atom]),
  retract(Atom),
  !,
  fail.         

Answer 2

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

В любом случае, хороший момент для начала будет здесь: Сборник программ Lehr- undForschungseinheit für Programmier- и Modellierungssprachen, LMU Munich .Один из профессоров, Франсуа Брай, был одним из разработчиков SATCHMO, и его подразделение проделало немалую работу по расширению его в разных направлениях.Посмотрите на компиляцию SATCHMO.Сотрудники института PMS должны уточнить, можно ли использовать код для неакадемической работы.Для академической работы это не должно быть проблемой.

Для обзора всех вещей SATCHMO (хотя уже несколько лет), вы можете использовать эту библиографию: Вариации на тему