Figure 1. FOL translation options
The diamond property (DP) in rewriting theory states that, if x rewrites to both y and z, then the latter two rewrite both to some u (all in one step). We want to prove that if some rewrite relation satisfies DP, then its reflexive closure also satisfies DP (reflexive closure means adding point loops to every point). In the following code dom is user domain predicate, r the rewrite relation, and re = r or equal (that is, the reflexive closure of r).
%dpe.fol
axiom:fol:1_domain_contains_a_b_c:
(true => (dom(a) & dom(b) & dom(c))).
axiom:fol:2_goal_axiom:
![X]:((re(b,X) & re(c,X)) => conjecture).
axiom:fol:3_reflexivity_of_equal:
![X]:(dom(X) => X=X).
axiom:fol:4_aassumption:
(true => (re(a,b) & re(a,c))).
axiom:fol:_symmetry_of_equal:
![X,Y]:(X=Y => Y=X).
axiom:fol:6_left_congr_of_equal:
![X,Y]:((X=Y & re(Y,Z)) => re(X,Z)).
axiom:fol:7_re_contains_equal:
![X,Y]:(X=Y => re(X,Y)).
axiom:fol:8_re_contains_r:
![X,Y]:(r(X,Y) => re(X,Y)).
axiom:fol:9_re_elimination:
![X,Y]:(re(X,Y) => (X=Y | r(X,Y))).
axiom:fol:10_diam_prop_of_r:
![X,Y,Z]:((r(X,Y) & r(X,Z)) => ?[U]:(r(Y,U) & r(Z,U))). %10
conjecture:fol:11_TO_PROVE:
conjecture.
GeologUI requires FOL file inputs to actually have a .fol file extension. Save a clip of the previous code to file dpe.fol in order to reproduce the experiments described here.
We have three(3) options for loading this theory into GeologUI: Hit the F key to elicit the following little dialog (showing default option).
Using terse tabulation produces 35 geolog rules (or 45 verbose rules). Attemps to achieve a proof with either translation eventually convinces us that too many cases are produced by tabulated translation of this FOL theory. It is worth while to spend some time tinkering with some proof attempts. Heuristic controls also seem too meagre.
Reload using the "preserve coherent axioms" option. This translation produces the geolog theory and refutation (proof of conjecture) illustrated in the following snapshot -- NO heuristic controls turned on!
However, the ordering of the inputs is maintained and this ordering played a role in achieving the refutation shown. Other orderings could still afford a (different) refutatation, possibly requiring some heuristic control.
The FOL theory dpe.fol mimics the following geolog theory (borrowed from Marc Bezem). Notice how conjecture is replaced by goal and there is no input corresponding to the conjecture in dpe.fol.
%% dpe.gl
true => exists(a), exists(b), exists(c). %1
re(b,X), re(c,X) => goal. %2
exists(X) => e(X,X). %3
true => re(a,b), re(a,c). %4
e(X,Y) => e(Y,X). %5
e(X,Y), re(Y,Z) => re(X,Z). %6
e(X,Y) => re(X,Y). %7
r(X,Y) => re(X,Y). %8
re(X,Y) => e(X,Y) ; r(X,Y). %9
r(X,Y), r(X,Z) => exists(U), r(Y,U), r(Z,U). %10
Save a clip of this code to file dpe.gl,
load dpe.gl into GeologUI and confirm that there there
is a proof essentially identical to the one illustrated
in Figure 2, except that false leaves in
the refutation are replace by