Re: [Caml-list] Problem formalizing a representation

[Oleg <oleg@okmij.org>]

> 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 ;

You have probably received lots of help already. Just in case, let me
mention that back in 2019 I gave a short course at a Dagstuhl summer
school on meta-programming on a similar topic. It was
formulated a bit differently: wires (instead of atoms) and logical
gates (as connectives).

        http://okmij.org/ftp/tagless-final/course2/index.html

Starting from zero, the course dealt with various transformations
(NAND conversion), constant propagation (or unit propagation, as
sometimes called) and finally the CNF conversion
(normalization). Actually the course finished with circuits (gate
assemblies with several inputs and outputs), full adder and applying
unit propagation/CNF to all these things, but you probably don't need
that. There was an exercise to make wires more interesting, like
32-bit busses.

As you can see from the course materials, I talked a lot about
parameterization.