Adding online exercises with automated grading to any logic course with Carnap

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:

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:

(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.)

The significance of the Curry-Howard isomorphism

In Gabriele M. Mras, Paul Weingartner & Bernhard Ritter (eds.), Philosophy of Logic and Mathematics. Proceedings of the 41st International Ludwig Wittgenstein Symposium. Berlin: De Gruyter. pp. 313-326 (2019)

The Curry-Howard isomorphism is a proof-theoretic result that establishes a connection between derivations in natural deduction and terms in typed lambda calculus. It is an important proof-theoretic result, but also underlies the development of type systems for programming languages. This fact suggests a potential importance of the result for a philosophy of code.

DOI 10.1515/9783110657883-018

Embargoed until November 2020. Please email for offprint.

Book cover

Sets, Logic, Computation. An Open Introduction to Metalogic

Sets, Logic, Computation is an introductory textbook on metalogic. It covers naive set theory, first-order logic, sequent calculus and natural deduction, the completeness, compactness, and Löwenheim-Skolem theorems, Turing machines, and the undecidability of the halting problem and of first-order logic. The audience is undergraduate students with some background in formal logic, e.g., what is covered by forall x.

LINK

Book cover

forall x: Calgary. An Introduction to Formal Logic

forall x: Calgary is a full-featured textbook on formal logic. It covers key notions of logic such as consequence and validity of arguments, the syntax of truth-functional propositional logic TFL and truth-table semantics, the syntax of first-order (predicate) logic FOL with identity (first-order interpretations), translating (formalizing) English in TFL and FOL, and Fitch-style natural deduction proof systems for both TFL and FOL. It also deals with some advanced topics such as truth-functional completeness. Exercises with solutions are available. It is provided in PDF (for screen reading, printing, and a special version for dyslexics) and in LaTeX source code.

LINK

BibTeX-friendly PDF management with Zotero

For years I’ve been jealous of colleagues with Macs who apparently all use BibDesk for managing their article PDF collections and BibTeX citations in one nice program. I think I’ve finally figured out how to do both things on Linux: Zotero, with the Better BibTeX and ZotFile add-ons.

Zotero is first of all a citation management system. It’s multi-platform, open-source, not tied to a commercial publisher, widely used and well-supported. Your article database lives on your computer, but is synced with a central server. So any changes you make to the citation database gets automatically mirrored to your other computers (even if they run different OSs), and you can access it online as well. The browser extension Zotero Connector lets you import & download references and PDFs from publishers’ websites, JSTOR, etc., with a single click. It does everything a reference manager does, e.g., give you bibliographies and citations in Word or LibreOffice.

Zotero manages PDFs in one of two ways: you can store a PDF in Zotero, or you can add links to PDFs on your local drive. The former option manages the PDFs for you, syncs them across computers, etc. But you only get 300MB of online storage for free, and that’s gone quickly. But if you keep your PDF directory synced across computers (e.g., if it lives in your Dropbox), linking the PDFs is just as good. If you add a PDF, Zotero will look up the metadata for you and add a reference to your database. It keeps an index of the content of PDFs, so search will pick up hits in the PDFs and not just in the metadata. If you have a reference already, Zotero can look it up online and help you find the PDF (or library call number). The ZotFile add-on makes this even easier. For instance, with one click you can add the most recently downloaded file to a reference item, move it into your PDF directory, and rename it according to some standard schema, say “Author – Year – Title.pdf”.

All of this has worked to some extent for a while, and also works with other reference managers. What has kept me from using them is that I want my reference manager to play nice with BibTeX. That means it should export BibTeX files with (a) proper capitalization, (b) LaTeX code where necessary (e.g., mathematical formulas in titles), (c) keep track of BibTeX fields like the crossref and note fields, which may contain LaTeX code itself (e.g., “Reprinted in \cite{...}“), and (d) not change cite keys on you. On the other hand, the database itself should look as normal as possible and avoid LaTeX code whenever possible (e.g., I want Gödel’s papers to be indexed under “Gödel”, not under “G{\”o}del”). When I tried Zotero the last time (and other reference managers), it would deal with (a) by enclosing the entire title field in braces. That meant BibTeX would not lowercase anything; and sometimes the style does require lowercasing things. I don’t remember if (b) or (c) ever worked.

Anyway, Zotero’s Better BibTeX extension does an excellent job.  You can put in “Gödel” as the author name, and it will export to “G{\”o}del”. It assigns cite keys according to a configurable pattern, but it keeps cite keys the same when importing BibTeX files. You can change them manually, and it will remember them. Additional BibTeX fields not already supported by Zotero are saved on import and included on export.  It will convert HTML tags (which Zotero understands as well) to LaTeX code on export (e.g., <i>...</i> to \emph{...}). If you need LaTeX code, just enclose it in <pre>...</pre> tags. It does a very good job with capitalization and is even smart enough to do its transformations only to English language titles. Especially nice: Better BibTeX will keep your exported BibTeX files up to date. So, e.g., you can put all the references for a paper you’re working on in a Zotero “collection”, tell Better BibTeX to export it, and the .bib file will stay up to date if you change or add something to the collection in Zotero.

Want to try it?

  • Install Zotero Standalone and Connector
  • Install ZotFile
  • Install Better BibTeX
  • Check your preferences, e.g., whether you want Zotero to rename PDFs or look up metadata when saving them.
  • If you want your PDFs to be linked and collected in, say, your Dropbox, set the attachment base directory in Preferences: Advanced: Files and Folders.
  • Tell ZotFile where your downloaded files and your PDF direcories are, so it knows where to look for the most recent PDF to attach (in Tools > ZotFile preferences) and where to move them to. Make sure you set the ZotFile PDF naming pattern there to something you like.
  • Set up an account on zotero.org and link your library to it in Preferences: Sync (but uncheck “Sync attachment files” if you don’t want your PDFs on zotero.org)
  • Tweak your Better BibTeX settings, esp. the cite key pattern to make sure imported cite keys are the way you want them.

Indian Conference on Logic and its Applications 2019

The Association for Logic in India (ALI) announces the eighth edition of its biennial International Conference on Logic and its Applications (ICLA), to be held at the Indian Institute of Technology Delhi from March 3 to 5, 2019.

ICLA is a forum for bringing together researchers from a wide variety of fields in which formal logic plays a significant role, along with mathematicians, computer scientists, philosophers and logicians studying foundations of formal logic in itself. A special feature of this conference is the inclusion of studies in systems of logic in the Indian tradition and historical research on logic.

As in the earlier events in this series, we shall have eminent scholars as invited speakers. Details of the last ICLA 2017 may be found at https://icla.cse.iitk.ac.in. See http://ali.cmi.ac.in for information on past events as well as updates on this conference.

The call for papers is here: https://easychair.org/cfp/icla2019