unicode_fol_kit.relevant_faithfulness_theory

unicode_fol_kit.relevant_faithfulness_theory(theory_name='RelFaithfulness', formula=None)[source]

Emit the self-contained relevant-B deep/maximal/minimal + faithfulness theory.

When formula is given, its deep encoding is appended as definition example :: rpl. With a local Isabelle/HOL the theory is verified end to end by unicode_fol_kit.hol.isabelle_runner.check_theory().

Parameters:

  • theory_name (str)

  • formula (Node | None)

Return type:

str