FOL, ZFC, NGB and Prolog

Hello,
I have finally grasped the dichotomy of the declarative (FOL, i.e.
math) and imperative (CS) knowledge, and concluded that e.g. Prolog is,
merely, FOL in executable notation. Having thought that, I made my
first steps towards what I thought to be "the easiest", i.e. Peano
axioms. Without ample skill in pattern matching to do the transcription
myself, I browsed the web and obtained:

number(zero).
number(X) :-
X = next(Y),
number(Y).


less(0, X):-X\=0.
less(X, next(X)).
less(X, Z) :-
Z = next(Y),
less(X, Y).
less(next(X),X):-fail.

(Dear me, one can formalize PM within that!)

http://www.csci.csusb.edu/***/cs320/prolog/peano.plg

Would someone be kind enough as to point me to a web resource
containing the transcription of ZFC, NGB (and maybe even Frege's
Grundlanden) into Prolog's syntax? Of course, there are the great
Metamath Proof Explorer and DCProof, still, I am only a beginner.

Thank You very much indeed.

Kindest regards,
Tom

.