# Special Relations

## Special Binary Relations

Binary relations that are partial orders, linear orders, tree orders, and piece-wise linear orders can be axiomatized using first order quantifiers. However, reasoning with these quantified axioms involves non-linear overhead, up to a quadratic number of quantifier instantiations. The decision procedures for partial, linear, tree and piece-wise linear orders in z3 use variants of Bellman-Ford push relabeling graphs.

### Partial Order

Use instead

`(define-fun R ((x A) (y A)) Bool ((_ partial-order 0) x y))`

We are using the index 0 to identify the partial order relation `R`

. To create a different relation that is also a partial order use
a different index, such as `(_ partial-order 1)`

.

### Linear Order

Use instead

### Tree Order

Use instead

### Piece-wise Linear Order

Use instead

`(define-fun R ((x A) (y A)) Bool ((_ piecewise-linear-order 0) x y))`

## Transitive Closures

The transitive closure of a relation is not first-order axiomatizable. However, the decision problem for ground formulas is decidable
because for every binary relation `R`

over a finite domain, the transitive closure of it is defined over the finite graph of `R`

.
The small model property contrasts non-ground first-order formulas using transitive closure that are not first-order axiomatizable.