New to the Gateway?
The Gateway to Logic is a collection of web-based logic programs offering a number of logical functions (e.g. truth tables, normal forms, proof checking, proof building). These functions are divided into four main categories. If you are a new user to the Gateway, consider starting with the Server-side functions. They work with every browser.
On each category page, beneath the headline of the respective page, there are two important links: "Other programs" and "Help". You can at any time return to this overview page by selecting "Other programs". The link "Help" will open up a new page (or browser tab) showing a detailed documentation of the respective program category.
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.
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.
Proof builder (requires Java)
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).
Client side (requires Java)
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.
The Gateway to Logic is © by Christian Gottschall. Any kind of feedback, problem report, or proposed improvement is welcome at any time.