KIF Form Grammar

variable

indvar
| seqvar

term

indvar
| constant
| charref
| string
| block
| quoterm
| funterm
| listterm
| logterm

quoterm

( "\\(\s*quote" listexpr "\\)" )
| ( "'" listexpr )
| ( "^" listexpr )

listexpr

atom
| ( "\\(" listexpr * "\\)" )
| ( "," listexpr )

atom

word
| charref
| string
| block

funterm

( "\\(\s*value" term term * [ seqvar ] "\\)" )
| ( "\\(" constant term * [ seqvar ] "\\)" )

listterm

"\\(\s*listof" term * [ seqvar ] "\\)"

logterm

( "\\(\s*if" logpair + [ term ] "\\)" )
| ( "\\(\s*cond" logitem * "\\)" )

logpair

sentence term

logitem

"\\(" sentence term "\\)"

sentence

constant
| equation
| inequality
| relsent
| logsent
| quantsent

equation

"\\(\s*=" term term "\\)"

inequality

"\\(\s*/=" term term "\\)"

relsent

( "\\(\s*holds" term term * [ seqvar ] "\\)" )
| ( "\\(" constant term * [ seqvar ] "\\)" )

logsent

( "\\(\s*not" sentence "\\)" )
| ( "\\(\s*and" sentence * "\\)" )
| ( "\\(\s*or" sentence * "\\)" )
| ( "\\(\s*=>" sentence * sentence "\\)" )
| ( "\\(\s*<=" sentence sentence * "\\)" )
| ( "\\(\s*<=>" sentence sentence "\\)" )

quantsent

( "\\(\s*forall" "\\(" varspec + "\\)" sentence "\\)" )
| ( "\\(\s*exists" "\\(" varspec + "\\)" sentence "\\)" )

varspec

variable
| ( "\\(" variable constant "\\)" )

form

sentence