SyntaxNuts And Bolts

This page details the syntax for Logic for Fun input. This is a proper subset of FINDER input. Full FINDER input allows more freedom in ordering items and includes text format for settings, notation for soft constraints, randomisation and other things.

Input text is case-sensitive.

In the grammar, literal text is in bold face. Normal plain text expressions are defined in the grammar. Italic expressions in pointed brackets are not defined here. As usual, the vertical bar indicates alternatives and square brackets indicate that the enclosed expressions are optional. The star indicates a series of zero or more of the indicated items, separated by white space.

The expression “posint” stands for a positive integer, and “natint” for a natural number or non-negative integer.

Identifiers are character sequences not beginning with numerical digits and not containing white space or any reserved characters such as punctuation. Local (user-defined) identifiers and may not be overloaded. Sort names (whether user-defined or built-in) may not be overloaded. Undeclared identifiers, used as variables in clause form or as names in FOF form, must start with letters, though declared identifiers may start with non-alphabetic characters.

Specifically, user-defined identifiers may not include white space or any of the symbols:
( ) { } . , : ; % # = < > + – * / ! ¬ ∧ ∨ → ∀ ∃
They should not redefine numerals (0, 1, 2, etc) or the reserved expressions:
MIN, MAX, PRED, SUCC, FALSE, TRUE, NOT, SOME, ALL, IFF, AND, XOR, OR, IMP.
While it is not forbidden by the grammar, it is recommended that you avoid redefining the words:
all_different
bool
clause
commutative
constraint
cut
end
function
hidden
injective
int
nat
natnum
no_cut
no_priority
partial
print
priority
scope
setting
sort
surjective
total
vocabulary

Sorts must be declared before they can be used in the cardinality specifications of other sorts. For example, the sort declarations
        foo {}
        bar {size = foo.size + 1}
are fine, but
        foo {size = bar.size – 1}
        bar {}
are not.

Types must match. Each type specification gives its function symbol an arity and specifies the types of its arguments (if any) and its value. Function symbols in infix position must be binary (dyadic). Function symbols of arity greater than 0 must be declared before they occur in a formula.

Built-in expressions such as “+” may be typically ambiguous. They may be disambiguated as required by subscripting with a sort name (i.e. appending an underscore and the sort name). Some of them such as “=” never need such disambiguation: in their cases, subscripting is an error.

Normally, the outermost function symbol of a formula is expected to have value type bool. This is not a requirement, however: a formula F occupying an antecedent or consequent place in a clause is treated as equivalent to NOT (F=MIN) on the same convention as in C.

The built in sorts are:

bool { enum: FALSE, TRUE. }

natnum { cardinality = 30 alias nat alias int }

The non-negative integers 0, 1, 2, etc behave as an enumeration of the natnum sort, but the cardinality of natnum may be changed by means of a sort specification, so it is not regarded as an enumerated sort in the full sense.

A quantifier binding a variable is not allowed inside the scope of another quantifier binding the same variable. In FOF form, but not in clause form, all variables must be bound by quantifiers. In clause form, but not in FOF form, all names (0-adic function symbols) must be declared before they are used.

In FOF form, every clause must consist of a single formula with a terminating period.

The grammar for formulae as it stands is ambiguous, as strings such as “A foo B bar C” are generated. This is deliberate. Ambiguity is resolved according to scope settings, breaking ties by associating to the left.