Technical Report TR-ARP-11-95

Automated Reasoning Project
Research School of Information Sciences and Engineering
and Centre for Information Science Research
Australian National University

June 19, 1995

MaGIC, MATRIX GENERATOR FOR IMPLICATION CONNECTIVES: RELEASE 2.1 NOTES AND GUIDE

John Slaney

Abstract This is the documentation for release 2.1 of the program MaGIC (Matrix Generator for Implication Connectives). It is also included with the source of the program which is available from arp.anu.edu.au by ftp. MaGIC allows the user to specify a system of logic as a Hilbert system with axioms and rules of inference, and it then searches for small algebraic models of that logic. Many axioms involving standard connectives are hard-coded, and a number of logics defined in terms of them are made available. Further connectives and further axioms and rules may be defined by the user. It is easy to customise MaGIC by adding code to implement more axioms and more logics. The documentation explains how to do this.

Release 2.1 is a considerable advance on release 2.0 which was made three years ago. All current MaGIC users are urged to upgrade to 2.1 now, as 2.0 will not be actively supported in future.