Unterschied zwischen Logikprogrammierung und automatisiertem Theorembeweis

Question

Was ist der Unterschied zwischen Logikprogrammierung und automatisiertem Theorembeweis (ATP) (z. B. mit E-Prover, Spass oder Princess)?

Ich suchte viel und die einzige Information, die ich fand, ist, dass ATP der Vorläufer der Logikprogrammierung ist. Aber ich sehe den Unterschied nicht. Aber ich denke, es ist mehr als die Syntax.

Answer 1

Was der Prolog Teil der Frage betrifft, so wurde dies gesagt am besten durch Richard O'Keefe:

Prolog eine effiziente Programmiersprache ist, weil es eine dumm Theorembeweisers ist.

So gibt es eine Verbindung zwischen Prolog und Theorem beweisen. Prolog hat einige Merkmale eines Theorembeweisers, zum Beispiel sucht es nach Beweisen oder besser Auflösung Widerlegungen, aber es tut so in einer unvollständigen Weise, die mehr auf eine allgemeine Programmiersprache zugeschnitten ist.

Natürlich macht die vergleichsweise enge Affinität zwischen Prolog und Theorembeweiser Prolog zu einer ausgezeichneten Wahl implementieren Sie mehr vollwertige Theorem Provers.

Tatsächlich ist es vergleichsweise einfach, die unvollständige Standardausführungsstrategie von Prolog zu ergänzen und zu erweitern, so dass die Suche vollständiger wird.

Beachten Sie, dass Prolog auch einige extra logische Merkmale aufweist, die nicht in den Geltungsbereich des Theorembeweises fallen und dem deklarativen Denken oft im Wege stehen können. Siehe auch logical-purity.