page 2  (16 pages)
to previous section1
3to next section

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 one-sorted 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 n-ary 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 operator-operand 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 first-order 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 (first-order) definable set of structures (and defined by OE).