Javascript Interactive Higher-Order Theorem Prover

Automated Reasoning in Higher Order Logic

Automated Reasoning in Higher Order Logic

Scunak

Math Gate

This page was created and is maintained by Chad E Brown.

Here's an example of a locally confluent reduction which is not confluent (and not terminating).

I found this in Gehrke's Thesis.

a <- b <-> c -> d

Here's another example. I created this one.

Consider the reduction defined on the natural numbers by:

2^n -> 2^{n+1}

2^n -> 3^{n}

3^n -> 3^{n+2}

This is locally confluent, since 2^n -> 2^{n+1} -> 2^{n+2} -> 3^{n+2} and 2^n -> 3^n -> 3^{n+2}. However, it is not confluent since 2 -> 3 and 2 -> 4 -> 9, but 3 and 9 are not joinable. The reduction is clearly not terminating.