- Attribute sequence
A clause attribute is a characteristic of a
clause . Some examples of clause attributes are:- the number of
literal s 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
integer s. 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 k=3 and n=2. 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 ).ee also
*
Carine theorem prover External links
* [http://www.atpcarine.com] CARINE's web site
Wikimedia Foundation. 2010.
