Propositional parser

A formula is not a string of symbols but a structure, and the parser finds that structure. Working through the formula symbol by symbol, it builds the syntax tree: which connective is the main one, what its immediate parts are, and what each bracket is doing. Everything later depends on that reading. A valuation, a truth table and a proof all follow the structure the parser finds, which is why an ambiguous formula is useless to a logician and to a compiler alike.

Scope. The propositional language of chapter 2: the variables p, q and r, or p with a subscript index. Quantifiers, predicates and terms are not part of that language, so a first-order parser will be its own tool rather than a mode of this one.

Full brackets

Strict mode follows the fully bracketed grammar, in which every connective carries its own pair of brackets and no formula needs a precedence rule. Click through the steps, or use the pencil to enter a formula of your own.

Bracket conventions

Conventional mode reads formulas written the way people actually write them, with the brackets that precedence already determines left out. Try the same formula in both apps: the trees agree, and the brackets you dropped are the ones the convention puts back.

Using it

Both modes accept p, q and r, and p with a subscript index. Type mathematical symbols directly, or write LaTeX commands such as \land and \neg, which convert as you type. The pencil button unlocks the input and clears the previous trace; Start parsing freezes it and builds a new one. The text button swaps the diagram for a nested list of the same tree.

In the book

• Chapter 2 · Parsing develops the algorithm this app runs, and explains why it terminates.
• Chapter 2 · Conventional notation gives the precedence and grouping rules behind the second mode.
• The exercise on omitted brackets practices translating between the two notations, and the guided grammar exercise builds a parser for conventional notation.