[Caml-list] Problem formalizing a representation

[Nicolas FRANCOIS <nicolas.francois@free.fr>]

Hi.

I'd like to represent logical formulas for different logics.

A logic is syntactically represented by atoms, and rules involving (at
the very least) and, or, not, and possibly implies and equivalence...

What differs between my logics is the atoms :
- for propositional logic LP, atoms are just variables, and
  interpretations assign true or false to those variables ;
- the there is a logic LQ, where atoms are of the form
  "variable=r"
  r being a rational number (there may later be atoms of the form
  "variable >= r", and so on).

Then, with those logics, I can define new logics, for example, with LP,
I can define atoms of the form a^+, meaning a was false and becomes
true, or a^.1, meaning a was anything, but becomes true...

So what I would like to do is create some parametrized types (or
modules), taking atoms types as parameter, the methods for manipulating
logics (for example, computing a normal form) being defined in those
types (via modules, maybe ?), independently of the atoms types, and the
code for manipulating atoms being inside each atom type.

last but not least, certain methods would have to take two formulas
from a logic, and build with them a formula of a new type.

I don't know if I'm perfectly clear (as a matter of fact, I'm quite
sure I'm not :-(, but maybe I gave you a sufficiently clear image of
what I want to do for you to give me some tips...

The problem is I've never used parametrized modules or objects, so I
don't know how to start. If you could give me the initial thrust, maybe
I could fly :-)

Thank you for any tip, and sorry for my poor english.

\bye

-- 

Nicolas FRANCOIS                      |  /\ 
http://nicolas.francois.free.fr       | |__|
				      X--/\\
We are the Micro$oft.		        _\_V
Resistance is futile.		    
You will be assimilated.         darthvader penguin