Attributes

Several kinds of attribute can be attached to input formulas with the # operator, for example,

x * y = y * x              # label(commutativity).
x * c != e                 # answer(x) # label("the denial").
-p(c) | -q(c)              # answer("here it is").
a * b != b * a             # action(in_proof -> exit) # answer(commutativity).
x * (y * z) = y * (x * z)  # bsub_hint_wt(500).

Each attribute has a data type of string, integer, or term. A string attribute is really just a term attribute that is a constant. If a string attribute is not a legal constant, it can be enclosed in double quotes to make it so.

Attributes can be attached only to the top level of a formula; they cannot be attached to proper subformulas. (This restriction might be lifted in future versions of Prover9.)

The accepted attributes are shown in the following table.

Name	Type	Inheritable	Purpose
label	string	No	Comment
answer	term	Yes	Record substitutions and what has been proved
action	term	No	Triggers action when clause is used
bsub_hint_wt	integer	No	Used for hints

Inheritable attributes are passed from parent to child during most inference rules.

Label Attributes

Label attributes are simply comments that can be attached to input clauses, including hint clauses.

Answer Attributes

Answer attributes on clauses are essentially answer literals. They are inherited during application of inference rules, and if they contain variables, the variables are instantiated by the substitution used in the inference.

Answer attributes (like all other attributes) contain exactly one argument. If you wish to record substitutions for more than one variable, you must use a term that contains all of the variables, for example, a list, as in the following clause.

-p(c,x,y,z)  # answer([x,y,z]).

Answer attributes need not contain variables. For example, when there are multiple goals, answer attributes can be used on the goal formulas to identify the goals that are proved.

Answer attributes on non-clausal formulas cannot contain variables. (This restriction might be lifted in future versions of Prover9.)

Action Attributes

Action attributes cause various things to happen when clauses are used in various ways. See the section on Actions.

Bsub_hint_wt Attribute

This attribute can be attached to a hint clause, and it is used to override ordinary weight assigned to clauses that match the hint. That is, if a hint matches a clause, and if the hint has a bsub_hint_wt attribute, the clause gets the value of the attribute as its weight instead of the weight that would be assigned by the ordinary weighting method.

Next Section: Goals and Denials