A. The possibilities of the package Predicata, a combination of the words predicate and automata, can be best described with the following example.
For which natural numbers n does the formula, describing the McNuggets numbers,
\exists x: \exists y: \exists z: 6 \cdot x+9 \cdot y+20 \cdot z=n
hold? Furthermore, denoting the previous formula as P[n], for which natural number n does
(\forall m: m > n \Rightarrow P[m]) \wedge \neg P[n]
hold?
The idea is to create a deterministic finite automaton which corresponds to a first-order formula such that upon interpretation of every accepted word of the automaton the first-order formula is satisfied (Automata theory: [HMU01], [Pip97], [Koz97]).
The main object type Predicaton consists of an automaton and a list and represents a first-order formula containing the nullary operations 0 and 1 and the binary operation +. A first-order formula with n different free variables, where each free variable is assigned to pairwise distinct natural numbers, is represented by an automaton over the alphabet {0,1}^n. The variables are stored internally as a list of these n natural numbers, where the list coincides with the letters. The i-th position in a letter, i.e. in the n-tuple, corresponds to the variable at the i-th position in the list, i.e. to the variable which is assigned to the natural number at the i-th position. Leaving this technical details aside, the object type Predicaton (4.1-3) can also be called with a mathematically more intuitive first-order formula, which internally creates the deterministic finite automaton and takes care of the variables.
The special case are the first-order formulas with no free variable which can be seen as deterministic finite automaton with one state. This deterministic finite automatons can be either interpreted as True if the only state is a final state or as False otherwise. Thus this procedure, going back to J. R. Büchi ([Büc60]), decides the Presburger arithmetic (by Mojżesz Presburger, 1929, [Pre29]), the first-order theory of the natural numbers with the operation +.
For first-time users it is recommended to start with chapter 4, especially to start with the examples in section 4.2. The structure of the manual follows the structure of the package, thus the chapter 2 and 3 gives insight on how in the background a first-order formula is transferred into deterministic finite automaton. However this is quite lengthy and definitely not recommended to begin with.
Hence it's more interesting to start with the example from above:
We start with A:=Predicaton("(E x:(E y:(E z:6*x+9*y+20*z=n)))");, consisting of a deterministic finite automaton with 17 states. The deterministic finite automaton displays the alphabet on the left, the states on the top, the transitions as entries in the table and the initial and final states at the bottom.
Furthermore we can also display the Predicaton anytime with: Display(A);. Additionally, we can draw it with DrawPredicaton(A);, using the external program graphviz (for requirements refer to the manual of the package Automata).
We can also test for accepted natural numbers with AcceptedByPredicaton(A, 20); where the optional second parameter gives an upper bound. DisplayAcceptedByPredicaton(A, 99); prints the accepted words converted into natural numbers in a nice format.
To conclude with the example, we ask for the greatest natural number which cannot be purchased with the function B:=GreatestNonAcceptedNumber(A); and test for AcceptedWordsByPredicaton(B, 50); or sum up the regular expression PredicatonToRatExp(B) (note: here the binary representation is read form behind.)
A. generated by GAPDoc2HTML