Is it a formula?

The whole input is a formula when the start symbol impl spans it, from 0 to its full length:

formula() :- impl(0, T), len(T).
?- formula().
  • yes for ~(p|q)&r|p or p->q->r
  • no for p&|q or (p|q.

Try it live in the playground.

This only recognises well-formed formulas; it does not yet build the tree.

For that we need a way to deal with structured data (Part 4).