Title: A Search Engine based on Model Checking First Order Formulas
Fahiem Bacchus
University of Toronto
Abstract:
Search and declarative representations are two of the most important
themes in AI research. Many problems in AI (and Computer Science in
general) are most effectively solved by search, and declarative
representations of the knowledge required to specify and solve these
problems offer many advantages. In this talk I will show how a general
purpose search engine can be constructed from the simple idea of
evaluating logical formulas against finite, or more generally,
recursively enumerable models. The system can then be configured to
solve particular search problems by simply specifying those problems
using appropriate collections of logical formulas. Advice as to how to
solve the problem can be supplied using standard heuristics, or more
declaratively by including temporal logic formulas characterize
sensible state sequences contained in the search space. The resulting
system has much in common with the "programming in logic" paradigm
advanced by Prolog, but offers the user much more flexible control
over the underlying search procedure.