ulkb.Theory.new_theorem#

Theory.new_theorem(arg1, arg2=None, **kwargs)[source]#

Adds new theorem.

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

Parameters:

  • arg1 – Id or Sequent.

  • arg2 – Sequent.

  • kwargs – Annotations.

Returns:

Sequent

Equivalent to:#
extend(NewTheorem(
   Constant(arg1, BoolType()), arg2), **kwargs));
self.theorems_dict[arg1]

See also

new_theorem().