Ich möchte etwas Wissen formalisieren und führen Sie Abfragen in was bezeichnet als vollständig deklarative Horn logic (oder vollständig deklarative Prolog). Könnte jemand einige Richtlinien zur Umsetzung geben? Ich fasse kurz die schöne Beschreibung von dem Link oben zusammen:Wie implementiert man vollständig deklarative Horn Logik?
Die formale Sprache ist die von (der Kern von) Prolog: ein "Programm" ist eine Reihe von Regeln und Fakten wie in Prolog (einschließlich Funktionen und Variablen und im Grunde, enthält nur benutzerdefinierte Prädikate).
Im Gegensatz zu Prolog bin ich jedoch auf der Suche nach einer Implementierung, die solide und vollständig in Bezug auf die Standard-deklarative Semantik von Logikprogrammen ist - das geringste Herbrand-Modell (dh die induktiv definierte Menge von Grundbegriffen) . In der theoretischen Arbeit zur Logikprogrammierung ist dies in der Regel Gegenstand des Studiums, und es ist bekannt, dass eine fundierte und vollständige Antwort auf Abfragen (im "rekursiv aufzählbaren" Sinn), beispielsweise unter Verwendung von SLD-Auflösung, erhalten werden kann die folgenden Bedingungen:
- Messe Suche nach Regeln passend (zB Prolog der Tiefensuche ist nicht fair);
- Vereinheitlichung mit "auftritt-check" (Überprüfung, dass eine Variable nicht in einem Begriff auftritt, mit dem es vereinheitlicht ist).
Ich bin auf der Suche nach einer prägnanten Implementierung, die auf vorhandenen Fähigkeiten aufbauen würde, anstatt das Rad zu erfinden. Zwei der vielversprechendsten Richtungen, die ich sehe, sind die Implementierung als Meta-Interpreter von Prolog oder als Teil eines Theorembeweisers. Könnte jemand mit praktischen Kenntnissen in diesen Bereichen eine Anleitung zur Umsetzung geben? Kann es leicht in miniKanren implementiert werden?
Meine Absichten sind einige Kenntnisse in einem vollständig deklarative Weise zu formalisieren. Das entscheidende Merkmal einer solchen Formalisierung ist, dass sie genau dem mathematischen Begriff der (monotonen) Induktion entspricht, so dass das Wissen und seine Eigenschaften leicht mit induktiven Argumenten begründet werden können.
Fragen fragen uns, zu empfehlen oder ein Buch, Werkzeug, Software-Bibliothek, Tutorial oder andere Off-Site-Ressource sind Wegthema für Stack-Überlauf zu finden, da sie opinionated Antworten und Spam zu gewinnen neigen. – Enigmativity
Ich bin nicht auf der Suche nach einer Meinung. Ich bitte um Hilfe, um etwas zu finden, das ich nicht gefunden habe, oder einige Richtlinien, wie ich es selbst machen könnte (zB in [miniKanren] (http://minikanren.org/)). – amka00
@ amka00 - Das ist der "finde einen" Teil meines Kommentars. – Enigmativity