Principia Mathematica II

Subject: Design Ideas
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
===========
This document describes some java technical design ideas of the
prototype.


Main Package Structure
======================

com.meyling.principia
 some "main" programs that could be called directly

com.meyling.principia.module:
 starting point of all module handling business

com.meyling.principia.argument
 defines and implements the idea of argument lists containing
 atoms and/or other argument lists (lisp like)
 has (basic) pattern matching methods

com.meyling.principia.logic.paragraph
 here are objects like "Axiom"s, "Sentence"s, "ProofLine"s,
 
com.meyling.principia.logic.basic
 the basic logic operators

com.meyling.principia.logic.rules
 the logical rules that could be used

com.meyling.principia.io
 contains input output related issues


Important class: "Argument"
===========================
The "Argument" interface introduces lisp like trees with some 
pattern matching operations. There are currently two kinds of
Atoms: Text and Counter. Additionally every list has a
certain type, which restricts its possible elements.
If you write the type of a list before the list you could get 
for example: 

IMPL(OR(PROP(1), PROP(2)), PROP(1))

It is a list of type IMPL that has the following two elements:
OR(PROP(1), PROP(2))
PROP(1)
The first element is a list that contains two elements:
PROP(1) and PROP(2). Each of these lists contains one Atom,
the Counter 1 and the Counter 2  respectively.
A list has certain attributes. First there is it's type.
In our example we start with a list of the type IMPL.
There is also the elements of that list. Each element is
a list itself or an atom. Both occurences are called
Argument. From every Argument you could say how many 
and which elements (Arguments) build it up. 


Creators
========
Creators are in every package which has implementations of 
the Argument interface. 
They are simular constructed, but may only use the Argument
to use the String mapping of other creators.
A creator could create any of these classes by different
(static) methods. One import one is by an input stream (here:
TextInput). This is the deseralization of an Argument.
The seralization job could also be done by a creator.
(The  ModuleCreator is a little bit different, but look at the 
SimpleModuleCreator.)
One could easily replace an creator by another that 
operates on XML files. That's just another serialization form
There should be a creator for every package to be independent
of other packages (at least as much independent as possible).
So it would be possible to change the packages independenty.


Tests
=====
The packages "basic" and "module" should have a PackageTest.
In package "basic" there is also a JUnit test "TestConjunction"
for the class "Conjunction". This unit test tests more than 
"Conjunction", other classes are needed to perform the tests. 
So the whole pattern matching stuff is also tested.
