Monadic Combinator Parser For FOL

The data structure needed to represent an FOL sentence is largely derived from the grammar above. The following data types are defined:

$$\begin{eqnarray*} data\, Sentence & = & Connective\, Sentece\, Connective\, Sent... ...\ type\, Predicate & = & String\\ type\, Function & = & String \end{eqnarray*}$$

The data structure is droppped because is sufficient once the and constructors are added. In the data type , two constructors: and are added. The parser does not make use of them, however, functions that convert a raw sentence to conjunctive normal form and implicative normal form would rename some given function names or constants into a unique numbering so that they can be updated when inserted into the knowledge base.

A monadic combinator parser of the form was implemented to convert a raw string that a user types into a system into the a data structure.The standard library ``ParseLib.hs'' that is distributed with hugs is used for the building of this parser. For handling parse (syntax) errors, the function , is used at the top level.

The following is a list of keywords that are reserved: ``TRUE'', ``FALSE'', ``NOT'', ``AND'', ``OR'', ``FORALL'', ``EXISTS'' (as well as the all-lowercase and capitalized versions of each keyword). It was decided that ``TRUE'' and ``FALSE'' are not allowed to be part of a sentence inputed by the user since doing so is redundant.

When matching constants, predicates and functions, the names must begin with an uppercase letter, while variables must begin with a lowercase letter.

In fact, as will be described in later sections, the interactive system that accepts commands from the user also uses monadic combinator parser of the form is used to parse user commands (although its syntax is much simpler.)