MaGIC: Matrix Generator for Implication Connectives
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, AUSTRALIAJohn.Slaney@anu.edu.au