Description: |
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]) |