DEDUCTION_FUNCTIONS:DeductionRulesDictInterface = <DeductionRulesDictInterface>{[DEDUCTION_RULES.ADDITION]: DF.addition,[DEDUCTION_RULES.ASSUMPTION]: () => true,[DEDUCTION_RULES.ASSOCIATIVITY]: DF.associativity,[DEDUCTION_RULES.COMMUTATIVITY]: DF.commutativity,[DEDUCTION_RULES.CONDITIONAL_PROOF]: DF.conditionalProof,[DEDUCTION_RULES.CONJUNCTION]: DF.conjunction,[DEDUCTION_RULES.CONSTRUCTIVE_DILEMMA]: DF.constructiveDilemma,[DEDUCTION_RULES.DEMORGANS]: DF.deMorgans,[DEDUCTION_RULES.DISJUNCTIVE_SYLLOGISM]: DF.disjunctiveSyllogism,// This assumes a structure like `p & (q V r)` instead of `(q V r) & p`// If we wanted to allow the latter, we could define a more permissive// version of this that tries to commute the arguments as well[DEDUCTION_RULES.DISTRIBUTION]: DF.distribution,[DEDUCTION_RULES.DOUBLE_NEGATION]: DF.doubleNegation,[DEDUCTION_RULES.EXPORTATION]: DF.exportation,[DEDUCTION_RULES.HYPOTHETICAL_SYLLOGISM]: DF.hypotheticalSyllogism,[DEDUCTION_RULES.INDIRECT_PROOF]: DF.indirectProof,[DEDUCTION_RULES.MATERIAL_EQUIVALENCE]: DF.materialEquivalence,[DEDUCTION_RULES.MATERIAL_IMPLICATION]: DF.materialImplication,[DEDUCTION_RULES.MODUS_PONENS]: DF.modusPonens,[DEDUCTION_RULES.MODUS_TOLLENS]: DF.modusTollens,[DEDUCTION_RULES.PREMISE]: () => true,[DEDUCTION_RULES.SIMPLIFICATION]: DF.simplification,[DEDUCTION_RULES.TRANSPOSITION]: DF.transposition,[DEDUCTION_RULES.TAUTOLOGY]: DF.tautology}
Rules of implication are easier to compute because they only apply to the
main operator and only go in "one direction."
If there isn't an obvious strategy for identifying the application of
a rule of replacement, we attempt to apply the rule to the target
in all possible ways and see if we can generate the source(s). Essentially,
we perform a depth-first-search of the space of possible applications of
the rule.
First, we try to apply the rule to the main operator, at the top level,
to see if we can generate a "match." If that fails, we check whether one
of the main operands matches the other. If it does, we recurse on
the other operand and try to generate a match.
For rules of replacement, we first define a function that checks whether
a match can be found by transforming on the main operator. Then we take
that function and apply a higher-order-function that performs the DFS
with that function/rule recursively on the formula.
Higher-order function that takes a SimpleDeductionRule and converts it to a
function that recursively checks whether it applies to a formula
and its subformulas.
Rules of implication are easier to compute because they only apply to the main operator and only go in "one direction."
If there isn't an obvious strategy for identifying the application of a rule of replacement, we attempt to apply the rule to the target in all possible ways and see if we can generate the source(s). Essentially, we perform a depth-first-search of the space of possible applications of the rule.
First, we try to apply the rule to the main operator, at the top level, to see if we can generate a "match." If that fails, we check whether one of the main operands matches the other. If it does, we recurse on the other operand and try to generate a match.
For rules of replacement, we first define a function that checks whether a match can be found by transforming on the main operator. Then we take that function and apply a higher-order-function that performs the DFS with that function/rule recursively on the formula.