• 3.2 一阶定理证明

    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