The future of FLiP

Here are some suggestions for projects to extend FLiP.  These are
largely independent of each other, so the order they appear here does
not indicate any priority or project plan.

Projects that extend the core of FLiP, and apply to all logics and programs:

- Add a parser, so we can input formulas as strings in the same format
  as they are now printed by nd, with operator symbols, infix synax,
  and implicity precedence (optional parentheses).  In the present
  version, formulas must be entered as Formula constructor expressions
  with operator names, prefix syntax, and lots of required
  parentheses.

- Make it easy to store the results of a proof as a derived rule in
  the database of rules, so it can be used in subsequent proofs in
  the same session.  In the present version, the only way to add a
  rule is to add code to a logic module and import it.

- Make it easier to define functions and relations in a session.  In
  the present verson, the only way to add these is to define classes
  in a module and import it (as in the grail.villagers module, for
  example).

- Support automated proof search, or semi-automated proof with tactics.

Projects that add logics or checkers:

- Add more logics: Peano arithmetic including a rule for induction, 
  sets, lists, etc.

- Revise nd or add another checker to support backward proof from
  goals to premises (proceeding in the order suggested by the proof
  format shown by the present ptree command).

- Add another checker eq for equational logic, along with logics that
  better support this style of reasoning.  There are many examples of
  equational logics in Gries and Schneider, A Logical Approach to
  Discrete Math, and Eric Hehner, A Practical Theory of Programming.