Problem formalizing a representation
Nicolas FRANCOIS <[email protected]>
| Newsgroups | gmane.comp.lang.caml.inria |
|---|---|
| Message-ID | <[email protected]> |
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