Evaluation of Pedagogical Logic Software
Paul Hovda , Philosophy

• Logic 2000 by David Kaplan, et. al. Designed to be used in conjunction with Logic: Techniques of Formal Reasoning by Kalish, Montague, and Mar.

• The package of software connected with the textbook Language, Proof, and Logic , by John Barwise and John Etchemendy. (LPL)

• The software for two textbooks Introduction to Logic: Propositional Logic and Introduction to Logic: Predicate Logic by Howard Pospesel.

Below I will outline what I gathered about the features of typical software, including some details about these three packages.

The Subject
The traditional subject matter in introductory formal logic courses can be divided into four different central subjects, each explored at two levels. The subjects are these:

• Symbolization and Translation
  Symbolization is the representation of sentences from English (or other natural languages) in formal languages. Translation is the reverse process.
  
  
• Formal grammar
  The exact syntax of the formal language, as well as conventional rules for abbreviating formal sentences (such as dropping the outermost parentheses of certain sentences).
  
  
• Derivations
  Formal derivations (or "proofs") are intended to be the formal analogues of natural-language rational arguments (paradigmatically, mathematical proofs). What counts as a derivation is defined by a small set of rules; typically, each rule corresponds to some clearly acceptable step of reasoning, for example, modus ponens.
  
  
• Formal semantics
  A semantics for a formal language gives exact definitions for "interpreting" symbols in that language. The usual result is a definition of "truth" relative to an "interpretation" or "model" that yields, for each interpretation or model, a definite truth-value for every sentence in the formal language.
  These four subjects are usually studied at each of two levels: first, that of propositional logic ; second, that of predicate , or quantifier , or first-order logic.

Subject-driven software features

• Completeness
  Appropriate logic software should cover all four subjects at both levels. Only a few of the available packages actually do so; the three I highlight here all do.

