@inproceedings{06316301f9d1476d802d3ab27e06d234,
title = "A lattice-theoretic analysis of ATMS problem solving",
abstract = "This paper presents a lattice-theoretic formalization of the ATMS which allows us to define the semantics of the ATMS, the ATMS labeling operation, as well as focusing algorithms for the ATMS. These focusing algorithms are integrated cleanly within the proposed framework by assigning a real-valued cost to the lattice boundary sets, and allow performance improvements even for cases where there is little domain-dependent knowledge. The resulting BF-ATMS algorithm explores a search space of size polynomial in the number of assumptions, even for problems which are proven to have labels of size exponential in the number of assumptions. Empirical testing indicates significant speedups over the standard ATMS for such problems, while retaining the multiple-context capability of an ATMS, the important properties of consistency, minimality, soundness, as well as the property of bounded completeness.",
author = "Ngair, \{Teow Hin\} and Gregory Provan",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1993.; European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty, ECSQARU 1993 ; Conference date: 08-11-1993 Through 10-11-1993",
year = "1993",
doi = "10.1007/bfb0028211",
language = "English",
isbn = "9783540573951",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "282--289",
editor = "Michael Clarke and Rudolf Kruse and Serafin Moral",
booktitle = "Symbolic and Quantitative Approaches to Reasoning and Uncertainty - European Conference ECSQARU 1993, Proceedings",
address = "Germany",
}