LRC_P

This is mostly just showing off the capabilities of the system, but consider: especially with free use of the formula parser, the tableaux and the point and click form of the derivation, Polish notation is now teachable.

Constants

¬&∨→↔∀∃=⊥

Example Formula

∀x∀y→=xy↔LxLy

Term Extensions

F1a2x3

Allow Open Sentences

No

Known Issues

None

Problem Types

Typed Forward Strict DerivationPoint And Click DerivationExperimental Point And Click TableauExperimental Free Tableau

Derivation Rules

Typed Forward Strict

A: AssumptionR: Reiteration&E: Conjunction Elimination&I: Conjunction Introduction∨E: Disjunction Elimination∨I: Disjunction Introduction→E: Conditional Elimination→I: Conditional Introduction↔E: Biconditional Elimination↔I: Biconditional Introduction¬I: Negation Introduction⊥I: Falsum Introduction¬E: Negation Elimination⊥E: Falsum Elimination∃E: Existential Elimination∃I: Existential Introduction∀E: Universal Elimination∀I: Universal Introduction=E: Identity Elimination=I: Identity Introduction

Point And Click

A: AssumptionR: Reiteration&E: Conjunction Elimination&I: Conjunction Introduction∨E: Disjunction Elimination∨I: Disjunction Introduction→E: Conditional Elimination→I: Conditional Introduction↔E: Biconditional Elimination↔I: Biconditional Introduction¬I: Negation Introduction⊥I: Falsum Introduction¬E: Negation Elimination⊥E: Falsum Elimination∃E: Existential Elimination∃I: Existential Introduction∀E: Universal Elimination∀I: Universal Introduction=E: Identity Elimination=I: Identity Introduction