kenny2github / validtnt

Parse and validate Typographic Number Theory proofs

validtnt

Parse and validate Typographic Number Theory proofs.

Examples

This proof passes:

∀a:~Sa=0	axiom 1
∃b:∀a:~Sa=b	existence
<∀a:~Sa=0∧∃b:∀a:~Sa=b>	joining

because all rules of TNT were applied correctly.

This proof doesn't:

∀a:(a+0)=a	axiom 2
∃b:∀a:(a+b)=a	existence
∃b:(b+b)=b	specification

because specification is not allowed when the term that specifies the variable contains any quantified variable.