PropCards.jar implements one of Martin Gardner's card-based logic machines from his book Logic Machines and Diagrams. He explains the system like so:
Grid cards can be designed to operate on the same basis as the Venn diagrams (or Jevons's logical alphabet). They are awkward to use on syllogisms, but work fairly well with elementary problems in the propositional or truth-value calculus. If there are more than three terms, however, the number of cards required is so large that they serve no useful purpose. The figure below shows a set of triangular-shaped cards of this type for handling up to three terms in the propositional calculus. Premises must be no more complicated than a binary relation or the assertion of truth or falsity for a single term. Only nine cards are shown in the illustration, but you should have on hand several duplicates of each card except the first one, since the same card may be required for more than one premise. Cards 2 and 3 assert the truth value of a single term. Cards 4 through 9 are for binary relations. The basic form of the relation is shown on the edge, with less commonly encountered equivalent statements lettered on the same edge inside of parentheses. To solve a problem, pick out the required card for each premise, turning the card so that the premise appears on the bottom edge or base of the triangle. After all the premises have been assembled (it does not matter in what order), place them on top of card 1. Combinations visible through the windows are combinations consistent with the premises. Inspecting them will tell you what can be inferred about the terms. A sample problem should make this procedure clear. Suppose we wish to determine, if possible, the truth values of B and C from the following premises: These premises are found on cards 2, 6, 9. We turn each card until the desired statement is at the bottom, then place all three cards on card 1. Only a single combination, A~BC, is visible through the grid. We therefore infer that B is false and C is true. When no combinations at all are visible through the windows it indicates that at least two premises are contradictory. The entire procedure corresponds exactly to Jevons's elimination method and to the use of Venn circles for truth-value problems. Discussions of these procedures in Chapters 2 and 3 may be reviewed for additional details on how to handle the triangular cards. Window cards have little value except as novelties, although they suggest how easily a punch-card machine could be devised that would take care of more complicated problems of formal logic with considerable efficiency. The most promising line of development, however, is offered by the recent electric network machines which provide the subject matter of the next chapter.
A is true (A)
If B is true, then A is false (B ⊃ ~A)
Either B or C or both are true (B ∨ C)
Gardner's example is shown in the following screenshot from the application:
The stack of cards on the right is my addition, to make it possible to rearrange and delete cards in the pile in the middle of thewindow. Of course, there's no logical reason for rearranging the stack (which represents a conjunction), but a card can only be rotated when it's at the top of the pile.
Incidentally, the screenshot has been reduced in size a little, so the logic statements printed on each card are a tad easier to read in the actual app.
"Logic Machines and Diagrams" is a great read, and strongly recommended.