A couple of years ago I posted a roundup of interactive logic courseware with an automatic grading component. The favorite commercial solution is Barwise & Etchemendy’s Language, Proof, and Logic textbook that comes with software for doing truth tables, natural deduction proofs, and semantics for propositional and first-order logic, which also automatically grades student’s solutions. The problem is, that (a) it costs money and (b) will only grade problems from that textbook. I already pointed to the open-source, and free-to-use alternative Carnap by Graham Leach-Krouse and Jake Ehrlich. Graham wrote a guest post on Daily Nous about it a while ago. I’ve now used this myself with great success and thought I’d write up my experience.
Carnap is an online tool that allows you to do the following. You can upload webpages (written in a variant of Markdown) which may include logic problems of various sorts. These are, right now:
- Translation exercises (i.e., you provide a sentence in English and the student’s task is to symbolize it in propositional or first-order logic).
- Truth tables (you give sentence(s) of propositional logic, the student must fill in a truth table, and use it to determine, say, if an argument is valid, a sentence is a tautology, or if two sentences are equivalent, etc.).
- Derivations (you provide a sentence or argument and the student has to construct a formal proof for it).
- Model construction (you provide a sentence or argument, the student has to give a domain and extensions of predicates to make the sentence true, false, or show that the argument is invalid, etc.).
- Basic multiple choice and short-answer questions.
Carnap comes with its own textbook and a collection of pre-made problem sets. But you can make up your own problem sets. That’s of course a bit of work, but you have complete control over the problems you want to assign. Here are some sample exercises that go with the Calgary version of forall x:
- Propositional symbolizations
- Truth tables
- Fitch-style natural deduction proofs for propositional logic
- Symbolization in first-order logic
- Model construction
- Natural deduction proofs for first-order logic
These are pages I give to my students to get them to become familiar with Carnap before they have to actually do problems for credit. The main difference is that for a real problem set, each exercise has a “submit” button that the student can click once they’ve found a correct solution.
To get an idea of how these problem sets are written, have a look at the documentation.
As you see, the problems are interactive: the student enters the solution, and Carnap will tell them if the solution is correct. In the case of derivations, it will also provide some feedback, e.g., tell the student why a particular application of a rule is incorrect.
You can assign a point value to each problem. Carnap also allows you to set up a course, let students sign up for the course, and lets you assign the pages you’ve created as problem sets. It will allow students to submit problems they have correctly solved, and Carnap will tally the point score earned. You can then download a spreadsheet of student scores per problem set and assign marks on the basis of that.
As you see, Carnap is incredibly flexible. Moreover, it supports the syntax and proof rules of a number of popular textbooks. I’ll highlight the free/open ones:
- Graham Leach-Krouse, Carnap: The Book
- Gary Hardegree, Introduction to Modal Logic
- P. D. Magnus, forall x: An Introduction to Formal Logic, and also its derivatives
(Of course, the last is my favorite.)
Commercial texts supported by Carnap, which you would be evil to make your students buy of course, are:
- Bergman, Moore, Nelson, The Logic Book (McGraw-Hill, $130)
- Goldfarb, Deductive Logic (Hackett, $39)
- Hausman, Kahane, Tidman, Logic and Philosophy (Wadsworth, $120)
- Howard-Snyder, Howard-Snyder, Wasserman, The Power of Logic (McGraw-Hill, $130)
- Kalish and Montague, Logic: Techniques of Formal Reasoning (Oxford, $90)
- Tomassi, Logic (Routledge, $54)
All of these textbooks use a linear version of natural deduction (Fitch, Lemmon, or Montague), but Carnap now also has proof editors for Gentzen-style sequent calculus and natural deduction proofs and checks them for correctness.
How does it support different textbooks? Basically, the document you upload just tells Carnap, say, what sentence you want the student to produce as a translation, or what sentence you want them to give a proof of. You can change the “system” in which they do that, and based on that Carnap will show them the symbols differently (e.g., will ask them to do a truth table for \((\lnot P \land Q) \to R\) or for \((\mathord\sim P \mathbin\& Q) \supset R\)), and and will accept and display proofs in different formats and allow different rules. Even if your favorite text doesn’t show up above it’s likely that it is already partially supported. Graham is also incredibly helpful and responsive; last term he introduced new proof system systems and other features based on my request, often within days. (Bug reports and feature requests are handled via GitHub.)
Carnap is already pretty smart. It will accept not only solutions to translation questions that are syntactically identical to the model solution, but any equivalent solution (the equivalence check is not perfect for the first-order case, but will generally accept any reasonable equivalent translation). Graham has recently introduced a few new features, e.g., you can randomize problems for different students, or require that some conditions are met for translation problems (e.g., that the translation only uses certain connectives or is in a normal form).
To get set up, just email Graham. Once you have an instructor account and are logged in, you’ll be able to see the actual problem sets I assign in my class. You’re welcome to copy and use them of course! (If you happen to use a different textbook, you’ll just have to adjust the terminology and change the “system” Carnap is supposed to use in each problem.)