Helsinki Logic Machine: A System for Logical Expertise, Series B, Number 1

摘要

Helsinki Logic Machine is an experimental reasoning system designed to provide assistance needed for application-oriented research in logic. The system includes theorem proving, model synthesis, model checking, and formula manipulation capabilities for classical, modal, temporal, epistemic, deontic, dynamic, and non-monotonic logic calculi. For example, decision procedures have been implemented for over 60 logical calculi. The system is implemented in Quintus Prolog (about 10,000 lines of code) on a VAX 8650 mainframe computer running under VMS operating system. The report can be used as the user's guide for Helsinki Logic Machine; in addition, the principles of implementation of the different reasoning capabilities are explained and references to further information are given.