Zur deutschen Fassung dieser Seite...
You are visitor number to the Gateway to Logic.
Wenn Sie diesen Satz verstehen, interessiert Sie vielleicht die Deutsche Fassung des Logikübergangs.
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 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 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:
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).
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.
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.
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.