Encode a theorem or a definition

In this how to we will show you how to encode a theorem (this concept will also work for many other knowledge artifacts like definitions). To do so, we will make use of pyirk scopes and pythons context managers. The resulting script can be found here.

The example theorem

As an example, we want to encode a simplified version of the Pythagorean theorem, which reads:

Let \((a, b, c)\) be the sides of a triangle, ordered from shortest to longest, and \((l_a, l_b, l_c)\) the respective lengths. If the angle between a and b is a right angle then the equation \(l_c^2 = l_a^2 + l_b^2\) holds.

As you can see, the theorem consists of several “semantic parts”, which in the context of Pyirk are called scopes. In particular we have the three following scopes:

  • setting: “Let \((a, b, c)\) be the sides of a triangle, ordered from shortest to longest, and (la, lb, lc) the respective lengths.”

  • premise: “If the angle between a and b is a rect angle”

  • assertion: “then the equation \(l_c^2 = l_a^2 + l_b^2\) holds.”

In the following, we will see how this structure can be exploited to encode the theorem.

The theorem item

As usual, we start by creating a “blank” item to encode the theorem. Note however, that we make it an instance of I15["implication proposition"], which is one of several mathematical propositions are already included in pyirk.

1# create the theorem
2I5000 = p.create_item(
3    R1__has_label="simplified Pythagorean theorem",
4    R4__is_instance_of=p.I15["implication proposition"],
5)

Defining setting, premise and assertion

With our theorem I5000 being an implication, it possesses a scope() method that returns a context manager that we can use in a with statement to define the setting:

1# create the setting
2with I5000["simplified Pythagorean theorem"].scope("setting") as st:
3    # the theorem should hold for every planar triangle,
4    # thus a universally quantified instance is created
5    st.new_var(ta=p.uq_instance_of(I2917["planar triangle"]))
6    st.new_var(sides=I9148["get polygon sides ordered by length"](st.ta))
7
8    a, b, c = p.unpack_tuple_item(st.sides)
9    la, lb, lc = a.R2495__has_length, b.R2495, c.R2495

Note

To keep this howto simple, the objects I2917["planar triangle"] as well as I1002["angle"] and I1002["right_angle"] are taken from the OCSE.

Next, we encode the premise:

1# create the premise
2with I5000["simplified Pythagorean theorem"].scope("premise") as st:
3    st.new_equation(lhs=I1002["angle"](a, b), rhs=I1003["right angle"])

At last, we are able to state the assertion:

1# create the assertion
2with I5000["simplified Pythagorean theorem"].scope("assertion") as st:
3    # convert a pyirk items into  sympy.Symbol instances to conveniently
4    # denote formulas (see documentation below)
5    La, Lb, Lc = p.items_to_symbols(la, lb, lc)
6    st.new_equation(La ** 2 + Lb ** 2, "==", Lc ** 2)