Discussion: Formalizing Wu's Characteristic Set Method

Stream: general

[Julien Narboux]

Interesting work !
Is your goal to formalize the theory, or to implement the decision procedure as a computation within Lean ? Do you consider using an approach based on the verification of a certificate produced by an external implementaton of Wu's method ?

[Notification Bot]

A message was moved here from #announce > Formalizing Wu's Characteristic Set Method by Matthew Ballard.