risoluzione Axiom

Question

cerco di capire come funziona la risoluzione assioma in Prolog.

Supponiamo che io definisco le due operazioni di base sui numeri naturali:

• s (termine) (acronimo di successore) e

• add (termine, anotherTerm).

La semantica di add è dato da

• add (0, x1) -> x1

• add (x1, 0) -> x1

• add (s (x1), y1) -> S (add (x1, y1))

Poi, vorrei risolvere l'equazione

add (x, add (y, z)) = s (0)

immagino che una strategia potrebbe essere quella di

• test se il lato destro (RHS) dell'equazione è uguale alla sua sinistra (LHS)

• se non vedere se una soluzione possa essere trovare, cercando per la maggior unifier generale

• se non poi cercare di trovare un assioma che può essere utilizzato in questa equazione. Una strategia per fare questo lavoro potrebbe essere quella (per ogni assioma): cercare di risolvere il RHS dell'equazione è uguale al RHS dell'assioma. Se c'è una soluzione quindi provare a risolvere i LHS dell'equazione è uguale alle LHS del assioma. Se ci riesce, allora abbiamo trovato l'assioma destra.

• casualmente, se non esiste una soluzione e la LHS e RHS dell'equazione sono la stessa operazione (cioè stessa firma ma non stessi operandi), applicare l'algoritmo su ogni operando e una soluzione viene trovato se una soluzione è trovato per ogni operando.

Credo che questo (semplice) algoritmo può funzionare. Tuttavia, vorrei sapere se qualcuno ha esperienza risolvere questo tipo di problema? Qualcuno sa dove posso trovare qualche documentazione su un algoritmo migliore?

Grazie in anticipo

Answer 1

Quello che state cercando è chiamato restringimento . E 'implementato in alcune lingue funzionale-logic come Curry , ma non in Prolog stesso.

Answer 2

Un programma Prolog è un insieme di predicati.

Un predicato è una raccolta di clausole.

Una clausola ha la forma

Head :- Body.

che significa "Head è vero se Body è vero".

C'è una forma clausola di stenografia

Head.

che significa la stessa come

Head :- true.

dove true è un comando interno che è sempre vero.

Tornando alla parte Body di una clausola, Body è un obiettivo che può assumere una delle seguenti forme (A, B e C denotano obiettivi arbitrari):

Atom            % This is true if Atom is true (see below).
A, B            % This is true if A is true and B is true.
(A ; B)         % This is true if A is true or B is true.
\+ A            % This is true if A is not true.
(A -> B ; C)    % If A is true then B must be true, else C must be true.

Ci sono alcune regole speciali in materia di Prolog ordine di valutazione (da sinistra a destra) e "tagli" (che potare l'albero di ricerca), ma questo è dettaglio fine che va oltre lo scopo di questo breve tutorial.

Ora, per decidere se un Atom è vero, Atom può essere una delle seguenti forme (X e Y denotano termini arbitrari):

true                % or some other builtin with given truth rules.
X = Y               % True if X and Y are successfully unified.
p(X, Y, ...)        % True if p(X, Y, ...) matches the head of some clause
                    % and the Body is true.

Un termine è, essenzialmente, qualsiasi pezzo di sintassi.

La cosa fondamentale da individuare qui è che Prolog non ha funzioni! Dove in un linguaggio funzionale si potrebbe definire una funzione add(X, Y), che restituisce la somma di X e Y, in Prolog si definisce un predicato il cui capo è add(X, Y, Z) che, in caso di successo, unifica Z con il termine che denota la somma di X e Y.

Dato tutto questo, siamo in grado di definire le regole in Prolog come segue:

add(0, Y, Y).                        % 0 + Y = Y.
add(Y, 0, Y).                        % Y + 0 = Y.
add(s(X), Y, s(Z)) :- add(X, Y, Z).  % s(X) + Y = s(X + Y).

dove sto usando 0 per indicare zero (!) E s(X) per indicare il successore di X.

Si consideri la valutazione add(s(s(0)), s(0), Z):

add(s(s(0)), s(0), Z)                 % Only the third head for add matches, so...
---> Z = s(Z0), add(s(0), s(0), Z0).

add(s(0), s(0), Z0)                   % Only the third head for add matches, so...
---> Z0 = s(Z1), add(0, s(0), Z1).

add(0, s(0), Z1)                      % Only the first head for add matches, so...
---> Z1 = s(0).

Mettendo tutte queste unificazioni per Z insieme, abbiamo Z = s(s(s(0))).

Ora, si può chiedere "che cosa succede se le partite più di una testa in una clausola di" o "che cosa succede se un percorso di valutazione non riesce?", Alla quale le risposte sono "determinismo", "backtracking", e, in generale, , leggere un libro di testo Prolog!

Spero che questo aiuti.

Answer 3

"rappresentazione della conoscenza" di Brachmann e Levesque dà una discreta introduzione a come funzionano queste cose.