LRC_F

The Logic Resource Center Base System. This system has a clean sytax and offers the falsum and identity. All problem types will be available in this sytem.

Constants

¬&∨→↔∀∃=⊥

Example Formula

∀x∀y(x=y→(Lx↔Ly))

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