computing satisfying instance?

Stream: new members

[Mark Aagaard]

Is there an existing mechanism to compute a satisfying instance of a propositional formula? For example $(p \vee q) \wedge \neg r$ would return $p \wedge \neg r$.

-mark

[Daniel Weber]

What do you need it for?

import Mathlib.Tactic

example {p q r : Bool} (h : (p ∨ q) ∧ ¬ r) : False := by
  slim_check

can give you an example assignment

[Mark Aagaard]

Thanks, Daniel. This is great.

I'm teaching an intro to logic and verification course and want to show off some of the features of Lean4 as it relates to exercises that the students have done by hand.

-mark