functions-test-file_new.txt

Base_functions      := { }
Extension_functions := { (f,1), (g,1), (h,1)}
Relations           := { (R,2), (M,3) }
Constants         := { (a, int), (b, int), (c, int), (d, int), (e, int) }

Base :=
  (FORALL x, y, z). M[x,y,z] --> R[z, x];
  (FORALL x, y, z). M[x,y,z] --> R[z, y];
  (FORALL x, y, z, u). M[x, y, z], R[u, x], R[u, y] --> R[u, z];
  (FORALL x). R[x, x];
  (FORALL x, y). R[x, y], R[y, x] --> y = x;
  (FORALL x, y, z). R[x, y], R[y, z] --> R[x, z];



Clauses:=
% Axiom R1
% Monotonicity axioms of f, g, h
  (FORALL x, y). R[x, y] --> R[f(x), f(y)];
  (FORALL x, y). R[x, y] --> R[g(x), g(y)];
  (FORALL x, y). R[x, y] --> R[h(x), h(y)];

Query:=

R[c, a];
R[a, g(b)];
R[b, d];
R[e, f(a)];
% Negation of inclusion to be proved:
NOT(R[e, h(d)]);


R[b, g(b)] --> R[f(b), h(b)];
R[b, g(a)] --> R[f(b), h(a)];
R[b, g(d)] --> R[f(b), h(d)];
R[a, g(b)] --> R[f(a), h(b)];
R[a, g(a)] --> R[f(a), h(a)];
R[a, g(d)] --> R[f(a), h(d)];
R[d, g(b)] --> R[f(d), h(b)];
R[d, g(a)] --> R[f(d), h(a)];
R[d, g(d)] --> R[f(d), h(d)];