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 
}