8 Translations
the Translate
class indicates that a code block will contain translation exercises that require symbolizing natural language sentences.
8.1 Propositional Logic
You can create propositional logic translation problems by also adding the class Prop
, like so:
~~~{.Translate .Prop}
3.1 P/\Q : People want to know what's going on and questions are unavoidable
~~~
The number 3.1 indicates the exercise number, and the colon separates the solution from the text that will be presented for translation. The result of the above is:
To complete it, replace the text to the left of the submit solution button with your translation, press return to check, and then press “Submit Solution”. Propositional translations are considered correct if they are logically equivalent to the original answer. So for example, Q/\P
will be accepted above.
8.2 First-Order Translation
It is also possible to create first-order translation problems using the class FOL
, thus:
~~~{.Translate .FOL}
3.2 AxF(x) : Everything is fine
~~~
with the result:
These are completed as above. Equivalence of first-order sentences is undecidable, so we can’t check it, but we can catch most cases of “equivalent” translations by using some rewriting rules.1 So, for example ~Ex~F(x)
will be accepted above.
8.3 Exact Translations
Using the class Exact
, you can also create “translations” that don’t accept logically equivalent answers. These may be useful if you wish to, for example, ask a student what the missing premise in some inference is. So, for example you might write
~~~{.Translate .Exact}
3.3 P : To make a modus ponens inference with P→Q, you need...
~~~
to generate:
Exact translations use the same syntax as Prop
by default, but can be configured to use a large number of alternative syntaxes (see below)
8.4 Systems
The way that formulas are parsed can also be customized. This is done by setting the system
attribute to indicate which formal system you are drawing your syntax from. So for example,
~~~{.Translate .FOL system="magnusQL"}
3.5 AxBx : Everything is bananas
~~~
will generate:
For first-order translations, the available systems are: firstOrder
montagueQC
magnusQL
thomasBolducAndZachFOL
thomasBolducAndZachFOL2019
LogicBookPD
LogicBookPDPlus
hausmanPL
howardSnyderPL
ichikawaJenkinsQL
hardegreePL
goldfarbAltND
goldfarbNDPlus
and goldfarbAltNDPlus
.
For propositional translations, the available systems are: prop
montagueSC
LogicBookSD
LogicBookSDPlus
hausmanSL
howardSnyderSL
ichikawaJenkinsSL
hausmanSL
magnusSL
magnusSLPlus
thomasBolducAndZachTFL
thomasBolducAndZachTFL2019
tomassiPL
and hardegreeSL
.
For exact translations, the available systems are all of the above, together with modal logic systems .HardegreeSL
.HardegreePL
.HardegreeWTL
, .HardegreeL
.HardegreeK
.HardegreeT
.HardegreeB
.HardegreeD
.Hardegree4
.Hardegree5
, second order systems .SecondOrder
.PolySecondOrder
, and set theory systems ElementaryST
and SeparativeST
8.5 Advanced usage
8.5.0.1 Multiple Solutions
If you wish to allow students to find one translation of a sentence that admits several formalizations, you can use a comma-separated list of admissible solutions. So,
~~~{.Translate .FOL}
3.4 (P /\ Q) \/ R, P/\(Q\/R) : Jack jumped the fence and was caught by the watchman or got away.
~~~
generates
8.5.0.2 Options and Attributes
In addition to allowing for custom point values with points=VALUE
, and turning off submission with submission="none"
, translations also have the following options
Name | Effect |
---|---|
nocheck |
Disables checking solutions |
exam |
Allows for submission of work which is incomplete or incorrect |
checksyntax |
When exam is active, blocks submission of syntactically incorrect work |
These can be included in the space separated list supplied to the options
attribute.
8.5.0.3 Translation tests
Finally, you can impose one or more extra tests on a translation. This is done by setting the tests
attribute to indicate which tests you wish to require the translation to pass. The available tests for propositional translations are
Name | Effect |
---|---|
CNF |
Requires conjunctive normal form |
DNF |
Requires disjunctive normal form |
maxCon:N |
Requires that the translation contain N or fewer connectives |
maxNot:N |
Requires that the translation contain N or fewer negations |
maxAnd:N |
Requires that the translation contain N or fewer conjunctions |
maxIff:N |
Requires that the translation contain N or fewer biconditionals |
maxIf:N |
Requires that the translation contain N or fewer conditionals |
maxOr:N |
Requires that the translation contain N or fewer disjunctions |
maxFalse:N |
Requires that the translation contain N or fewer falsity constants |
maxAtom:N |
Requires that the translation contain N or fewer atomic sentences |
The available tests for first-order translations are all the propositional tests, plus:
Name | Effect |
---|---|
PNF |
Requires prenex normal form |
When using multiple tests, their names must be separated by spaces, so for example,
~~~{.Translate .FOL tests="PNF maxNeg:0"}
3.6 ~Ex~F(x) : Nothing is not bananas.
~~~
will generate:
8.5.0.4 Partial Solutions
It’s possible to include a partial solution to a translation problem, by including the partial solution after a |
following the problem. So for example,
~~~{.Translate .FOL options="nocheck"}
3.7 AxF(x) : Everything is fine
| For all x, x is fine
~~~
Generates
the procedure is roughly as follows:
- using the standard rules of passage, drive quantifiers in as far as possible in both the submitted solution
, and in the target sentence , generating two result sentences , - using the standard rules of passage, pull out quantifiers as far as possible, in every possible way, generating a set
of sentences from , and a set of sentences from - allowing permutation of quantifiers within blocks, look for pairs of sentences
with matching quantifier prefixes. Canonically rename the variables. Check the matricies of the resulting formulas for propositional equivalence.
- using the standard rules of passage, drive quantifiers in as far as possible in both the submitted solution