Search
next up previous
Next: Rick Blute - Nuclear Up: Applied Logic / Logique Previous: Applied Logic / Logique

Fahiem Bacchus - A search engine based on model checking



FAHIEM BACCHUS, Department of Computer Science, University of Toronto, Toronto Ontario
A search engine based on model checking


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 also be supplied by including temporal logic formulas that are used to help guide the search. 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.


next up previous
Next: Rick Blute - Nuclear Up: Applied Logic / Logique Previous: Applied Logic / Logique