This is extraordinarily difficult and sometimes impossible. Even first order logic is undecidable with regard to checking if a formula is decidable. That said, LEAN does leverage a SAT solver to try and do a bit of what you describe.
This is extraordinarily difficult and sometimes impossible. Even first order logic is undecidable with regard to checking if a formula is decidable. That said, LEAN does leverage a SAT solver to try and do a bit of what you describe.