Precedence Declarations

All orderings that one may select require a complete precedence of function and predicate symbols. This precedence may be partially or completely defined by the user. Partial precedences will be completed automatically by the system.

The optional declaration of the form

$$\mbox{{\tt top\_ {}predicates\_ {}precedence(list(PredicateSymbols)).}}$$

lists all the predicates (in deceasing precedence) that are considered to be greater than any function symbol (including those that occur in subsequent enrichments of this theory) and greater than any other predicate symbol. (In previous versions of Saturate the term first_ predicate_ precedence was used.) The declaration

$$\mbox{{\tt precedence(list(FunctionAndPredicateSymbols)).}}$$

specifies the possibly partial precedence of the non-top predicate and function symbols in decreasing order. There is a pre-defined constant '$min' which is smaller than any other symbol. '$min' may occur in clauses but must not occur in the precedence declaration. We have examples in which saturation is much faster if the smallest constant is employed (e.g., modal logic KD45).

Each theory module may have separate [top predicates] precedence declarations associated with it in which the symbols of the module are related to each other. When combining modules by importing them into another module, the union of the precedences must be non-circular. In particular it is not allowed to declare a predicate as a ``top predicate'' in one module and at the same time include it in a precedence declaration for non-top symbols in another module. Precedence declarations in a module which imports one or several modules must be consistent with the declarations in the module(s).

The automatic completion of the precedence seems to work well in most cases for predicate symbols. For function symbols that occur in equations some rather simple pragmatic assumptions are made. In particular, the system attemps to define the precedence such that equations are oriented from left to right.

Imprint | Data Protection