Syntax of First-Order Logic (FOL)

The Prolog syntax of first-order formulas is defined below in BNF.

<fol> ::= all(<var>,<fol>) |
          some(<var>,<fol>) |
          and(<fol>,<fol>) |
          or(<fol>,<fol>) |
          imp(<fol>,<fol>) |
          not(<fol>) |
          <functor>(<var>{,<var>}) |
          eq(<var>,<var>)

Variables are represented as Prolog variables (i.e. starting with uppercase characters or underscores), functors as Prolog atoms.

<var> ::= <prolog-variable>
<functor> ::= <prolog-atom>