namespace logic.propositional
supports logic.propositional.dnf, logic.propositional.dnf.unicode
string okay = Well done!
string incorrect = This is incorrect.
string multiple = You have combined multiple steps (or made a mistake).
string finished = Are you aware that you already reached disjunctive normal form?
string commText = {
You have applied one of the commutativity rules correctly.
This step is not mandatory, but sometimes helps to simplify the formula.
}
string youRewroteInto = You rewrote @diffbefore into @diffafter.
string appliedRule = You have applied @recognized correctly.
string pressBack = Press the Back button and try again.
string suggested
| @hasexpected = However, the standard strategy suggests to use @expected.
| true = However, the standard strategy suggests a different step.
string askForHint
| not @oldready = You may ask for a hint.
| true = {} # empty text
feedback same = {
You have submitted a similar term. Maybe you inserted
or removed parentheses (the tool supports associativity)?
}
feedback ok = @okay @appliedRule
feedback noteq = @youRewroteInto @incorrect @pressBack @askForHint
feedback unknown = @youRewroteInto @multiple @pressBack @askForHint
feedback buggy = @youRewroteInto @incorrect @recognized @pressBack @askForHint
feedback detour
| @oldready = @appliedRule @finished
| recognize commor = @commText
| recognize command = @commText
| true = @appliedRule This is correct. @suggested
feedback hint
| @hasexpected = Use @expected.
| true = Sorry, no hint available.
feedback step
| @hasexpected = Use @expected to rewrite @diffbefore into @diffafter.
| true = Sorry, no hint available.
#-------------------------------------------------
# Rewrite rules rules
# text declarations define the textual appearance of identifiers
text falsezeroor, truezeroor, falsezeroand, truezeroand,
nottrue, notfalse = one of the False/True rules
text compland, complor = a complement rule
text notnot = double negation
text defimpl = implication elimination
text defequiv = equivalence elimination
text command, commor = commutativity
text assocor, assocand = associativity
text oroverand, genoroverand = distribution of or over and
text andoveror, genandoveror = distribution of and over or
text idempor, idempand = idempotency
text absorpor, absorpand = absorption
text demorganor, demorganand, gendemorganor, gendemorganand,
invdemorganor, invdemorganand = De Morgan
text invandoveror, invoroverand = distributivity
#-------------------------------------------------
# Buggy rules
string thinkthat = Did you think that
string notcase = This is not the case.
string tryto = Did you try to
text buggy.commimp = @thinkthat implication is commutative? @notcase
text buggy.assimp = @thinkthat implication is associative? @notcase
text buggy.implelim2 = {
Make sure that you use the rule for implication
elimination, you seemed to use equivalence elimination
}
text buggy.equivelim3 = {
Make sure that you use the rule for equivalence
elimination, you seemed to use implication elimination
}
text buggy.idemimp = @thinkthat implication is idempotent? @notcase
text buggy.idemequi = @thinkthat equivalence is idempotent? @notcase
text buggy.andsame = {
@thinkthat phi AND phi is equivalent to True? @notcase Idempotency of
AND means that phi AND phi is equivalent to phi.
}
text buggy.orsame = {
@thinkthat phi OR phi is equivalent to True? @notcase Idempotency of
OR means that phi OR phi is equivalent to phi.
}
text buggy.equivelim1 = {
Be careful with the elimination of an equivalence; take care
of the negations.
}
text buggy.equivelim2 = {
Be careful with the elimination of an equivalence; make sure that the
disjunctions and the conjunctions are at the right place.
}
text buggy.implelim = {
Be careful with the elimination of an implication;
make sure the negation is at the right place.
}
text buggy.implelim1 = {
@tryto eliminate an implication? In that case you used an
AND instead of an OR.
}
text buggy.demorgan1 = @tryto apply DeMorgan? Be careful with the negations.
text buggy.demorgan2 = {
@tryto apply DeMorgan? Make sure that you remove the outer
negation when applying this rule.
}
text buggy.demorgan3 = {
@tryto apply DeMorgan? Make sure that you replace AND by OR.
}
text buggy.demorgan4 = {
@tryto apply DeMorgan? Make sure that you replace OR by AND.
}
text buggy.demorgan5 = {
@tryto apply DeMorgan? Take care of the scope of the negations.
}
text buggy.notoverimpl = {
Did you think that you can distribute a negation over an
implication? This is not the case.
}
text buggy.parenth1 = Take care of the negations and the parentheses.
text buggy.parenth2 = {
Take care of the outer negation when you eliminate an equivalence.
}
text buggy.parenth3 = {
@tryto apply double negation? At this place this is not allowed,
because of the parenthesis between the negations.
}
text buggy.assoc = {
Did you change the parentheses? This is not allowed in a subformula
consisting of a disjunction and a conjunction.
}
text buggy.absor = {
@tryto apply absorption? You can't apply this rule at this place
since the resulting sub formula is not a subformula of the bigger term.
}
text buggy.distr = {
@tryto apply distribution? Take care of the place of the disjunctions
and the conjunctions.
}
text buggy.distrnot = @tryto apply distribution? Don't forget the negations!
text buggy.andcompl, buggy.orcompl = {
Be careful in the application of the complement-rules
}
text buggy.trueprop, buggy.falseprop = {
Be careful in the application of the True-False rules
}