5

Prolog の実装について述べている SATCHMO 定理証明者に関するかなりの数の論文を見てきました。しかし、私がこれまでに見つけた唯一のソース コードの実装は本にあり、それは非常に限られており、ルールがどのように評価され、起動されるかの例を示すことのみを目的としていました。Prolog で SATCHMO の優れたオープン ソース実装を見た人はいますか?

Satchmo と呼ばれる Django 用の Python 言語ツールについて言及しているのではないことに注意してください。タグに Satchmo を含めなかったのは、そのタグの主要な定義として Stack Overflow が示しているものだからです。

4

2 に答える 2

6

Satchmoに関する最初の論文（上記の「テーマのバリエーション」にも記載されています）は

レイナー・マンタイとフランソワ・ブライ。SATCHMO：Prologに実装された定理証明者。自動控除に関する第9回国際会議の議事録、415〜434ページ。Springer-Verlag、1988年。

このペーパーでは、SatchmoのいくつかのProlog実装を紹介し、それらのメリットについて説明します。また、いくつかの例を示します。これは、私がAttemptoControlledEnglishの推論RACEの開始点として使用したSatchmoバージョンです。

:- 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.
于 2012-02-08T17:25:10.627 に答える
4

1か月前に修士論文のために集めたすべての論文をゴミ箱に放り込んだとき、いつか後悔するだろうとどういうわけか知っていました. 私の論文は、SATCHMO を制約付きで拡張することに関するものだったので、SATCHMO に関するさまざまな実装を示す論文がいくつかありました...

とにかく、ここから始めるのが良いでしょう: Software Collection of the Lehr- und Forschungseinheit für Programmier- und Modellierungssprachen, LMU Munich . 教授の 1 人である Francois Bry は、SATCHMO の開発者の 1 人であり、彼のユニットは SATCHMO をさまざまな方向に拡張するためにかなりの作業を行いました。Compiling SATCHMO を見てください。PMS インスティテュートの人々は、コードを学業以外の目的で使用できるかどうかを明確にする必要があります。アカデミックな仕事なら問題ないはずです。

SATCHMO (すでに数年前のものですが) のすべての概要については、次の参考文献を使用できます: Variations on a Theme

于 2012-02-08T07:22:57.803 に答える