Variable IR`Readonly`

IR: (formulas: PropFormula[]) => PropFormula[] = implicationReversalRule

Type Declaration

- (formulas: PropFormula[]): PropFormula[]
- Applies the rule of Implication Reversal.
  
  Given a formula of the form ¬F => ¬G, it derives the implication G => F.
  
  This rule allows contraposition in Hilbert-style calculus, enabling the derivation of equivalent implications with reversed arguments.
  Parameters
  - formulas: PropFormula[]
    An array of propositional formulas, each with form ¬F => ¬G.
  Returns PropFormula[]
  An array of derived implications, each with form G => F.
  
  Throws
  if implication reversal is not applicable.