Nieuwenhuis, Oliveras, and Tinelli (2006) showed how to describe enhancements of the Davis-Putnam-Logemann-Loveland algorithm using transition systems, instead of pseudocode. We design a similar framework for several algorithms that generate answer sets for logic programs: Smodels, Smodels_cc, Asp-sat with Learning, Cmodels, and a newly designed and implemented algorithm Sup. This approach to describing answer set solvers makes it easier to prove their correctness, to compare them, and to design new systems.
View:
PDF
Citation:
Theory and Practice of Logic Programming (2011).
Bibtex:

Yuliya Lierler Ph.D. Alumni ylierler [at] unomaha edu