# SPEC 7: search order, forward reasoning, bounds, halting and conclusions.

=== derived facts are tried before program clauses
spec: 7.1
args: program.py --goal "p(X)"
--- program.py
from peye import *
fact(p('source'))
fact(q)
implies(q, p('derived'))
--- stdout
p('derived')
p('source')

=== program clauses are tried in clause order
spec: 7.1
args: program.py --goal "p(X)"
--- program.py
from peye import *
fact(p(1))
implied_by(p(X), q(X))
fact(p(3))
fact(q(2))
--- stdout
p(1)
p(2)
p(3)

=== a forward rule's conclusions feed rules in later rounds
spec: 7.2
--- program.py
from peye import *
fact(a(1))
implies(b(X), c(X))
implies(a(X), b(X))
--- stdout
b(1)
c(1)

=== forward rules close over cycles
spec: 7.2
--- program.py
from peye import *
fact(edge('a', 'b'), edge('b', 'a'))
implies(edge(X, Y), path(X, Y))
implies(path(X, Y) & edge(Y, Z), path(X, Z))
--- stdout
path('a', 'b')
path('b', 'a')
path('a', 'a')
path('b', 'b')

=== a conclusion identical to a program fact is not derived again
spec: 7.2
--- program.py
from peye import *
fact(p(1))
implies(p(X), p(X))
--- stdout

=== an unbound head variable becomes a Skolem atom of its own per activation
spec: 7.2
args: --skolem-genid test program.py
--- program.py
from peye import *
fact(person('ann'), person('bob'))
implies(person(X), has_parent(X, Y))
implies(has_parent(X, P) & has_parent(Y, P) & not_identical(X, Y), siblings(X, Y))
--- stdout
has_parent('ann', 'https://eyereasoner.github.io/.well-known/genid/test#sk_0')
has_parent('bob', 'https://eyereasoner.github.io/.well-known/genid/test#sk_1')

=== activations giving the same head instance share their Skolem atoms
spec: 7.2
args: --skolem-genid test program.py
--- program.py
from peye import *
fact(p('a', 1), p('a', 2))
implies(p(X, Y), q(X, B))
--- stdout
q('a', 'https://eyereasoner.github.io/.well-known/genid/test#sk_0')

=== each rule has Skolem atoms of its own
spec: 7.2
args: --skolem-genid test program.py
--- program.py
from peye import *
fact(p('a', 1))
implies(p(X, Y), q(X, B))
implies(p(X, Y), q2(X, B))
--- stdout
q('a', 'https://eyereasoner.github.io/.well-known/genid/test#sk_0')
q2('a', 'https://eyereasoner.github.io/.well-known/genid/test#sk_1')

=== a rule that keeps meeting new activations exceeds the bound
spec: 7.2, 7.3
args: --max-iterations 10 program.py
exit: 1
stderr: prefix peye:
--- program.py
from peye import *
fact(person('ann'))
implies(person(X), has_parent(X, P) & person(P))
--- stdout

=== the same activation in a later round gets the same Skolem atoms
spec: 7.2
args: --skolem-genid test program.py
--- program.py
from peye import *
fact(person('ann'))
implies(person(X), has_parent(X, Y))
implies(has_parent(X, P), known(X))
--- stdout
has_parent('ann', 'https://eyereasoner.github.io/.well-known/genid/test#sk_0')
known('ann')

=== Skolem names are numbered by first occurrence and shared across heads
spec: 7.2
args: --skolem-genid test program.py
--- program.py
from peye import *
fact(person('ann'))
implies(person(X), r(X, Y, Z, Y) & s(Z))
--- stdout
r('ann', 'https://eyereasoner.github.io/.well-known/genid/test#sk_0', 'https://eyereasoner.github.io/.well-known/genid/test#sk_1', 'https://eyereasoner.github.io/.well-known/genid/test#sk_0')
s('https://eyereasoner.github.io/.well-known/genid/test#sk_1')

=== query reports each instance once
spec: 7.2, 7.6
--- program.py
from peye import *
fact(p(1), p(1), p(2))
query(p(X))
--- stdout
p(1)
p(2)

