gistfile1.pl

write_siki(X) :-
  atomic(X), write(X).
write_siki(X+Y) :-
  write_siki(X), write(' と '),
  write_siki(Y), write(' との和').
write_siki(X*Y) :-
  write_siki(X), write(' と '),
  write_siki(Y), write(' との積').

d(x, 1).
d(Y, 0) :- atomic(Y), Y \== x.
d(Y+Z, DY+DZ) :- d(Y, DY), d(Z, DZ).
d(Y^N, N*Y^N1*DY) :- integer(N), N1 is N-1, d(Y, DY).
d(Y-Z, DY-DZ) :- d(Y, DY), d(Z, DZ).
d(Y*Z, DY*Z+Y*DZ) :- d(Y, DY), d(Z, DZ).
d(sin(Y), cos(Y)*DY) :- d(Y, DY).
d(cos(Y), -sin(Y)*DY) :- d(Y, DY).

canbe_t(t) :- !.
canbe_t(A /\ B) :- canbe_t(A), canbe_t(B).
canbe_t(A \/ B) :- canbe_t(A); canbe_t(B).
canbe_t(-A) :- canbe_f(A).
canbe_t((A -> B)) :- canbe_f(A); canbe_t(B).

canbe_f(f) :- !.
canbe_f(A /\ B) :- canbe_t(A); canbe_t(B).
canbe_f(A \/ B) :- canbe_t(A), canbe_t(B).
canbe_f(-A) :- canbe_t(A).
canbe_f((A -> B)) :- canbe_t(A), canbe_f(B).