OLI

The Carnegie-Mellon University (CMU) Online Learning Initiative (OLI) system.

Constants

¬&∨→↔∀∃=⊥

Example Formula

(∀x)(∀y)(x=y→(L(x)↔L(y)))

Term Extensions

F1a2x3

Allow Open Sentences

Yes

Known Issues

* The citation format is not correct in some cases - e.g. having a comma where OLI has a dash. * Citation order has not thoroughly been checked. * Error message terminology has not yet been customized for this system.

Problem Types

Point And Click DerivationExperimental Point And Click TableauExperimental Free Tableau

Derivation Rules

Point And Click

Assum: Assumption&I: Conjunction Introduction&EL: Conjunction Elimination Left&ER: Conjunction Elimination Right∨IL: Disjunction Introduction Left∨IR: Disjunction Introduction Right∨E: Disjunction Elimination¬I: Negation Introduction⊥I: Falsum Introduction¬E: Negation Elimination⊥E: Falsum Elimination→I: Conditional Introduction→E: Conditional Elimination↔I: Biconditional Introduction↔EL: Biconditional Elimination Left↔ER: Biconditional Elimination Right∀I: Universal Introduction∀E: Universal Elimination∃I: Existential Introduction∃E: Existential Elimination=I: Identity Introduction=E: Identity EliminationComm&: Conjunction CommutivityComm∨: Disjunction CommutivityDeM: De MorganDSL: Disjunctive Syllogism LeftDSR: Disjunctive Syllogism RightDNE: Double Negation EliminationDNI: Double Negation Introduction→DefI: Conditional Introduction From Material Definition→DefE: Conditional Elimination For Material DefinitionHS: Hypothetical SyllogismMT: Modus TollensTrans: Transposition