ulkb.Theory.new_axiom

Theory.new_axiom(arg1, arg2=None, **kwargs)

Adds new axiom.

If arg2 is not given, uses arg1 to generate an id.

Parameters:

• arg1 – Id or Formula.

• arg2 – Formula.

• kwargs – Annotations.

Returns:

Sequent.

Equivalent to:

self.extend(NewAxiom(
   Constant(arg1, arg2.type), arg2, **kwargs));
self.axioms_dict[arg1]

See also

new_axiom().