What the name means

UF means uninterpreted functions and permits abstract sorts. Without QF, formulas may quantify over their values.

An abstract sort supplies a nonempty set of values without choosing a numeric representation. A function maps inputs to outputs consistently. Quantifiers can impose laws on every input, beyond the calls explicitly named in a query.

The domain is not automatically limited to the constants declared in the file. A solver must account for the general rule, not only try the objects already named. General quantified reasoning can return unknown when the search cannot settle the formula.

Worked example

Use a rule for every object

Let Object be an abstract sort and normalize a function from Object to Object. Require normalize(x) = x for every x.

  1. Declare a particular object named sample.
  2. Ask whether normalize(sample) ≠ sample.
  3. Apply the universal rule to sample. It requires normalize(sample) = sample and contradicts the requested difference.

The query is unsat. A rule covering every object also covers the named sample.

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

Remove the universal rule. Then normalize(sample) ≠ sample is sat in a domain with distinct objects: the function can send sample to a different object.

Use cases

  • Express general algebraic laws for abstract interfaces.
  • Model relational rules over identifiers when the number and representation of objects are not fixed in advance.

Modeling caution

Listing a few constants does not declare the whole domain. If the application has exactly a fixed set of states, use a finite datatype or explicit constraints that establish that restriction.

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 appears in the site's retained regression scoreboard. Read the individual slices and their source records for the tested scope.

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.