=== query reports in order of first report
spec: 7.6
--- program.py
from peye import *
fact(p(1), q(2))
query(q(X))
query(p(Y))
--- stdout
q(2)
p(1)

=== a query without answers concludes nothing
spec: 7.6
--- program.py
from peye import *
fact(p(1))
implies(p(X), q(X))
query(r(X))
--- stdout

=== Skolem atoms cannot clash with the program's atoms
spec: 7.2
args: --skolem-genid test program.py
--- program.py
from peye import *
fact(p('a'), knows('sk_0', 'x'))
implies(p(X), q(X, Y))
implies(q(X, Y) & knows(Y, Z), r(X, Z))
--- stdout
q('a', 'https://eyereasoner.github.io/.well-known/genid/test#sk_0')

=== without a genid, each run's Skolem atoms have a random one
spec: 7.2, 14
--- program.py
from peye import *
fact(p('a'))
implies(p(X), q(X, Y))
--- stdout
q('a', 'https://eyereasoner.github.io/.well-known/genid/…#sk_0')

=== query output replaces the derived facts
spec: 7.6
--- program.py
from peye import *
fact(p(1))
implies(p(X), q(X))
query(p(X))
--- stdout
p(1)

=== goals replace the program's own queries
spec: 7.2, 7.6
args: program.py --goal "q(Y)"
--- program.py
from peye import *
fact(p(1))
implies(p(X), q(X))
query(p(X))
--- stdout
q(1)

=== several goals are answered in turn
spec: 7.4
args: program.py --goal "q(X)" --goal "p(X)"
--- program.py
from peye import *
fact(p(1), q(2))
--- stdout
q(2)
p(1)

=== a goal with no solution has no conclusion
spec: 7.4, 7.6
args: program.py --goal "p(2)"
--- program.py
from peye import *
fact(p(1))
--- stdout

=== a contradiction stops reasoning and prints what was derived
spec: 7.2, 7.5, 7.6
exit: 65
--- program.py
from peye import *
fact(p(1))
implies(p(X), q(X))
contradiction(q(X))
query(p(X))
--- stdout
q(1)
'false'

=== a contradiction overrides goals
spec: 7.5, 7.6
args: program.py --goal "p(X)"
exit: 65
--- program.py
from peye import *
fact(p(1))
implies(p(X), q(X))
contradiction(q(X))
--- stdout
q(1)
'false'

=== a contradiction stops the rules after it
spec: 7.2
exit: 65
--- program.py
from peye import *
fact(p(1))
contradiction(p(1))
implies(p(X), q(X))
--- stdout
'false'

=== a contradiction that never holds changes nothing
spec: 7.5
--- program.py
from peye import *
fact(p(1))
implies(p(X), q(X))
contradiction(q(2))
--- stdout
q(1)

=== exceeding max-depth is an error
spec: 7.3
args: program.py --goal "p()" --max-depth 10
exit: 1
stderr: nonempty
--- program.py
from peye import *
implied_by(p, p)
--- stdout

=== exceeding max-iterations is an error
spec: 7.3
args: program.py --max-iterations 3
exit: 1
stderr: nonempty
--- program.py
from peye import *
fact(n(0))
implies(n(N) & is_(M, N + 1), n(M))
--- stdout

=== exceeding max-inferences is an error
spec: 7.3
args: program.py --max-inferences 1
exit: 1
stderr: nonempty
--- program.py
from peye import *
fact(p(1))
implies(p(X) & p(X), q(X))
--- stdout

=== bounds large enough change nothing
spec: 7.3
args: program.py --max-depth 5 --max-iterations 5 --max-inferences 100
--- program.py
from peye import *
fact(n(0))
implies(n(N) & (N < 3) & is_(M, N + 1), n(M))
--- stdout
n(1)
n(2)
n(3)

=== a run without a proof may use a mode test
spec: 7.7
args: program.py --goal "p(X)"
--- program.py
from peye import *
implied_by(p(X), is_var(X) & unify(X, 'a'))
--- stdout
p('a')

=== a proof that cannot be recorded faithfully is refused
spec: 7.7
args: --proof program.py --goal "p(X)"
exit: 1
stderr: nonempty
--- program.py
from peye import *
implied_by(p(X), is_var(X) & unify(X, 'a'))
--- stdout