tnt 1.0.2

Simple runtime validated proofs in number theory
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

// Well-formed formulas are only equalities, logical statements, quantifications, and negations
formula = _{ equality | logical_formula | quantification | negation }

// Note that equality is between *expressions* not formulas
equality = { term ~ "=" ~ term }

// A logical assertion about two formulas: and, or, implies
logical_formula = _{ and | or | implies }
and = { "[" ~ formula ~ ("&"|"∧") ~ formula ~ "]" }
or = { "[" ~ formula ~ ("|"| "∨") ~ formula ~ "]" }
implies = { "[" ~ formula ~ (">"|"⇒") ~ formula ~ "]" }

// Valid uantifications are a universal or existential assertion followed by a formula
quantification = _{ universal | existential }
universal = { ("A"|"∀") ~ variable ~ ":" ~ formula }
existential = { ("E"|"∃") ~ variable ~ ":" ~ formula }

// A negation is a negation symbol followed by a formula
negation = { ( "~"|"¬" ) ~ formula }

// Terms are arithmetic expressions
term = _{ zero | variable | addition | multiplication | successor }
zero = { "0" }
variable = { ASCII_ALPHA_LOWER ~ "'"* }
addition = { "(" ~ term ~ "+" ~ term ~ ")" }
multiplication = { "(" ~ term ~ ("*"|"×"|"·") ~ term ~ ")" }
successor = { "S" ~ term }

WHITESPACE = _{ " " | NEWLINE }