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