Projects: BU CS 511 - Spring 2011

From Accessible Integrated Formal Reasoning Environments

Jump to: navigation, search

This page contains information and examples pertaining to aartifact projects from the Spring 2011 iteration of the Boston University course CS 511. Descriptions and requirements for the individual projects can be found in the following articles:

NOTE: These articles will be updated and extended over time. However, once a requirement is listed, it will never change and will not be removed.

Contents

[edit] Overview

The purpose of the projects is to implement at least some of the components of the aartifact system using modern tools and technologies such as Python, jQuery, GWT, etc. These components should be correctly implemented, robust, and well-documented.

Implementing JavaScript versions of the parser, validation procedure, and context will make the system more scalable and suitable for use in a classroom setting. Implementing a Python module will make it possible to use the features of the system for formal reasoning in a programming context.

[edit] Writing the Report

Your report should contain at least the following information. You may include anything else that you consider important or helpful.

  1. Introduction: Describe at a high level what your project does.
  2. Description: List the components and algorithms of your project and how they interact with one another and the user. Describe how they were implemented (e.g. which algorithm was used). Do some basic analysis of the efficiency and practicality of your algorithms and components.
  3. Usage: Provide examples that demonstrate how your project can be used. From the perspective of the user, what are the limitations and efficiency concerns that might affect usability?
  4. Resources and References: List and briefly describe the third party languages, platforms, systems, libraries, or technologies you used in your project. Also list any projects or systems you used as a reference or starting point. Were there any difficulties in using any of these to complete your project?

[edit] Common Components

This section defines and describes components that are common to all aartifact projects. Slight deviation from these is appropriate if it is explicitly justified. In particular, simplifications or extensions that make it easier to write and read formulas are encouraged.

[edit] Parsers

The concrete syntax of the system represents logical expressions that deal with mathematical formulas and English phrases. It is defined using a simple variant of BNF notation.

A parser must convert concrete syntax from plain text into abstract syntax (a tree data structure) for formulas. This sequence of syntactic definitions can be used to build a parser in stages.

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. The syntax below is only an example. View the source code to see how this syntax is converted into a parser. 

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

[edit] Syntax for Logical Formulas

We now present the syntax in stages, beginning with simpler variants and expanding it to add more structures.

  • The most basic syntax is suitable for representing formulas in propositional logic. 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 can be built up by combining these predicates using four logical operators. Braces {...} can be used to group formulas. This concrete syntax allows users to write logical formulas such as [the ground is wet] implies {[it is raining] or [it rained]}. 
    <word> ::= a-zA-Z
 
 <formula> ::= [<word> <word> ... <word>]
             | <formula> and <formula>
             | <formula> or <formula>
             | <formula> implies <formula>
             | not <formula>
             | { <formula> }
  • The above syntax can be extended to allow predicates to be applied to arguments. The arguments of predicates are called terms. In the syntax defined below, only variables can be terms. This syntax allows logical formulas such as [$X$ is a set] and [$f$ is a function]. 
  <variable> ::= a-zA-Z 

      <term> ::= <variable>

      <word> ::= a-zA-Z
               | $<term>$
 
   <formula> ::= [<word> <word> ... <word>]
               | <formula> and <formula>
               | <formula> or <formula>
               | <formula> implies <formula>
               | not <formula>
               | { <formula> }
  • The syntax for formulas can be extended with two quantifiers. 
   <formula> ::= ...
               | for all $<variable>, ..., <variable>$, <formula>
               | exists $<variable>, ..., <variable>$, <formula>
  • The syntax for terms can be extended further to include mathematical symbols. 
  <constant> ::= 0 | 1 | 2 | \mathbb{N} | \mathbb{Z} | \mathbb{R} | ...
 
      <term> ::= <variable>
               | <constant>
               | <term> <term>
               | ( <term>, ..., <term>)

[edit] Validation Procedure

The JavaScript parsing example contains an evaluation function that converts the abstract syntax data structure into a result. An validation procedure serves the same purpose: it evaluates a formula into one of two boolean values ("true" or "false").

A validation procedure recursively processes the abstract syntax representation of a formula to determine whether it is logically true or false. Typically, each case in the set of axioms of a logic corresponds to one case in the definition of the recursive function. For example, suppose a logic has the following inference rule:

\frac{P \,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\,\, Q}{P \ \text{and} \ Q}

This rule can also be written in the following way:

P,Q \vdash P \ \text{and} \ Q

The bottom portion (in the first notation) or right-hand side (in the second notation) specifies the shape of the abstract syntax tree that a validation algorithm might handle. The top portion or left side represent the decomposition of the tree into two subtrees that can then be checked recursively. Thus, one case of the definition of a validation algorithm might look as follows: 

 validate(P and Q) = validate(P) && validate(Q)

[edit] Contexts and Closure Operations

Logically, a context is a large conjunction of formulas that are assumed to be true. Data structures for representing contexts are often implemented so that certain kinds of formulas chosen by the system designer can be manipulated easily or efficiently.

A context usually supports at least two operations: assumption and assertion. To assume a formula is to add it to the context (potentially with other formulas implied by the new formula being added); to assert a formula is to check whether it is found (or implied by) the context.

Because any context is just a conjunction of formulas, it can be extended with a library of formulas of a particular form. Each of the predicates P1 to PK can be applied to zero or more of the variables x1,...,xN. 

 for all $x1,...,xN$, 
    { P1(x1,...,xN) and ... and PK(x1,...,xN) }
 implies
    Q(x1,...,xN)

Whenever a new formula is assumed, the entire library of formulas is checked to see if any new conclusions can be added to the context.

This paper [1] describes a way to compute assertions quickly for a particular kind of context data structure. This report [2] describes the context used in the aartifact system implementation.

[edit] JavaScript Interface

The current prototype JavaScript interface (integrated into the Edit pages of this MediaWiki instance) can be found here.

Retrieved from "http://www.aartifact.org/wiki/index.php/Projects:_BU_CS_511_-_Spring_2011"
Personal tools
 
ongoing projects
user tools