• Symbolization and Translation
  Symbolization (from English to the formal language) is never an exact science. It involves sensitivity to natural language, including such things as the recognition of equivalences (for the purposes of logic) between superficially different forms (e.g. seeing why one might treat "and" and "but" as the same), and awareness of the possibilities of syntactic ambiguity (e.g. seeing the ambiguity in "Bring your spouse or come alone and have a good time."). As a result, this tends to be one of the more difficult areas for which to create useful pedagogical software. The best packages offer only a little more than would be offered by a textbook: natural-language sentences to symbolize, and a set of correct symbolizations for each. Putting the questions on one page and the answers on another has virtually the same pedagogical effect as what the typical package does: a problem sentence is given, the student enters an answer, and the computer tells the student whether the given answer is or is not identical to a "correct" answer (determined by the software's author). Some software would also try to say whether the given answer is logically equivalent to a selected "correct" answer. (Such equivalence cannot generally be done by a computer in the setting of first-order logic, though it can be done quite easily in propositional logic.)
  
  Kaplan's software allows the student to give the answer in stages, working down through the grammatical tree (i.e. from the main connective, to subsentences, and eventually to atomic sentences) for the formal sentence the student gives as answer. At each stage, the student can give the English sentences that correspond to the formal subsentences connected by the preceding connective.
  
  Teaching the process of translating from formal symbols to natural language seems to be a subject computers are even less suited for. None of the software tested provides any significant component geared toward teaching this process. This is not too worrisome, however, as the skills needed are adequately developed by learning to symbolize natural language.
  
  
• Formal Grammar
  What counts as a formula or sentence of formal logic, and what its grammatical structure is, is specified by a small inductive definition. A proper appreciation of the definition and of the grammatical structure of a given formal formula is essential to a full understanding of formal logic. Pedagogical software should at least provide a means for checking whether a given string of symbols is indeed a well formed formula. Pospesel's software provides a separate module for this, while LPL provides it only as is needed for the other three main subject areas. (The notion of the main connective of a formula is reinforced in the software dealing with truth-tables.) Kaplan's software goes further, and provides graphical grammatical trees (which I find pedagogically valuable), as part of the symbolization module.
  
  
• Derivations
  Derivations involve the application of derivation rules: small sentence-transforming steps, specified in terms of the logical grammar of sentences, and corresponding to intuitively valid steps of reasoning. The application of a sequence of such steps can take one from premises to a conclusion which may not obviously follow from them. Learning to do derivations is greatly facilitated by software, because students can get immediate feedback at every step of the derivation; they do not need to wait to have an instructor tell them when they have misapplied a rule.
  
  All three packages do a decent job with derivations, but Kaplan's software stands out because of at least two of its many features. First, the set of rules of derivation is flexible; the instructor can allow derived rules of his or her liking, or not, on individual problems. Further, students can make their own derived rules, which helps them to understand the technically important concept of derived rules, and gives them a certain satisfaction. Second, students can perform derivations in "command mode", which amounts to specifying the justifying rule for a step without spelling out the sentence that results from the application of the rule; the software computes the result (or, where more than one result might arise, prompts the student for which result is desired). Besides speeding up the process, this may well help the student understand the nature of a derivation.
  Pospesel's package adds software for a different "derivation" technique: the method of truth-tree analysis. This method has been less emphasized traditionally, as far as I know, but seems to be gaining popularity. It provides an interesting alternative perspective, if nothing else.
  
  
• Formal Semantics
  
  Truth tables
  At the propositional level, the standard formal semantics involves (1) "assignments", which assign truth values to the atomic sentences or proposition letters, and (2) an inductive definition of the truth-value of a compound sentence in terms of its main connective and the truth-values of the immediate subsentences connected by this connective. The semantics is usually represented with truth-tables.
  All three packages have useful programs for teaching truth-tables, and this is one area where software seems especially pedagogically effective: students can see immediately where they may have made mistakes in filling in a truth-table.
  
  Models
  At the level of predicate logic, the standard formal semantics ( models for first-order languages) is significantly more complicated, and is usually not explicitly given in introductory classes. There are intuitive ideas that come reasonably close to the formal ideas, however, and these are routinely employed to help students understand what the symbols are supposed to mean. One of the central intuitive ideas is the specification of a counter-model or counter-example to a given set of sentences. If there is a model (a domain and an appropriate interpretation of predicates and names) in which some sentences are true (think of the premises of an argument), and in which some other sentence is false (think of the conclusion of an argument), then the argument from the first to the second is not valid. Students are taught how to attempt to construct counter-examples to arguments to show that they are invalid.
  Software can be useful here as well, but the problem is more challenging than in the case of truth-tables, in part because there is no standard way of representing models. The obvious pedagogical idea is to have some intuitive way of representing a model, and then the means for checking whether arbitrary sentences are true in the model. Then the problem of specifying a counter-example to an argument can be given, and the student can construct the model in the software, and the computer can check to see whether the model indeed works as a counter-example.
  
  Our three packages all provide such software. But they approach the problem of representing models in different ways. The LPL software has a nice method. Models are graphically represented as small "worlds" consisting of three-dimensional objects on a grid. The objects can vary in size and shape, and their locations on the squares of the grid are precise. Thus there are natural, vivid properties and relations to serve as interpretations for formal predicates. The predicates can be thought of as symbolizing English predicates like "is a cube" and "is behind". One benefit of this is that this software can also be used to help students with the symbolization of certain English sentences. For example, students can simply see that in a given model the English sentence "For every cube, there is a dodecahedron larger than it and behind it" is true (or false). Then they can attempt to symbolize the sentence, and, by checking to be sure that their symbolization gets the right truth-value, have some idea that they have symbolized correctly. Further, they can modify the world (model) and see whether the truth-value of the symbolization changes when appropriate. One drawback of the LPL software is that the formal predicates have fixed interpretations, and students do not get a chance to specify arbitrary interpretations; this is a minor issue, but it is important for a proper appreciation of the formal semantics that one realize that in principle, there is no constraint at all on the interpretation of formal predicates.
  
  Pospesel's software includes the means for both graphical and symbolic representations of models. The graphic representations are rather simple (objects of a few sorts in a three by three grid), but, again, because they are graphical, there are obvious, visually ascertainable properties and relations (like being above or being the same color as) to serve in giving interpretations; thus, the software provides a way to appreciate the connection between the formal symbols and given interpreted meanings. The Pospesel software, unlike the LPL software, does not have formal predicates with fixed interpretations; rather, the student must choose interpretations for the formal predicates. This is especially helpful, I believe, for understanding the nature of the formal semantics, though the software is somewhat limited even here, as one cannot choose arbitary interpretations, but rather only ones that correspond to a given list of English predicates appropriate for the domain. The Pospesel software also allows students to construct models represented symbolically (rather than graphically), using, for example, the integers from -100 to 100 and mathematical properties for the interpretation.
  Kaplan's software for model-building provides only a symbolic representation of models. The models have domains consisting of a few natural numbers. The interpretation of the predicates is a matter of assigning an extension directly (object by object, pair by pair, etc.), not by means of some property expressed by an English predicate (like "is odd"). Thus, with this software, unlike the other two, students can easily appreciate the sense in which any arbitrary interpretation of formal predicates is allowed by the formal semantics. But this strength is balanced by a weakness: since interpretation cannot proceed by means of a familiar, or, better yet, graphically represented property, students may well have a harder time seeing what is going on at first.
  The best software for model-building would combine the best features of these three packages: it would provide both graphical and non-graphical representations of models, with an apparatus for having predicates with fixed interpretations, interpretations by means of familiar and graphically presented properties, and completely arbitrary interpretations.
  

   

Back to List of Projects

Return to Murdock Grant home page