What the name means

QF means quantifier-free. RDL is historically named rational difference logic; its variables range over real numbers and its fixed bounds are rational numbers.

Quantifier-free formulas have no explicit "for every" or "there exists" binders. They can still contain unknown values that the solver must find.

A rational number is a ratio of integers, such as 1/2. Real-valued variables can lie between any two distinct bounds. They do not advance in whole ticks and do not round like floating-point values.

Each comparison bounds the difference between two variables. Strict bounds matter here: finish − start < 1/2 excludes exactly one-half, while ≤ includes it. Boolean choices can combine these comparisons.

Worked example

Check a response window

A response must arrive more than one-quarter of a second after a request, but no later than one-half of a second afterward.

  1. Let request and response be real-valued times.
  2. Require request − response < −1/4 and response − request ≤ 1/2.
  3. Set request = 0 and response = 3/8. The gap is greater than 1/4 and at most 1/2.

The query is sat. A gap of 3/8 second fits inside the response window.

This is an authored mathematical example, not captured Axeyum output. Here, sat means the constraints can all hold; unsat means they cannot.

A contrasting case

A gap strictly below 1/2 and at least 1/2 cannot exist. The query with both requirements is unsat, even though the endpoints touch.

Use cases

  • Check consistency among clock differences in timed-system models.
  • Test fractional latency bounds without rounding them to integer ticks.

Modeling caution

Real time is a modeling choice. A physical clock has resolution and measurement error; encode those facts if the answer depends on them.

Axeyum coverage

The examples explain the logic's meaning. They do not establish complete Axeyum support for this division. Acceptance, solving, and evidence coverage depend on the input and the solver route.

This division has no row in the site's retained regression scoreboard. Consult the engine's support documentation for the relevant route.

The results page also includes a retained comparison for this division. Its figures apply to the named benchmark list and resource budget.

A solver may return unknown if it cannot settle a query. That result establishes neither sat nor unsat. Parsing a declared logic name alone does not prove support for every formula in it.

Engine support documentation at the site's recorded snapshot, 03ae4a3c9, 2026-10-05.

Definitions and references

Definitions consulted September 6, 2026. The worked examples and use-case explanations are authored for this guide.