AXolotl

Axolotl is an educational game designed for self study and training of logic and formal reasoning. The app includes a library of over 60 problems using three different logic calculi and a short tutorial to get started. Additionally, completed problems can be viewed through the included proof viewer and saved to your gallery as a jpeg image. If you would rather compile to a Latex file, the completed proof may be copied to clip board as a latex file. To learn more about the creators of the app and the supporting institutions please see the About page within the app. If you would like to support us, visit our patreon page:
patreon.com/AXolotlLogicSoftware

Additional problems may be loaded into the app using a simple text based file input language (AXolotl files). Note that only the following unicode symbols are allowed within
AXolotl files ⇒, ⇔, ¬, ∧, ∨,⊤,⊥, ⊢, □, ◦, ε. The symbols ⊢ and ε may only be used for Entailment and the empty list. Furthermore ⊢ will always take two arguments which are lists and constructed using cons and ε. To make this clear we provide multiple example files below:


Function: ◦ 2 infix
Function: a 0
Function: b 0
Function: c 0
Variable: x
Variable: y
Variable: z
Problem: 1 ◦(c,◦(b,a))
Rule: 1 ◦(z,◦(x,y)) ◦(z,◦(y,x)) [C:r]
Rule: 1 ◦(◦(x,y),z) ◦(◦(y,x),z) [C:l]
Rule: 1 ◦(◦(x,y),z) ◦(x,◦(y,z)) [A:r]
Rule: 1 ◦(x,◦(y,z)) ◦(◦(x,y),z) [A:l]
Rule: 0 ◦(a,◦(b,c)) [Goal]


Function: ⇔ 2 infix
Function: ⇒ 2 infix
Function: ∨ 2 infix
Function: p 0
Function: q 0
Variable: x
Variable: y
Variable: z
Variable: w
Problem: 1 ⊢(ε,⇔(∨(p,q),∨(q,p)))
Rule: 2 ⊢(w,cons(⇒(x,y),z)) ⊢(w,cons(⇒(y,x),z)) ⊢(w,cons(⇔(x,y),z)) [⇔:r]
Rule: 1 ⊢(cons(⇒(x,y),cons(⇒(y,x),z)),w) ⊢(cons(⇔(x,y),z),w) [⇔:l]
Rule: 1 ⊢(cons(x,w),cons(y,z)) ⊢(w,cons(⇒(x,y),z)) [⇒:r]
Rule: 2 ⊢(z,cons(x,w)) ⊢(cons(y,z),w) ⊢(cons(⇒(x,y),z),w) [⇒:l]
Rule: 1 ⊢(w,cons(x,cons(y,z))) ⊢(w,cons(∨(x,y),z)) [∨:r]
Rule: 2 ⊢(cons(x,z),w) ⊢(cons(y,z),w) ⊢(cons(∨(x,y),z),w) [∨:l]
Rule: 1 ⊢(w,cons(cons(y,z),x)) ⊢(w,cons(x,cons(y,z))) [shift:r]
Rule: 1 ⊢(cons(cons(y,z),x),w) ⊢(cons(x,cons(y,z)),w) [shift:l]
Rule: 0 ⊢(cons(x,y),cons(x,z)) [AX]


Function: ⇒ 2 infix
Function: ∧ 2 infix
Function: ¬ 1
Function: p 0
Function: q 0
Variable: x
Variable: y
Variable: z
Variable: w
Problem: 1 ⊢(¬(⇒(p,¬(q))),∧(p,q))
Rule: 1 ⊢(cons(x,w),cons(y,z)) ⊢(w,cons(⇒(x,y),z)) [⇒:r]
Rule: 2 ⊢(z,cons(x,w)) ⊢(cons(y,z),w) ⊢(cons(⇒(x,y),z),w) [⇒:l]
Rule: 1 ⊢(cons(x,w),z) ⊢(w,cons(¬(x),z)) [¬:r]
Rule: 1 ⊢(w,cons(x,z)) ⊢(cons(¬(x),w),z) [¬:l]
Rule: 2 ⊢(w,cons(x,z)) ⊢(w,cons(y,z)) ⊢(w,cons(∧(x,y),z)) [∧:r]
Rule: 1 ⊢(cons(x,cons(y,z)),w) ⊢(cons(∧(x,y),z),w) [∧:l]
Rule: 1 ⊢(w,cons(cons(y,z),x)) ⊢(w,cons(x,cons(y,z))) [shift:r]
Rule: 1 ⊢(cons(cons(y,z),x),w) ⊢(cons(x,cons(y,z)),w) [shift:l]
Rule: 0 ⊢(cons(x,y),cons(x,z)) [AX]


Function: ⇒ 2 infix
Function: ∨ 2 infix
Function: ¬ 1
Function: p 0
Function: q 0
Function: ⊥ 0
Variable: x
Variable: y
Variable: z
Variable: w
Problem: 1 ⊢(∨(p,q),⇒(¬(p),q))
Rule: 1 ⊢(cons(x,z),y) ⊢(z,⇒(x,y)) [⇒:I]
Rule: 2 ⊢(w,y) ⊢(w,⇒(y,x)) ⊢(w,x) [⇒:E]
Rule: 1 ⊢(z,x) ⊢(z,∨(x,y)) [∨:I1]
Rule: 1 ⊢(z,y) ⊢(z,∨(x,y)) [∨:I2]
Rule: 3 ⊢(cons(x,z),w) ⊢(cons(y,z),w) ⊢(z,∨(x,y)) ⊢(z,w) [∨:E]
Rule: 2 ⊢(w,y) ⊢(w,⇒(y,x)) ⊢(w,x) [⇒:E]
Rule: 1 ⊢(z,⊥) ⊢(z,x) [⊥:E]
Rule: 1 ⊢(cons(¬(x),z),⊥) ⊢(z,x) [Contra]
Rule: 0 ⊢(cons(x,y),cons(x,z)) [AX]
Rule: 1 ⊢(z,⇒(x,⊥)) ⊢(z,¬(x)) [¬:def1]
Rule: 1 ⊢(z,¬(x)) ⊢(z,⇒(x,⊥)) [¬:def2]
Rule: 1 ⊢(cons(cons(y,z),x),w) ⊢(cons(x,cons(y,z)),w) [shift:l]


Function: ∧ 2 infix
Function: ⇒ 2 infix
Function: □ 1
Function: p 0
Function: q 0
Function: ⊤ 0
Variable: x
Variable: y
Variable: z
Variable: w
Problem: 1 ⊢(ε,⇒(∧(□(p),□(q)),□(∧(p,q))))
Rule: 1 ⊢(y,x) ⊢(□(y),□(x)) [□:r1]
Rule: 1 ⊢(cons(y,z),x) ⊢(cons(□(y),□(z)),□(x)) [□:r2]
Rule: 1 ⊢(cons(x,z),y) ⊢(z,⇒(x,y)) [⇒:r]
Rule: 2 ⊢(z,x) ⊢(z,y) ⊢(z,∧(x,y)) [∧:r]
Rule: 1 ⊢(cons(x,y),z) ⊢(∧(x,y),z) [∧:l]
Rule: 1 ⊢(cons(cons(y,z),x),w) ⊢(cons(x,cons(y,z)),w) [shift:l]
Rule: 0 ⊢(cons(x,y),cons(x,z)) [AX]