search

LeePatPat / NatDud

System L-style Natural Deduction Learning Tool - validates and gives feedback on proofs
MIT License
1 stars 0 forks source link

¬(X→X)→Y is a WFF but is rejected anyway #4

Open LeePatPat opened 6 years ago

LeePatPat commented 6 years ago

As the title says...

LeePatPat commented 6 years ago

¬(¬P ∨ ¬Q) → (P ∧ Q)

Same with this. There is an issue with negated parentheses to implication formulae.