Finite Algebras and AI: From Matrix Semantics to Stochastic Local Search - Artificial Intelligence and Symbolic Computation - page 12

Additional conditions to guarantee the soundness of the refutation process should
also be imposed (cf. [13]). The class of resolution logics consists of those calculi
which are indistinguishable on inconsistent sets from logics defined by finite ma-
trices. Furthermore, resolution algebras for logics defined by finite logical matri-
ces can be effectively constructed from the defining matrices (cf. [13]).

Lattices of Resolution Logics. For a logic P = L, ,let K P denote the

L P K P

class of all logics on which have the same inconsistent sets as . is a

≤ P i = L, i ,i =0 , 1,

bounded lattice under the ordering defined as follows: if

P 0 ≤P 1 iff P 1 is inferentially at least as strong as P 0 . The lattice K P , ≤

then is

a convenient tool to discuss the scope of the resolution method defined in terms
of resolution algebras: if

P is a resolution logic, then so are all the logics in K P .

From the logical standpoint, the systems in K P can be quite different; from the

refutational point of view, they can all be defined by the same resolution algebra.

Nonmonotonic Resolution Logics. Resolution algebras can also be used to
implement some nonmonotonic inference systems. Let

P = L, be an arbi-

trary cumulative inference system. The monotone base of P is the greatest logic

P B . The monotone bases of the

so-called supraclassical inference systems is classical propositional logic (cf. [8]).
The consistency preservation property limits the inference power by which

on L (with respect to ≤ ) such that P B ≤P

P

and P B have to have the same

inconsistent sets of formulas. Every cumulative, structural, and proper inference
system satisfies the consistency preservation property. Hence, every such system
can be provided with a resolution algebra based proof system, provided that its
monotone base is a resolution logic.

P B can differ (cf. [8,13]). It states that both P and

4 Problem Solving as Satisfiability

A reasoning task, such as a planning problem, can be solved by, first, expressing
it as a satisfiability problem in some logical matrix

M and, then, by solving it

using one of the satisfiability solvers for M . In spite of the fact that for many

finite matrices A,d , the satisfiability problem:

(SAT M ) for every formula α , determine whether or not there exists an inter-
pretation h such that h ( α ) ∈ d

is NP-complete, a number of complete and incomplete SAT M solvers have been
developed and their good performance in finding solutions to instances of many
problems in real-world domains empirically demonstrated.

Searching for Satisfying Interpretation. Given a matrix M = A,d for

a language starts

by generating a random interpretation h restricted to the variables of an input
formula α . Then, it locally modifies h by selecting a variable p of α , using some
selection heuristic select var ( α, h ), and changing its truth-value from h ( p )to

L , a stochastic local search algorithm for satisfiability in M