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