The "Vanilla" serialization is an unsurprising syntax for first-order logic. It serves as a reference point, being only trivially different from the language of first-order logic (FOL) as described in numerous logic texts and widely implemented in reasoners.
Most of these trivial differences are due to typographic constraints; I want Vanilla to be an ASCII syntax that looks somewhat like FOL. I also want to allow mnemonic and complex names for terms (not just subscripted letters). I've chosen to simply copy the formula syntax of Otter, with minor changes.
Another option would be to use a subset of Infix KIF, but its unclear to me how well accepted or supported that dialect is. (The proposed standard says "Note that Infix KIF is NOT intended for use in the exchange of knowledge between computers.")
|Vanilla LX||Classical Logic|
|all x exists y (P(x,y) | Q(x,y))||∀x ∃y (P(x,y) ∨ Q(x,y))|
|P(x) & Q(x) -> -R(x)||(P(x) ∧ Q(x)) ⊃ ¬ R(x)|
@@@ BNF to do, as difference?
The differences between Otter's formula syntax and Vanilla are:
LX development work is being done as part of the MIT/LCS DAML Project under the MIT/AFRL cooperative agreement number F30602- 00-2-0593. This work is not on the W3C recommendation track and is not the product of a W3C working group or interest group.
First: 2002/11/04; This: $Date: 2002/11/13 00:12:15 $