Eris

Interactive Proof Environment

Explorations in creating an direct manipulation logic tool

@prabros

Beginnings of creating a graphical logic environment where you can directly manipulate your proofs.

Logical Operators

20 August 2026

A small selection of logical operators for the environment

Shows a 3 by 3 table for the operators (∧, ∨, →) with their corresponding introduction and elimination functions. The introduction functions have one two ports on the left and one port on the right and the elimination ones have two ports on the right and one port on the left.

Semantic Zoom

17 August 2026

What if you could zoom through salient parts of your logical argumentation?

Zooming Logical Terms

Visualizes three levels of zoom on the logical terms. The first one shows the expression (P∧Q)∧(P∧R). In the second one, the middle ∧ is lifted as a common operation on containers with two terms (P∧Q) and (P∧R). In the third one, all the ∧s are lifted to visualize a container for (P∧Q), another for (P∧R), and both of them nested inside a big one with the operator ∧.

We will see this mechanism is in the context of a proof derivation shortly. For now, here are the various levels of detail of the logical terms.

The textual and graphical representation of the expression (L∧M∧N)∧(P∧Q∧R∧S). In the textual representation, there are 6 ∧ operations, while in the graphical representation there is only 3, as it is an s-expression like representation equivalent to (∧ (∧ L M N) (∧ P Q R S)).

While it might look like a straight forward visual change, lifting the operator to the container level means that the number of infix operators get reduced. This is analogous to an s-expression representation.