Rain makes the ground wet, and the ground is not wet. So it is not raining. This example writes that classic argument as one rule, and EyeProlog’s proof shows exactly which premises it used.
Run it in the playground · Source
Given that rain implies wet ground and the ground is not wet, can we refute “it is raining”?
The contrapositive of “if A then B” is “if not B then not A”. The two are logically equivalent, which is why proving one proves the other.
implies(raining, wet_ground).
false(wet_ground).
The implication is not Prolog’s :-; it is data, a fact about two
propositions. That lets one rule reason about any implication stored this way.
false(A) :-
implies(A, B),
false(B).
If A implies B and B is false, then A is false. This is modus
tollens, the rule behind every proof by contrapositive, written as an
ordinary clause.
refutes(proof1, raining) :-
false(raining).
eyeprolog examples/proof-contrapositive.pl
refutes(proof1, raining).
method(proof1, contrapositive).
reason(proof1, "if rain implies wet ground and the ground is not wet, then it is not raining").
eyeprolog --proof examples/proof-contrapositive.pl
step(refutes(proof1, raining), rule(4), [], [false(raining)]).
step(false(raining),
rule(3),
['A' = raining, 'B' = wet_ground],
[implies(raining, wet_ground), false(wet_ground)]).
The refutation rests on false(raining), which the modus tollens rule
(clause 3) derives from the implication and the observation that the ground is
not wet. The reason/2 string is a summary for people; the steps are the
argument.
condition('C1', resolution, ok, 6).
condition('C4', coverage, ok, 8).
condition('C7', relevance, ok, 9).
trusted(0).
verdict(checked).
All six steps replay and nothing is trusted.
false(wet_ground). The run prints nothing: without the observation
there is no refutation.implies(sprinkler, wet_ground). and ask --goal 'false(X)'. Both
raining and sprinkler are refuted by the same dry ground.implies(storm, raining)., and predict whether storm is
refuted too.Learn more in The Art of EyeProlog, Chapter 26.