a clause (a disjunction of literals) with at most one positive literal. Horn clause
~q v ~p v ~t v u.
this is equiv to:
(q v p v t) -> u.
to show **u**, show **q**, **p**, and **t**.
% in Prolog this is roughly.
% u if we can prove q and p and t.
u :- q,p,t.
a \= b. does’t unify.
a = b. % no, two atoms have to be the same to unify.
A = a. % yes, a variable can unify with a literal so A = a.
f(A) = B, g(B) = C.
B = f(A)
C = g(f(A))
| ?- f(A) = B, g(B) = C, A=ab.
A = ab
B = f(ab)
C = g(f(ab))
predicate.consequent :- antecedent.
% X is a carnivore if X eats Y and Y is meat
carnivore(X) :- eats(X,Y),meat(Y).
[a,b,c] = [X|Y]. % does this unify?
% X = ?
% Y = ?
;; in Lisp member looks like
(defun member (item list)
(cond
((null list) nil)
((eql item (car list)) list)
(t (member item (cdr list)))))
% X is a member of the list if it matches the head of the list
% OR if X is a member of the rest of the list.
member(X,[X|Y]).
member(X,[B|Y]) :- member(X,Y).
member(X,[X|Y]).
member(X,[B|Y]) :- member(X,Y).
% don't really care about Y in first line or B in second.
% so... don't clutter definition with variables that don't matter!
member(X,[X|_]).
member(X,[_|Y]) :- member(X,Y).
% these definitions are the same.
gprolog
eatsother(X) :- eats(X,Y),\+meat(Y).