proof

Mathlib.Tactic.Sat.FromLRAT

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

Lean4

/-- `f.proof c` asserts that `c` is derivable from `f`. -/
def proof (f : Fmla) (c : Clause) : Prop :=
  ∀ v : Valuation, v.satisfies_fmla f → v.satisfies c

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

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

Разделы

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

Аффилиация

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