I came across this natural number evaluation of logical numbers in a tutorial and it's been giving me some headache: natural_number(0). natural_number(s(N)) :- natural_number(N). The rule roughl...

Lets assume there is pure_2 Prolog with dif/2 and pure_1 Prolog without dif/2. Can we realize Peano apartness for values, i.e. Peano numbers, without using dif/2? Thus lets assume we have Peano apa...

The following Prolog program defines a predicate fact/2 for computing the factorial of an integer in successor arithmetics: fact(0, s(0)). fact(s(X), Y) :- fact(X, Z), prod(s(X), Z, Y). prod(0, ...

There are two possible rules for addition in Prolog, with different termination properties according to cTI: cTI reports sum(A,B,C)terminates_if b(A);b(C). for the following rule: sum(0, Y, Y). s...

This less-than predicate in Peano arithmetic less(0, s(_)). less(s(X), s(Y)) :- less(X, Y). loops when ?- less(X, Y), X=s(0), Y=0. Is there a better way to write less/2 (using Horn clauses only)?...

I have the following Lemma with an incomplete proof: Lemma s_is_plus_one : forall n:nat, S n = n + 1. Proof. intros. reflexivity. Qed. This proof fails with Unable to unify "n + 1" wit...

As a basic Prolog exercise, I set myself the task of writing a binary tree height predicate that would work forwards and "backwards" - that is, as well as determining the height of a known binary t...

suppose the following program: nat(0). nat(s(N)) :- nat(N). /* 0+b=b */ plus(0,B,B) :- nat(B). /* (a+1)+b = c iff a+(b+1)=c */ plus(s(A),B,C) :- plus(A,s(B),C). it works great for adding two nu...

I'm trying to write reversible relations in "pure" Prolog (no is, cut, or similar stuff. Yes it's homework), and I must admit I don't have a clue how. I don't see any process to create such a thing...

To grok green cuts in Prolog I am trying to add them to the standard definition of sum in successor arithmetics (see predicate plus in What's the SLD tree for this query?). The idea is to "clean up...

Let's consider the following Prolog program (from "The Art of Prolog"): natural_number(0). natural_number(s(X)) :- natural_number(X). plus(X, 0, X) :- natural_number(X). plus(X, s(Y), s(Z)) :- pl...

I'm doing a very simple exercise in Prolog and there's something I don't understand in the trace. The program is a "greater than" (>) on integers represented as successors: greater_than(succ(_)...

I start to learn Prolog and first learnt about the successor notation. And this is where I find out about writing Peano axioms in Prolog. See page 12 of the PDF: sum(0, M, M). sum(s(N), M, s(K))...

I need to create a Prolog predicate for power of 2, with the natural numbers. Natural numbers are: 0, s(0), s(s(0)) ans so on.. For example: ?- pow2(s(0),P). P = s(s(0)); false. ?- pow2(P,s(s(0))...

I have been trying to learn Prolog, and am totally stumped on what the predicate s() does. I see it used often and there is so little resources on the internet about Prolog that I cannot find an an...

I have the next rules % Signature: natural_number(N)/1 % Purpose: N is a natural number. natural_number(0). natural_number(s(X)) :- natural_number(X). ackermann(0, N, s(N)). % rule 1 ackermann(s...