From Automated Assistance for Formal Reasoning

This article documents the automated assistant (aartifact) for formal reasoning integrated into this instance of MediaWiki. The sources for the latest version of the system are available for download at the following location, released under the GNU General Public License:

Download: aartifact version 0.0.4

Previously released versions are archived: 0.0.3 0.0.2.

The quickest way to get started is to download and install the Haskell Platform, download the above source archive, and compile it using GHC (which is distributed as part of the Haskell Platform).

Contents 1 Brief documentation 1.1 Sources 1.2 Compiling the system 1.3 Running the system 1.4 Concrete syntax

Brief documentation

Sources

The system is implemented using Haskell, and only requires a few standard libraries (such as Parsec and System.Time) that usually come bundled with popular Haskell interpreters and compilers, such as the latest versions of GHC and WinHugs.

The source archive contains Haskell source files, a Makefile (for GHC), and a compilation script for Windows environments (also for GHC). The Haskell modules (*.hs files) follow the naming conventions described below.

• Main.hs: the main module; handle command-line arguments, reads input, and produces output by making appropriate invocations of the other modules.
• IO*.hs: modules with data structures and algorithms for reading input and producing formatted output.
• Exp*.hs: modules with data structures and algorithms that deal with logical expressions (including substitution, matching, and conversion).
• Context*.hs: modules with data structures and algorithms that are used to simulate the static and dynamic contexts.
• Validation*.hs: modules with data structures and algorithms for validating a document (including search algorithms for building derivations using inference rules).
• Others: general-purpose data structures and algorithms (e.g. sets, efficient association maps, rational numbers, labels).

Compiling the system

The source archive comes with a Makefile for Linux environments and a Make.bat batch script for Windows environments. Both scripts assume that GHC is installed and perform the equivalent of the following (in addition to some clean-up):

ghc -O2 --make Main -o aa

Running the system

To validate the contents of a single file, the system can be invoked from the command line with the path of the file as a string parameter:

aa examples/ex1.pf

To produce formatted output, the -html and -ansi options are available. The -ansi option produces colored text output using ANSI escape sequences, which may not work with all terminals.

aa -ansi examples/ex1.pf

aa -html examples/ex1.pf

It is possible to direct the output into a file using the -o option.

aa -html -o examples/out.html examples/ex1.pf

Using the -stat option, it is possible to output statistics collected over the course of the verification process. When this option is supplied, the data is automatically recorded in the file stat.dat in the executable's directory.

aa -stat examples/ex1.pf

Concrete syntax

Partial listing of the concrete syntax.

statement ::=
       Introduce $<varlist>$
     | Assert <langexp>
     | Assume <langexp>

varlist ::= <var> | <var>,<varlist>
langexp ::= $<exp>$
         |  <langexp> and <langexp>
         |  <langexp> , <langexp>
         |  <langexp> or <langexp>
         |  <langexp> implies <langexp>
         |  <langexp> implies that <langexp>
         |  <langexp> iff <langexp>
         |  <langexp> if and only if <langexp>
         |  for all $<varlist>$, <langexp>
         |  for any $<varlist>$, <langexp>
         |  there exist $<varlist>$ s.t. <langexp>
         |  there exists $<varlist>$ s.t. <langexp>

exp ::= 1 | 2.1 | 3.45 | ...

     | \emptyset
     | \infty
     | \N
     | \Z
     | \Q
     | \R

     | \max
     | \min
     | \log
     | GCF
     | LCM
     | dom
     | ran
     | powerset
     | \ast      -- Kleene star

     |        { <exp> }
     |        ( <exp> )
     |        [ <exp> ]
     |       \{ <exp> \}
     |        | <exp> |
     |  \lfloor <exp> \rfloor
     |  \lceil  <exp> \rceil
     |  \langle <exp> rangle  -- for vectors

     |  <exp> <exp>       -- function application or multiplication
     |  <exp>,<exp>       -- function application or multiplication
     |  <exp>_<exp>       -- subscript to access vector component
     |  <exp> + <exp>     -- addition
     |  <exp> - <exp>     -- subtraction and set union
     |  <exp> * <exp>     -- multiplication
     |  <exp> / <exp>     -- division
     |  <exp> \cdot <exp> -- multiplication
     |  <exp> \mod  <exp> -- modulus

     | <exp> \cup <exp>        -- set union
     | <exp> \cap <exp>        -- set intersection
     | <exp> \times <exp>      -- set product
     | <exp> \rightarrow <exp> -- space of functions
     | <exp> \circ <exp>       -- composition and vector concatenation

     | \sqrt{<exp>}
     | \sqrt[<exp>]{<exp>}

     | <exp> =    <exp>
     | <exp> <    <exp>
     | <exp> >    <exp>
     | <exp> \leq <exp>
     | <exp> \leq <exp>
     | <exp> \neq <exp>
     | <exp> \in  <exp>
     | <exp> \subseteq <exp>
     | <exp> \subset   <exp>