Vanilla LX Serialization

Introduction

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.")

Examples

Grammar

@@@ BNF to do, as difference?

Differences from Otter

The differences between Otter's formula syntax and Vanilla are:

1. Otter has special identifiers (the ones starting with "$")
2. Otter has syntactic sugar for lists: [first, second, third | rest]. (We'll add this back into LX Maple; lists don't belong in Vanilla, since they are not present in traditional first-order logic.)
3. Vanilla adds the @internal and @external directives as syntactic sugar. (@@@@ link to their special sections?)
4. In some cases, the precedence rules Otter uses seem to be different from those documented. Vanilla follows the documentations. (@@@@ detail and bug report?)

Issues