3.2 一阶定理证明

回顾一下我们较早前在(10)中提出的 to the north of 上的限制：

  1. all x. all y.(north_of(x, y) -> -north_of(y, x))

令人高兴的是，定理证明器证明我们的论证是有效的。相反，它得出结论：不能从我们的假设推到出north_of(f, s)：

  1. >>> FnS = read_expr('north_of(f, s)')
  2. >>> prover.prove(FnS, [SnF, R])
  3. False