
has a profile, which is a finite sequence of sorts. A relation constant with empty profile is called a propositional constant. A function constant with singleton profile is called an object constant. We will write a signature by listing its sorts, a semicolon, its relation constants, each followed by its profile in parentheses, another semicolon, and its function constants in a similar way. Thus, a onesorted signature with the unary relation constant P and a binary function constant f is written (u; P (u); f(u; u) : u). A structure over a signature F is a set of disjoint domains Ds, one for each sort s, and, for each relation constant in F of profile s1; : : : ; sn, an nary relation table over Ds1 ? ? ? ? ? Dsn , and, for every function constant, a function table compatible with its profile. We consider only finite domains, but also infinite families of structures with unbounded domain.
Objects easily defined using structures are various types of graphs (directed, undirected, multi), oriented and unoriented matroids, trees (ordered and unordered) etc. Another example:
Example 1. A propositional formula is representable as a structure relating formulas
and subformulas. Each logical operator used binds a formula together with
its operands. There are a number of possible signatures representing propositional
formulas. If the objects are formulas and subformulas, then one can have
unary relations to represent the operator of a formula, and a number of incidence
relations for pointing out the operatoroperand relations. For propositional logic
one can thus have the signature
F = (u; P:(u); P^(u); P_(u); Op1(u; u); Op2(u; u); Root() : u). As an example,
the formula p ^ (q _:p) is represented in signature F with domain fa; b; c; p; qg
as
Root : a
P: : fcg
P_ : fbg
P^ : fag
Op1 : f(a; p); (b; q); (c; p)g
Op2 : f(a; b); (b; c)g:
Many applications deal with propositional formulas and depend on solving their satisfiability and related problems. Note that not all structures over F correspond to well formed propositional formulas.
We assume known the concept of firstorder formula and satisfaction of a formula by a structure, using the intermediate concept of variable assignment[28]. Thus, if a formula is satisfied by structure I under variable assignment V we write I j= OE[V ].
A structure that satisfies a formula OE for all variable assignments V is called a model for OE, written I j= OE. If a set of structures is exactly the set of models of a first order formula OE, then the set is said to be a (firstorder) definable set of structures (and defined by OE).