Carnap Documentation
Carnap's Course Management Dashboard
Explains how instructors set up courses, upload problem sets, assign uploaded problem set or problem sets from the Carnap book them to their courses, and download grades.

Describes the format of problem sets that can be uploaded to and displayed by Carnap, and assigned to courses. This includes the MarkDown syntax, how to include problems in a problem set, how to display formulas, and how to include custom CSS or JavaScript on your problem sets.
Problem Types
Carnap supports various kinds of problems, which are described on the following pages:
 Syntax Checking exercises ask students to parse a formula.
 Translation exercises ask students for formulas which Carnap compares to model translations of English sentences. These can also be used for normal forms and equivalences.
 Truth Tables exercises ask students to fill in truth tables and answer questions on the basis of truth tables.
 Derivations exercises asks students to construct
proofs in formal systems, which Carnap checks for correctness
onthefly. Carnap can handle the following systems:
 Montague: Montaguestyle systems, two of which are used in the Carnap book.
 Logic Book: The Fitch system used in Bergmann, Moore, and Nelson's Logic Book.
 forall x: Fitch system used in Magnus's original forall x.
 forall x: Calgary: Fitch system used in the Calgary version of forall x by ThomasBolduc and Zach (and also in Tim Button's forall x: Cambridge.
 Fitchstyle systems of Gamut's Introduction to Logic.
 Systems based on HowardSnyder's The Power of Logic.
 Systems based on Hausman's Logic and Philosophy.
 Lemmonstyle systems based on Goldfarb's Deductive Logic.
 Lemmonstyle system based on Tomassi's Logic
 Hardegreestyle systems based on Hardegree's Modal Logic
 Sequent Calculus: Gentzen's sequent systems LK and LJ.
 GentzenPrawitz Natural Deduction: Gentzen's original treestyle natural deduction proofs as also used by Prawitz.
 Model Checking asks students to provide firstorder interpretations that make given formulas true or false, or show that arguments are invalid.
 Qualitative Problems provide ways for including multiplechoice, multiselect, short answer, and numerical questions on a problem set.
Installation Instructions