Information Technology Reference

In-Depth Information

Beyond Matrix Semantics.
The interplay between logic and universal algebra

goes far beyond Matrix Semantics; a wealth of results harvested in disciplines

such as type theory, term rewriting, algebraic logic, or fuzzy logic, and subjects

such as bilattices, dynamic logics, or unification, have had and will continue to

have a significant impact on AI research.

3

Problem Solving as Consistency Verification

Automated Reasoning deals with the development and application of computer

programs to perform a variety of reasoning tasks frequently represented as in-

stances of consistency verification problem.

Refutational Principle.
Refutational theorem proving methods, such as reso-

lution, rely on a correspondence between valid inferences and finite inconsistent

sets. The
refutational principle
for an inference system

P

=

L,

states that

there is an algorithm that transformes every finite set
X ∪{α}

of formulas into

another finite set
X
α
of formulas in such a way that

(ref)
X α
iff
X
α
is inconsistent in

P

(i.e., for every formula
β, X
α
β
).

In the light of (ref), a refutational automated reasoning system answers a query

X α
by determining the consistency status of
X
α
.

Resolution Algebras.
Let

L

=

Terms
(
Var
)
,f
0
,...,f
n

be a propositional

language (let us assume that the disjunction, denoted by

∨

,isamongthecon-

nectives of

L

). A resolution algebra for

L

is a finite algebra of the form

Rs
=

{v
0
,...,v
k
},f
0
,...,f
n
, F

where:

called
verifiers
, for every
i ≤ n, f
i

and the corresponding connective
f
i
are of the same arity, and

{v
0
,...,v
k
}

is a set of formulas of

L

F

is a subset of

V
.
Rs
defines two types of inference rules. The
resolution rule

α
0
(
p
)
,...,α
k
(
p
)

α
0
(
p/v
0
)

∨ ...∨ α
k
(
p/v
k
)

is the case analysis on truth of a common variable
p
expressed using verifiers.

The other inference rules are the simplification rules defined by the operations

f
0
,...,f
n
(see [13]). A set
X
of formulas is refutable in
Rs
if and only if one of

the verifiers from

F

can be derived from
X
using the inference rules defined by

Rs
.

Resolution Logics.
A propositional logic

is said to be a
resolu-

tion logic
if there exists a resolution algebra
Rs
such that for every finite set
X

of formulas (which do not share variables with the verifiers),

P

=

L,

X
is inconsistent in

P

iff
X
is refutable in
Rs
.

Search WWH ::

Custom Search