nat(0). nat(s(X)) :- nat(X). ?- nat(0). yes ?- nat(s(0)). yes ?- nat(s(s(s(s(0))))). yes ?- nat(X). X = 0 ->; X = s(0) ->; X = s(s(0)) ->; X = s(s(s(0))) ->; X = s(s(s(s(0)))) -> X = s(s(s(s(s(0))))) ->; X = s(s(s(s(s(s(0)))))) ->; X = s(s(s(s(s(s(s(0))))))) ->; X = s(s(s(s(s(s(s(s(0)))))))) ->; X = s(s(s(s(s(s(s(s(s(0))))))))) ->; X = s(s(s(s(s(s(s(s(s(s(0)))))))))) -> ...Με βάση τον ορισμό αυτό μπορούμε να ορίσουμε μια σχέση διάταξης:
less(0, X) :- nat(X). less(s(X), s(Y)) :- less(X, Y). ?- less(s(0), 0). no ?- less(s(0), s(s(0))). yes ?- less(X, s(s(s(s(0))))). X = 0 ->; X = s(0) ->; X = s(s(0)) ->; X = s(s(s(0))) ->; X = s(s(s(s(0)))) ->; noΜε παρόμοιο τρόπο μπορούμε να ορίσουμε και την πρόσθεση:
plus(0, X, X) :- nat(X). plus(s(X), Y, s(Z)) :- plus(X, Y, Z).Είναι αξιοσημείωτο πως το κατηγόρημα της πρόσθεσης με τη μορφή που έχει οριστεί μπορεί να υπολογίσει άθροισμα, διαφορά, όρους που δημιουργούν ένα άθροισμα, ή να ελέγξει αν ένα άθροισμα είναι αληθές:
?- plus(s(0), s(0), X). X = s(s(0)) yes ?- plus(s(0), X, s(s(s(0)))). X = s(s(0)) yes ?- plus(X, Y, s(s(0))). X = 0 Y = s(s(0)) ->; X = s(0) Y = s(0) ->; X = s(s(0)) Y = 0 ->; no ?- plus(s(0), 0, 0). noΜε τη χρήση του αθροίσματος μπορούμε να ορίσουμε και το γινόμενο:
times(0, X, 0) times(s(X), Y, Z) :- times(X, Y, W), plus(W, Y, Z).Το κατηγόρημα για το γινόμενο που έχει οριστεί με τον τρόπο αυτό έχει και αυτό παρόμοια ευελιξία:
?- times(s(s(0)), s(s(s(0))), X). X = s(s(s(s(s(s(0)))))) yes ?- times(X, s(s(0)), s(s(s(s(0))))). X = s(s(0)) ->. yes ?- times(X, Y, s(s(s(s(0))))). X = s(0) Y = s(s(s(s(0)))) ->; X = s(s(0)) Y = s(s(0)) ->; ?- times(s(0), s(0), s(0)). yes
?- is(X, 1 + 2). X = 3 ?- is(2, 1 + 1). yes ?- is(Y, 3 * 8 + 4 / 5). Y = 24.8 yes ?- is(2, X + X). no