LRATStep

Mathlib.Tactic.Sat.FromLRAT

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Sat.LRATStep

Lean4

/-- An LRAT step is either an addition or a deletion step. -/
inductive LRATStep
  |
  /-- An addition step, with the clause ID, the clause literal list, and the proof trace -/
  add (id : Nat) (lits : Array Int) (proof : Array Int) : LRATStep
  |
  /-- A (multiple) deletion step, which deletes all the listed clause IDs from the context -/
  del (ids : Array Nat) : LRATStep

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

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

Разделы

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

Аффилиация

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