refute

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Sat.Fmla.refute

Lean4

/-- If `f` is unsatisfiable, and every `v` which agrees with `ps` implies `¬⟦f⟧_v → p`, then `p`.
Equivalently, there exists a valuation `v` which agrees with `ps`,
and every such valuation yields `¬⟦f⟧_v` because `f` is unsatisfiable. -/
theorem refute {p : Prop} {ps} (f : Fmla) (hf : f.proof []) (hv : ∀ v, Valuation.implies v (Fmla.reify v f p) ps 0) :
    p :=
  (Valuation.mk_implies [] rfl (hv _)).1 (hf _)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru