search

Ayertienna / IS5

Intuitionistic S5 logic formalization
4 stars 0 forks source link

Automate proofs #1

Closed Ayertienna closed 12 years ago

Ayertienna commented 12 years ago

Proofs in labeled version are not automated enough and, frankly, quite ugly. They need a rewrite, possibly with more automation (Hint Resolve + writing own tactics for common tasks)

Ayertienna commented 12 years ago

This will be done as part of #30, closing