CHR has two kinds of declarative semantics: First-order logic declarative semantics and Linear logic declarative semantics.

Because CHR can model changes by removing and adding constraints, not each CHR program has First-order logic semantics, but it has linear logic semantics.

For example,

```
duplicate @ X leq Y \ X leq Y <=> true.
reflexivity @ X leq X <=> true.
antisymmetry @ X leq Y , Y leq X <=> X=Y.
transitivity @ X leq Y , Y leq Z ==> X leq Z.
```

This CHR program has First-order logic reading:

```
∀ X,Y (X≤Y ∧ X≤Y ⇔ X≤Y) ∧
∀X (X≤X ⇔ true) ∧
∀ X,Y (X≤Y ∧ Y≤X ⇔ X=Y) ∧
∀ X,Y,Z (X≤Y ∧ Y≤Z ⇒ X≤Z)
```

However, the following CHR program has no First-order logic reading:

```
throw(Coin) <=> Coin = head
throw(Coin) <=> Coin = tail
```

If you insist on First-order logic reading, it will be

```
∀Coin.(throw(Coin) ⇔ (Coin=head)) ∧
∀Coin.(throw(Coin) ⇔ (Coin=tail))
```

This is obvious wrong.

But it has linear logic reading:

```
!∀Coin.(throw(Coin) ⊸ !(Coin=head)) ⊗
!∀Coin.(throw(Coin) ⊸ !(Coin=tail))
```

which logically equivalent to:

```
!∀Coin.(throw(Coin) ⊸ !(Coin=head)) ⊗
(throw(Coin) ⊸ !(Coin=tail))
```

which logically equivalent to:

```
!∀Coin.(throw(Coin) ⊸ !(Coin=head) & !(Coin=tail))
```

This formula reads as “Of course, consuming `throw(Coin)`

produces: choose from `Coin=head`

and `Coin=tail`

”. In other words, we can replace `throw(Coin)`

with either `Coin=head`

or `Coin=tail`

but not both at the same time, i.e. a committed choice takes place.

Note that the penultimate logical equivalence uses “universal quantifiers distribution over ⊗”, I haven’t see this theorem on the internet, but intuitively it ought to be the same as “universal quantifiers distribution over ∧” in first order logic.