Clause Properties (Advanced)

Several Prover9 features (keep/delete rules and given-selection rules) allow the user to specify subsets of clauses by using a simple language. Examples are clauses to keep, clauses to discard, and clauses to be selected as given clauses. For example, to specify Horn clauses with more than three literals, one can write the rule

horn & literals>3.

Basic Properties:

`positive`	all literals are positive
`negative`	all literals are negative
`mixed`	contains positive literals and negative literals
`unit`	exactly one literal
`horn`	the clause has at most one positive literal
`definite`	the clause has exactly one positive literal
`has_equality`	contains a positive or negative equality literal
`true`	true in interpretations(s)
`false`	false in interpretations(s)
`hint`	the clause matches a hint
`initial`	the clause was present before the selection of the first given clause
`resolvent`	the clause is a (binary) resolvent
`hyper_resolvent`	the clause is a hyperresolvent
`ur_resolvent`	the clause is a unit-resulting (UR) resolvent
`factor`	the clause is a (binary) factor
`paramodulant`	the clause is a paramodulant
`back_demodulant`	the clause is a back demodulant
`subsumer`	the clause back subsumed another clause
`all`	all clauses have this property

Integral Properties

The following properties are used with relations <, <=, =, >=, >.

`weight`	weight of the clause
`literals`	number of literals in the clause
`variables`	number of (distinct) variables in the clause
`depth`	depth of the deepest term in the clause
`level`	level of the clause (derivation distance from input)

Boolean Combinations

Non-atomic expressions are constructed in the same way as ordinary formulas, with the following operations.

`&`	conjunction
`\|`	disjunction
`-`	negation