These notes are taken from the introduction to the MaGIC manual.
The manual comes with the package, or can be downloaded separately. [ DVI | PS]

The program MaGIC (Matrix Generator for Implication Connectives) is intended as a tool for logical research. It computes small algebras (normally with up to 14 elements) suitable for modelling certain non-classical logics. Along the way, it eliminates from the output any algebra isomorphic to one already generated, thus returning only one from each isomorphism class. Optionally, the user may specify a formula which is to be imvalid in each structure found. This enables MaGIC to be used for such purposes as showing invalidity of unwanted formulae, proving one system stonger than another and proving the independence of axioms. It can also be used to generate all the small algebras modelling some chosen logic. These can then be used as input for other programs: for instance, they can be used as a database for many purposes including those of refuting non-theorems. They can also be presented in a human-readable format so that they may be perused, for example to suggest metatheorems to an imaginative logician or just to gain a ``feel'' for this or that system. MaGIC has already been used in the course of researches reported elsewhere (for example, in the paper ``Finite Models for some Substructural Logics'' TR-ARP-04-94 [DVI | PS])

The program , is available.

It is suggested that if you install or use MaGIC you let us know that you have it, so that we can distribute information about updates, patches, etc. to as many sites as possible.

Dr J K Slaney                      Phone (Aus.):  (026) 125 8607
Logic and Computation Group        Phone (Int.): +61 26 125 8607
School of Computer Science         Fax (Aus.):    (026) 125 8651
Australian National University     Fax (Int.):   +61 26 125 8651
Canberra, ACT, 0200, AUSTRALIA