Herbrand in Prolog

Question

Stavo osservando alcuni problemi come Logica fuzzy logic e le clausole di Horn e ho visto alcuni semplici esempi di applicazioni, con Prolog.

La ragione di questa domanda è perché questi problemi sono anche tra i Herbrand teorema che considero un po 'più complicato di altri, almeno per me, e ho avuto difficoltà a trovare un esempio di applicazione relative al Prolog.

è per questo che ho voluto fornirmi qualche esempi applicativi utilizzando Prolog, non tanto quella di base (a causa che genera il modello di Herbrand, secondo la definizione, sono le regole di base e trovare sempre questo esempio di applicazione quando si ricerca su Herbrand), per uso esclusivo Herbrand. Grazie

Questo è un esempio di codice applicativo in Prolog:

p(f(X)):- q(g(X)). 
p(f(X)):- p(X). 
p(a). 
q(b). 

Answer 1

Un insieme di clausole ha un modello se e solo se ha un modello di Herbrand.

Per dimostrare che la clausola C è una conseguenza di clausole Cs, mostrano semplicemente che Cs ∪ ~C è insoddisfacibile.

Questo è, in termini astratti, che cosa fa Prolog, tramite un caso speciale di risoluzione: Si può considerare l'esecuzione di una (puro — quello   altro) programma Prolog come il motore Prolog   cercando di trovare a risoluzione   confutazione della query   negata.

La forma di risoluzione che implementa Prolog, SLD   risoluzionecon profondità prima ricerca, non garantisce però che tutte le clausole insoddisfacibile vengono smentite, è   incompleta.

In Prolog, le proprietà procedurali possono influire sulla derivazione delle conseguenze. Ad esempio, con il vostro programma:

 
?- p(X). 
wating... 

Mentre noi semplicemente riordinare le clausole come:

 
q(b). 
p(a). 
p(f(X)):- q(g(X)). 
p(f(X)):- p(X). 

otteniamo:

 
?- p(X). 
X = a ; 
X = f(a) ; 
X = f(f(a)) . 

Nota però che molte importanti proprietà dichiarative sono davvero conservati nel sottoinsieme puro e monotonico di   Prolog. Vedere logical-purity per ulteriori informazioni.