Vorrei formalizzare alcune conoscenze ed eseguire query in quello che può essere definito come completamente dichiarativo Horn logic (o Prologo pienamente dichiarativo). Qualcuno potrebbe fornire alcune linee guida su come implementarlo? Ricapitolerò brevemente la descrizione dettagliata dal link sopra:Come implementare la logica Horn pienamente dichiarativa?
Il linguaggio formale è quello di (il nucleo di) Prolog: un "programma" è un insieme di regole e fatti come in Prolog (incluse funzioni e variabili e in sostanza, contenente solo predicati definiti dall'utente).
Contrariamente a Prolog, tuttavia, sto cercando un'implementazione che sia solida e completa rispetto alla semantica dichiarativa standard dei programmi di logica --- il meno modello di Herbrand (vale a dire, l'insieme di termini di base definiti induttivamente) . Nel lavoro teorico sulla programmazione logica questo è di solito l'oggetto di studio, ed è noto che una risposta valida e completa alle domande può essere raggiunta (nel senso "ricorsivamente enumerabile"), ad esempio usando la risoluzione SLD soggetta a le seguenti condizioni:
- fiera ricerca di regole di corrispondenza (ad esempio, ricerca in profondità di Prolog è non fiera);
- unificazione con "verifica-verifica" (verifica che una variabile non si verifichi in un termine con cui è unificata).
Sto cercando un'implementazione concisa che si basi sulle funzionalità esistenti, piuttosto che sull'invenzione della ruota. Due delle direzioni più promettenti che vedo lo stanno implementando come meta-interprete di Prolog, o come parte di qualche dimostratore di teoremi. Qualcuno con conoscenze pratiche in questi domini può fornire alcune linee guida su come implementarlo? Può essere facilmente implementato in miniKanren?
Le mie intenzioni sono di formalizzare una certa conoscenza in maniera completamente dichiarativa. Le caratteristiche cruciali di tale formalizzazione sono che corrisponde esattamente alla nozione matematica di induzione (monotona), così che la conoscenza e le sue proprietà possono essere facilmente ragionate con argomenti induttivi.
Le domande che ci chiedono di consigliare o trovare un libro, uno strumento, una libreria di software, un'esercitazione o altre risorse fuori sede sono off-topic per Stack Overflow in quanto tendono ad attirare risposte e spam. – Enigmativity
Non sto cercando un'opinione. Sto chiedendo aiuto per trovare qualcosa che non sono riuscito a trovare, o alcune linee guida su come farlo da solo (diciamo, in [miniKanren] (http://minikanren.org/)). – amka00
@ amka00 - Questa è la parte "trova una" del mio commento. – Enigmativity