theorem-prover 0.1.1

Implementation of a theorem prover for first-order logic.
Documentation 
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
30
31
32

program = _{ SOI ~ formula ~ EOI }
formula = { atom ~ (bin_op ~ atom)* }
atom = _{ unary_op? ~ primary }
primary = _{ top | bottom | predicate | "(" ~ formula ~ ")" }

top = { "true" }
bottom = { "false" }

unary_op = _{ neg | forall | exists }
neg = { "~" }
forall = { "forall " ~ variable ~ "." }
exists = { "exists " ~ variable ~ "." }

bin_op = _{ and | or | imply | iff }
iff = { "<->" }
imply = { "->" }
or = { "\\/" }
and = { "/\\" }

// These 4 sets partition abcdefghijklmnopqrstuvwxyz by convention
variable = { 'u'..'z' }
constant = { 'a'..'e' | "o" }
function = { function_id ~ "(" ~ args* ~ ")" }
function_id = { 'f'..'n' }
predicate = { predicate_id ~ "(" ~ args* ~ ")" }
predicate_id = { 'p'..'t' }

args = { term ~ ("," ~ term)* }

term = _{ variable | constant | function }

WHITESPACE = _{ " " }