Eris

Interactive Proof Environment

Explorations in creating an direct manipulation logic tool

@prabros

Multiple Proof Paths

26 August 2026

There could be multiple ways to logically derive a proposition from the premises. What if we could visualize these different deductive trajectories? Here is the proposition P derived in two ways from the premise (P∧Q) ∧ (R∧P).

Text Representation
1 (P∧Q)∧(R∧P) Assumption
2 (P∧Q) ∧E (1)
3 P ∧E (2)
Multiple ways of deriving P from (P∧Q) ∧ (R∧P)

Shows the derivations of the following proofs in a single graph:
1 | (P∧Q)∧(R∧P) | Assumption
2 | (P∧Q) | ∧E (1)
3 | P | ∧E (2)

and

1 | (P∧Q)∧(R∧P) | Assumption
2 | (R∧P) | ∧E (2)
3 | P | ∧E (2)
Text Representation
1 (P∧Q)∧(R∧P) Assumption
2 (R∧P) ∧E (2)
3 P ∧E (2)