I am faithfully working toward translation checking for SLAPP. The “parallel tree” approach for sentential logic (as in section 5.2 of Symbolic Logic) is mostly working, and I have moved on to the quantificational case.

Translation checking presents special challenges: First, it is not entirely formal — with ordinary language expressions on one side of the equation. Second, checking for semantic equality blows up in the quantificational case.

I have attempted to solve the first problem with the aid of some natural language processing software. This is not created by me (!) but comes in the form of a “black box” that operates within SLAPP. It does however significantly increase the size of the SLAPP file.

Second, as we know (for example, from part IV of the text) there can be no generally sufficient mechanical method to decide equivalence for the quantificational case. If we limit the universe to, say, 4 members (sufficient, I think to expose simple translation failures), there are finitely many models. But a 4-member universe with just a couple of 2-place relation symbols has over 4 trillion (2¹⁶ x 2¹⁶) models — still too many to check in a reasonable way. I am working on an approach whose underlying idea is related to “truth trees” (treated in many introductory logic texts, though not Symbolic Logic) — where branches may close without testing all the cases. But even this is not guaranteed to finish in a reasonable time. So I am in the midst of something along the lines of an experiment — looking for a strategy adequate to our purposes!