Courseware for Logic Education

A significant portion of our effort is spent developing software tools for logic education at the undergraduate level. We have produced the courseware packages:

Tarski's World,
Language, Proof and Logic.
The Language of First-Order Logic,
Turing's World,
Hyperproof

Of these packages only the first two Tarski's World and Language, Proof and Logic are currently in print.

Language, Proof and Logic

Language, Proof, and Logic is a textbook and software package, intended for use in undergraduate level logic courses. The text covers topics such as the boolean connectives, formal proof techniques, quantifiers, basic set theory, and induction. The last few chapters include material on soundness, completeness, and Godel's incompleteness theorems.

The book is a completely rewritten and much improved version of The Language of First-order Logic. Introductory material is presented in a more systematic and accessible fashion. The book is appropriate for a wide range of courses, from first logic courses for undergraduates (philosophy, mathematics, and computer science) to a first graduate logic course.

The package includes four pieces of software:

Tarski's World, a program that teaches the basic first-order language and its semantics;
Fitch, a natural deduction proof environment for giving and checking first-order proofs;
Boole, a program that facilitates the construction and checking of truth tables and related notions (tautology, tautological consequence, etc.);
Submit, a program that allows students to submit exercises done with the above programs to the Grade Grinder, the online grading service.

Grade reports are returned to the student and, if requested, to the student's instructor, eliminating the need for tedious checking of homework. All programs are available for the Windows, Macintosh and Linux platforms. Instructors do not need to use the programs themselves in order to be able to take advantage of their pedagogical value.

Tarski's World (Revised and Expanded Edition)

Tarski's World (Revised and Expanded Edition) supercedes previous editions of the Tarski's World package. The text is significantly revised, with the addition of many more exercises and an update to the old manual for the program. In addition, many of the exerciss can be graded automatically using out Grade Grinder automated grading service.

The package includes two pieces of software:

Tarski's World, a program that teaches the basic first-order language and its semantics;
Submit, a program that allows students to submit completed work to the Grade Grinder, the online grading service.

Tarski's World is an innovative and enjoyable way to introduce your students to the language of first-order logic. The Tarski's World application allows the students to build three-dimensional worlds and to describe them in first-order logic. They evaluate the sentences in the constructed worlds and if their evaluation is incorrect, the program provides them with a game that leads them to understand where they went wrong. Using this program students quickly master the meaning of the connectives and quantifiers, and soon become fluent in the symbolic language at the core of modern logic.

Hyperproof

Hyperproof is a system for learning the principles of analytical reasoning and proof construction, consisting of a text and a Macintosh software program. Unlike traditional treatments of first-order logic, Hyperproof combines graphical and sentential information, presenting a set of logical rules for integrating these different forms of information. This strategy allows students to focus on the information content of proofs rather than the syntactic structure of sentences. It also reflects the heterogeneity of information encountered in everyday reasoning.

Using Hyperproof the student learns to construct proofs of both consequence and non-consequence using an intuitive proof system that extends the standard set of sentential rules to incorporate information represented graphically. Proofs of consistency and inconsistency are also covered as well as independence proofs. The Hyperproof software checks the logical validity of each type of proof.

The Hyperproof courseware package is currently out of print. The software is only available for the Macintosh Classic operating system (Macos 8.x or 9.x)

Turing's World

Turing's World is a self-contained introduction to Turing machines, one of the fundamental notions of logic and computer science. The text and accompanying diskette allow the user to design, debug, and run sophisticated Turing machines in a graphical environment on the Macintosh.

Turing's World introduces users to the key concepts in computability theory through a sequence of over 100 exercises and projects. Within minutes, users learn to build simple Turing machines using a convenient package of graphical functions. Exercises then progress through a significant portion of elementary computability theory, covering such topics as the Halting problem, the Busy Beaver function, recursive functions, and undecidability.

The Turing's World courseware package is currently out of print. The software is only available for the Macintosh Classic operating system (Macos 8.x or 9.x)

The Language of First-Order Logic

The Language of First-order Logic presents a new approach to teaching first-order logic. Taking advantage of the accompanying program Tarski's World, the text skillfully balances the semantic conception of logic with methods of proof. The book contains eleven chapters, in four parts. Part I is about propositional logic and Part II covers quantifier logic. Part III contains chapters on set theory and inductive definitions. Part IV contains advanced topics in logic, including topics of importance in applications of logic in computer science. The Language of First-order Logic contains hundreds of problems and exercises.

The The Language of First-Order Logic courseware package has been superceded by Language, Proof and Logic, and is currently out of print.