Title: A Search Engine based on Model Checking First Order Formulas

Fahiem Bacchus
University of Toronto


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.