athena
athena copied to clipboard
lib: basic: util.ath: add hsyl
Hypothetical syllogism is a rule defined in "Fundamental Proof Methods in Computer Science" p.215, but is not included in the language as part of util.ath.
dsyl is also defined on p.216 but is included.
Add hsyl to util.ath and implement as the book gives, but with dmatch.
This is useful for human written proofs, or exercises.
Thanks for this. I think it is a highly isolated update, but for the sake of good practice, let me fix the CI pipeline prior to merging. Consider this approved, though.