Abstract Answer Set Solvers (2008)
Nieuwenhuis, Oliveras, and Tinelli showed how to describe enhancements of the Davis-Putnam-Logemann-Loveland algorithm using transition systems, instead of pseudocode. We design a similar framework for three algorithms that generate answer sets for logic programs: Smodels, Asp-sat, 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:
In Proceedings of International Conference on Logic Programming (ICLP'08), pp. 377-391 2008. Springer.
Bibtex:

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