Laboratory of Mathematical Logic at PDMI

Пятница, 16 марта, комната 101. Начало в 17:00.

Докладчик: В. Жижкун.

A FIRST-ORDER DAVIS-PUTNAM-LOGEMANN-LOVELAND PROCEDURE
В докладе будет рассказано о Davis-Putnam-Logeman-Loveland (DPLL) procedure для первого порядка (FDPLL).
DPLL для пропозициональной логики представляет собой расщепление по контрарным литералам. FDPLL является обобщением DPLL, с расщеплением по неосновным (т.е., содержащим переменные) литералам.
В качестве преимуществ FDPLL приводятся скромные требования к памяти, наличие всего 2-х правил вывода и явное построение модели в случае, если опровержения формулы не существует.
Доклад основан на статье Peter Baumgartner "FDPLL - A First-Order Davis-Putnam-Logeman-Loveland Procedure".