Non-deterministic Choice

(30th-July-2020)

• In many AI programs, we want to separate the definition of a solution from how it is computed. Usually, the algorithms are non-deterministic, which means that there are choices in the program that are left unspecified. There are two sorts of non-determinism:

• An alternative proof method is to search backward or top-down from a query to determine if it is a logical consequence of the given definite clauses. This procedure is called propositional definite clause resolution or SLD resolution, where SL stands for Selecting an atom using a Linear strategy, and D stands for Definite clauses. It is an instance of the more general resolution method.