patrick/anthem-rs
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Add prime number example

Browse Source
This commit is contained in:
Patrick Lühne 2020-05-19 12:57:09 +02:00
parent 86d2857494
commit d88ac89b01
Signed by: patrick
GPG Key ID: 05F3611E97A70ABF
2 changed files with 22 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
examples/example-prime.lp Normal file
View File

@ -0,0 +1,3 @@
% Prime numbers from 1 to n.
composite(N) :- N = 1..n, I = 2..(N - 1), N \ I = 0.
prime(N) :- N = 2..n, not composite(N).

19
examples/example-prime.spec Normal file
View File

@ -0,0 +1,19 @@
input: n -> integer.
output: prime/1.
assume: n >= 1.
axiom: forall N1, N2, N3 (N1 > N2 and N3 > 0 -> N1 * N3 > N2 * N3).
lemma: forall N N + 0 = N.
lemma: forall I, J, N (I * J = N and I > 0 and N > 0 -> J > 0).
lemma(backward): forall X1 (composite(X1) <- (exists N1, N10 (X1 = N1 and 1 <= N1 and N1 <= n and 2 <= N10 and N10 <= N1 - 1 and exists N11 (N1 = (N10 * N11) and 0 < N11)))).
lemma(backward): forall N (composite(N) -> (exists N10 (1 <= N and N <= n and 2 <= N10 and N10 <= N - 1 and exists N11 (N = (N10 * N11) and 0 < N11)))).
lemma: forall X1 (composite(X1) <-> (exists N1, N10 (X1 = N1 and 1 <= N1 and N1 <= n and 2 <= N10 and N10 <= N1 - 1 and exists N11 (N1 = (N10 * N11) and 0 < N11)))).
assert: forall X (composite(X) -> p__is_integer__(X)).
assert: forall N (composite(N) <-> N > 1 and N <= n and exists I, J (I > 1 and J > 1 and I * J = N)).
assert: forall X (prime(X) -> p__is_integer__(X)).
assert: forall N (prime(N) <-> N > 1 and N <= n and not exists I, J (I > 1 and J > 1 and I * J = N)).