Gateway to Logic

Introduction

The Gateway to Logic is a collection of web-based logic programs offering a number of logical functions. These functions are divided into four main categories. If you are a new user to the Gateway, you should probably try out and play with each category of functions. Note that you can at any time return to this page by selecting Other programs. This link appears right beneath the headline of the respective page. If you are not sure which category to visit first, consider starting with the Server-side functions. They work with every browser, and they do not presuppose the familiarity with a particular logical calculus.

Server side

The server side functions operate on formulae of classical two-valued propositional logic. They work with any browser. Although the server side offers a few graphical functions (e.g. displaying syntax trees), its strengths lie in the field of syntactic operations like optimization (where it offers e.g. a Quine-McCluskey reducer), normal forms and showing truth-tables.

Client side

The client side functions are rather similar to those at the server side. There are two big differences, anyway: They are not restricted to classical two-valued logic, but they can deal with a number of popular multi-valued systems and even an infinite-valued system, too. Furthermore, they are implemented as a Java applet, thus requiring a Java-enabled browser. The strengths of the client side functions are the graphical functions (alpha graphs, Frege's notation), the animated visualization of several operations (e.g. evaluation and normal forms) and, of course, the support of multi-valued logical systems. The syntactical functions are rather weak: If you are into optimization and the like, you will find the server side much more useful.

Proof builder

The Proof Builder is a program for interactively constructing proofs. It is available in four (or five) versions, each implementing a popular and/or interesting calculus:

• the Lemmon-style Proof Builder uses the calculus of natural deduction in the version presented in E.J. Lemmon's book Beginning Logic that is particilarly popular in Europe;
• the Fitch-style proof builder supporting a subordinated calculus, also known as a Fitch-style calculus;
• the Peirce alpha-graph proof builder, implementing the much less known calculus of Alpha Graphs as presented by Charles Sanders Peirce (and extensively dealt with by Don D. Roberts' book The Existential Graphs of Charles S. Peirce; and, finally,
• both the Hilbert-style proof builder, implementing arbitrary axiomatic calculi for propositional logic, and its
• Principia Mathematica version preconfigured for using the Principia Mathematica axioms.

Although all three versions are documented rather well at this time, working with them requires some degree of familiarity with the respective calculus. There is a commercial version of the Fitch-style proof builder accompanied by a complete tutorial. If you are interested in obtaining a course CDROM, please visit the site of Tempest Media. If your browser doesn't support Java, you might consider to have a look at the Proof Checker below (supporting only Lemmon style proofs).

Proof Checker

The Proof Checker, umh, checks proofs submitted by the user - hence the name. It supports Lemmon's calculus only. As opposed to the Proof Builder, the Proof Checker requires the user to actually type in the proof she wants to check. For this reason, many people find the Proof Builder easier to use.

Theorem Prover

The automated theorem prover automatically derives arguments, preferably valid arguments. It is executed on the server side and does not require Java. The syntax is similar to that of the proof checker.

The difference between the theorem prover and the similar-named function of the server-side functions is that the prover supports predicate logic, whereas the server-side functions are restricted to propositional logic.

Author

The Gateway to Logic is © by Christian Gottschall. Any kind of feedback, problem report, or proposed improvement is welcome at any time. Please use the feedback form for contacting me.

2006/11/03 02:32:22
gottschall@gmx.de