Principia Mathematica II

Subject: ToDo List
Date:    2003-11-24
***********************************************************************

Prototype Warning
=================
This program suite is only a working prototype for the main project
*Hilbert II*. It concentrates on the basic logic foundation of 
mathematics. The software design of the main implementation will be 
highly different. The following information is only appropriate for 
this prototype. Look at 
 http://www.qedeq.org/
 http://sourceforge.net/projects/pmii/
to get the latest source code and information.


Description
===========

it is unclear if the following points still get implemented in the prototype!

- PDF/LaTeX Generation: \exists and \forall are changed!!!

- PDF Generation: change to A4 output format

- PDF Generation: \qed must be on the right edge

- PDF Generation: proof line references go to the first proof line! error!

- PDF Generation & HTML Generation: Used by list at end

- Make text only paragraphs

- is SubstLine ok? if a free variable is changed into a bound one
  this must be an error! one has to look at RenameBoundVariable
  RenameFreeVariable and ReplacePredicat

- proof lines with line number?
  A: yes we must change that

- write module transformation functions:
  - expand all proofs that reference internal sentence labels
  - expand all proofs that reference sentence labels

- new operator "DECLARE" for declaring a keyword that could be used
  further on, "ABBREVIATION" is an implicit declaration. Every
  mathematical operator and every proof rule must be declared before
  you could use it. Sometimes a declaration could have arguments:
  eg.: the rules of de Morgan require a reference to a proposition
  that proofs -(A & B) <=> -A v -B
  
  A: DECLARE for rules implemented, for operators we decided against doing
  it

- is getPartFormulaSize() neccessary, why don't use instance of Formula?

- allow no Counter with number==0

- make TestXMLrunnable in normal enviornment

- generate basic classes or methods with generators:
  write down parsing rules and parse them to generate
  code

- allow different proofs: this means also use of different imports
  why that? allow only different proofs!

- check entries of AbbrevitationList: do they use anything after
  (or in) current entry (check for recursivness)

- make new Abbrevitation for operators with variable
  argument number

- rename: AND -> LAND, OR -> LOR

- make new operators AND, OR with variable argument numbers

- more construction tests for proofs and their subarguments

- new tests for package tests

- new unit tests

- check all "TODO" s in source code

- new "definition" for predicate constants -> logic package

- adapt checkit doclet

- document PackageTest (and parameter -t)

- PackageTest: some more test files for Exceptions

- check error messages

- Input: add new Constructor for InputStream

- check: toString() must be final, if used in hashCode()

- set certain modifer to "protected" in certain methods of Argument
  (e.g. matchEnumerator)