Projects: Client-side Parsing and Verification

From Accessible Integrated Formal Reasoning Environments

This article describes the "Client-side Parsing and Verification" aartifact project for the Spring 2011 iteration of the Boston University course CS 511. A high-level outline for what your project report should contain can be found here.

NOTE: This article will be updated and extended over time. However, once a requirement is listed in this article, it will never change and will not be removed.

Contents 1 Requirement #1: Propositional Logic 1.1 Basic Parsing and Validation 1.2 Details about Parsing 2 Requirement #2: Arguments 3 Further Extensions

[edit] Requirement #1: Propositional Logic

[edit] Basic Parsing and Validation

Create a JavaScript application that can parse and evaluate propositional logic formulas written using the following syntax:

    <word> ::= a-zA-Z
 
 <formula> ::= [<word> <word> ... <word>]
             | <formula> and <formula>
             | <formula> or <formula>
             | <formula> implies <formula>
             | not <formula>
             | { <formula> }

Any sequence of one or more words (each word consisting of characters a-zA-Z) separated by spaces and surrounded by square brackets [...] represents a predicate. Formulas are built up by combining these predicates using the four logical operators. Braces {...} can be used to group formulas. This concrete syntax allows users to write logical formulas such as the following:

 [the ground is wet] implies {[it is raining] or [it rained]}

This application must interactively accept input from the user in some way (e.g. using an text input box), and must compute in real time whether the formula is true or false using a correctly implemented recursive validation procedure. You are encouraged to give the user visual feedback about syntax errors and the logical validity of the formula and its subformulas.

[edit] Details about Parsing

There is a parser library available for JavaScript: JS/CC. You may want to use it in your project. A smaller example of a JavaScript recursive descent parser that converts concrete syntax into an abstract syntax data structure can be found here. The small example parser handles the following simple syntax. View the source code to see how this syntax is converted into a parser.

  <number> ::= 0-9
    <term> ::= <number>
             | ( <term> )
             | <term> + <term>

Notice that for this small parser, the syntax has been converted slightly to avoid unbounded recursion. The left-hand side of the binary infix operator has been "factored out":

  <number> ::= 0-9
     <lhs> ::= <number>
             | ( <term> )
    <term> ::= <number>
             | ( <term> )
             | <lhs> + <term>

You will need to use the same approach for the infix binary operators and, or, and implies if you decide to use this example parser as a base.

[edit] Requirement #2: Arguments

Extend your syntax and parser to support the following constructs. This will allow a user to build a step-by-step argument involving assumptions and assertions that can be derived from those assumptions.

 <statement> ::= Assume <formula>.
               | Assert <formula>.
  <argument> ::= <statement> <statement> ... <statement>

Next, extend your validation procedure to support validation of arguments written using this syntax. This should not take much effort: think about how a sequence of assumptions and assertions can be converted into a logical formula that uses the existing logical operators.

[edit] Further Extensions

Beyond fulfilling the listed requirements, you have a lot of freedom in implementing other extensions or components. These may include better error messages and feedback, better text and graphical interfaces (such as a more "flexible" input interface that allows users to sketch and move around pieces of a proof text in a free-form manner), XML or other standards for exporting and importing data (e.g. use MathML 1, 2), and so forth. A list of examples is provided below:

• support for more logical systems:
  • parser support for:
    • formulas with terms (e.g. with specific constants and/or functions);
    • for infix relational predicates (e.g. "<");
  • (partial) validation support for other systems/models:
    • first-order logic on a subset of arithmetic over natural numbers;
    • first-order logic on a subset of set theory or algebra of sets;
• improvements to the user interface:
  • more "flexible" input mechanism for proofs;
  • better error messages or feedback about validation results (e.g. what is the counterexample if something is false);
  • a standardized representation of formulas and associated import/export capabilities.

Do not hesitate to email questions if you are not sure about your idea.