Attribute sequence

A clause attribute is a characteristic of a clause. Some examples of clause attributes are:
- the number of literals in a clause (i.e., clause length)
- the number of term symbols in a clause
- the number of constants in a clause
- the number of variables in a clause
- the number of functions in a clause
- the number of negative literals in a clause
- the number of positive literals in a clause
- the number of distinct variables in a clause
- the maximum depth of any term in all the literals in a clause
Example:
the clause C = ~P(x) \/ Q(a,b,f(x)) has
a length of 2 because it contains 2 literals
1 negative literal which is ~P(x)
1 positive literal which is Q(a,b,f(x))
2 constants which are a and b
2 variables (x occurs twice)
1 distinct variable which is x
1 function which is f
maximum term depth of 2
5 term symbols which are x,a,b,f,x
An attribute sequence is a sequence of k n-tuples of clause attributes that represent a projection of a set of derivations of length k. k and n are strictly positive integers. The set of derivations form the domain and the attribute sequences form the codomain of the mapping between derivations and attribute sequences.
Example:
<(2,2),(2,1),(1,1)> is an attribute sequence where k3 and n2. It corresponds to some derivation, say, <(B1,B2),(R1,B3),(R2,B4)> where B1, B2, R1, B3, R2, and B4 are clauses. The attribute here is assumed to be the length of a clause.
The first pair (2,2) correpsonds to the pair (B1,B2) from the derivation. It indicates that the length of B1 is 2 and the length of B2 is also 2. The second pair (2,1) corresponds to the pair (R1,B3) and it indicates that the length of R1 is 2 and the length of B3 is 1. The last pair (1,1) corresponds to the pair (R2,B4) and it indicates that the length of R2 is 1 and the length of B4 is 1.
Note: An n-tuple of clause attributes is similar to the feature vector named by Stephan Schulz, PhD (see E equational theorem prover).

Main Menu

See Also

Main Menu