S1⁰ Based Systems

Encoding S1⁰

• Axioms and rules for S1⁰ (S1-0.sys)
• Subsitution of strict equivalents by equality reasoning
  • HELP! Is this OK, or must the terms be ground?
• Definitions for operators
  • ! [X] : not(not(X)) = X is derivable

Encoding Modal Logics

• S1⁰ as above
• Axioms and rules for the chosen axiomatization,
  e.g., S1=S1-0M6.sys, S5=S1-0M6S3M9B.sys