=Paper=
{{Paper
|id=Vol-1872/paper2
|storemode=property
|title=Self-Correcting Unsound Reasoning Agents
|pdfUrl=https://ceur-ws.org/Vol-1872/paper2.pdf
|volume=Vol-1872
|authors=Yannick Chevalier
|dblpUrl=https://dblp.org/rec/conf/lpnmr/Chevalier17
}}
==Self-Correcting Unsound Reasoning Agents==
<pdf width="1500px">https://ceur-ws.org/Vol-1872/paper2.pdf</pdf>
<pre>
      Self-Correcting Unsound Reasoning Agents

                                 Yannick Chevalier1

    Université Paul Sabatier? , IRIT, Toulouse, France yannick.chevalier@irit.fr



       Abstract. This paper introduces a formal framework for relating learn-
       ing and deduction in reasoning agents. Our goal is to capture imperfect
       reasoning as well as the progress, through introspection, towards a better
       reasoning ability. We capture the interleaving between these by a reason-
       ing/deduction connection and we show how this—and related—definition
       apply to a setting in which agents are modeled by first-order logic the-
       ories. In this setting, we give a sufficient condition on the connection
       ensuring that under fairness assumptions the limit of introspection steps
       is a sound and complete deduction system. Under the same assumption
       we prove every falsehood is eventually refuted, hence the self-correction
       property.

       Keywords: Reasoning Agents, Unsound Reasoning, First-Order Logic,
       Ordered Resolution, Saturation


1     Introduction
We consider in this paper a framework in which an agent is described by state-
ments in a logic. These statements reflect the agent’s view of the world, and can
either be true—when the statement is known to be true in all possible cases—or
just satisfiable—in which case we say the statement is merely believed. While the
knowledge must be a consistent set of statements, we allow the set of beliefs to
be inconsistent, as sometimes belief just reflects uncertainty, lack of knowledge,
or simply queries related to the knowledge. Reasoning is accordingly split into
two part:
 – an introspective part, that aims at producing new known statements from
   existing ones;
 – a deductive part, that aims at evaluating believed statements to eliminate
   those in contradiction with what is known to be true.
    Specifically, we aim at capturing the dynamicity of reasoning, that is the
interplay between these two aspects of reasoning. This agency framework is
actually very close to what is routine in automated deduction. A given (usu-
ally first-order) theory T is saturated by adding consequences of already known
clauses to obtain a new, hopefully finite, equivalent theory T 0 . The rationale for
the development of a saturation procedure is to obtain a theory T 0 that can be
used with a specific deduction strategy to answer queries.
?
    CIMI Project FMS
    This work is built from the strong connection in first-order logic between a
saturation procedure on the one hand, and the deduction strategy that can be
proven complete for saturated sets of clauses on the other hand. For instance,
linear ordered resolution is complete [2] for a set of clauses saturated up to re-
dundancy under ordered resolution: given a saturated theory T and a ground
clause C such that T ∪ ¬C is inconsistent, there exists a proof by ordered reso-
lution of the empty clause in which each inference contains at most one clause
from T . Similar results are obtained for superposition [2], equational theories [6,
5], with the possible addition of a selection function [8, 11]. In some works [1,
9], the output of the saturation process is directly a decision procedure for a set
of queries (in the mentioned cases, a decision procedure for ground queries). In
other cases it is proven that if a saturation procedure terminates then a given
proof strategy is efficient, and in many cases this proof strategy can be turned
into a decision procedures for ground query problems [2, 10, 3, 9].
    In contrast with these more recent approaches, the dynamicity of reasoning
that we consider is closer to the unfailing completion procedure [5] that applies to
equational theories and does not have a subsumption rule. In [5] it is proved that
a transformation of the theory can be formulated as a transformation of proofs
that reduce their complexity for a well-founded ordering. Thus the absence of a
subsumption rule, after which proofs may become more complex, is essential in
that approach. Technically we aim at obtaining a similar main theorem, i.e. that
the presentations computed step by step are eventually complete for refutation
of any contradicted formula.
    In the context of this paper, this means we are interested in the interleaving of
saturation steps (called introspection above) and query evaluation steps (called
deduction above). We introduce in this paper pairs (`i , `d ) of inference rules
that reflect this situation. The relation `i represents the inference rules employed
during the saturation process, while the relation `d represents the inference rules
involved in the deduction.
    Beside that technical justification for this paper, we note that we model
a situation in which the lack of omniscience of agents is not the result of a
partial knowledge, but rather stems from an incomplete form of deduction. This
approach was proposed by Konolige in [7], but does not seem to have been
pursued. In [7] what we call an agent state is called a deduction structure.
While Konolige focuses on the properties of a deduction structure, for example
by introducing a possible worlds semantics, this paper focuses on the analysis
on the possible evolutions of deduction structures and on the general criteria
on pairs (`i , `d ) needed to ensure that a contradictory formula will always be
eventually (for relation `i ) be refuted (using `d ).


Outline. In this paper we first give basic definitions relating to first-order logic,
and saturation in Sect. 2. We then present agent models and their evolution in
Sect. 3, and we prove that under assumptions made on the introspection and
deduction process, an agent may eventually remove all beliefs contradicting her
knowledge. We give an example in Sect. 4 of how the processes of saturation and
deduction in first-order logic fit in that model. We conclude in Sect. 5 with the
possible extensions of this paper.


2     Basic Definitions

2.1    First-Order Logic

First-order objects. We assume the reader is familiar with the basics of first-
order logic, and just recall them here to define notations. Variables are denoted
x, y, z and decorations thereof and constants denoted c etc. We let X and C be
denumerable sets of variables and constants, respectively. Given a set F of func-
tion symbols with arity and a set S of nullary symbols, we denote T (F, S) the
set of terms over S, i.e. the least set containing S and closed by the application
of functions in F. The set of terms is T (F, X ∪ C), and the set of ground terms
is T (F, C).
      Given a set P of predicate symbols with arity, if p ∈ P is of arity n and
t1 , . . . , tn are terms then p(t1 , . . . , tn ) is an atom. A literal is either an atom A or
its negation ¬A. We say the literal is positive in the first case and negative in the
latter case. A clause is a multiset of literals denoting their disjunction. Accord-
ingly the empty clause ∅ is always false. A theory is a set—or conjunction—of
clauses. An atom, literal, clause, or theory is ground whenever all its atoms are
constructed on ground terms. By skolemization every first-order logic theory can
be presented by an equisatisfiable set of clauses. Finally we say a theory T is
inconsistent, and write T |= ∅ if it has no model.


Unifier, resolution and factorization. A substitution σ is an idempotent func-
tion from variables to terms of finite support, i.e. σ(x) = x for all but a
finite number of variables. Substitutions are extended homomorphically (us-
ing σ(f (t1 , . . . , tn ) = f (σ(t1 ), . . . , σ(tn )) for function or predicate symbols and
σ(c) = c for constants) to terms, atoms, literals, and clauses. As usual, we prefer
to use the infix notation, and write tσ in lieu of σ(t). A substitution σ is a unifier
of two terms t, t0 if tσ = t0 σ. It is a most general unifier of t, t0 if for every unifier
τ of t, t0 there exists a substitution θ such that σθ = τ . As is well known the most
general syntactic unifier of two terms is unique up to a renaming of variables.
We extend this notion to atoms in the usual way. Resolution and factorization
(see Fig. 2.1) were formally defined by Robinson [12]. A deduction sequence from
T is a finite sequence (C1 , . . . , Cn ) of clauses such that each Ci is either in T
or the conclusion of a resolution or factorization inference with antecedents in
{C1 , . . . , Ci−1 }. Whenever one such sequence exists we write T ` Cn . Resolution
is complete for refutation, i.e. if T |= ∅ then T ` ∅. If Φ is a clause and T is
not inconsistent, we have that T |= Φ is equivalent to T, ¬Φ |= ∅, and thus by
completeness for refutation T, ¬Φ ` ∅. Trivially, if Φ is an atomic formula, i.e.
contains only one literal, this implies T ` Φ.
        Γ ∨ A ¬B ∨ ∆ σ = mgu(A, B)              Γ ∨ A ∨ B σ = mgu(A, B)
           (Γ ∨ ∆)σ                             (Γ ∨ A)σ
                    resolution                          factorisation

                 Fig. 1. Resolution and factorization inference rules


3     Agent Model
3.1   Modeling Reasoning
Agents are defined wrt to a logic L in which formulas are evaluated wrt to a set
M of models. We let SL be the set of statements in L, and P(SL ) be the set of
subsets of SL , and Con be the set of consistent subsets of L. First we define the
introspection relation as a change of a representation of a theory T that yields
a theory T 0 in which truth in a given model is preserved.

Definition 1. (Introspection relation) An introspection relation `i on the logic
L is a truth-preserving relation on the powerset P(SL ) , that is, for all T, T 0 , if
T `i T 0 , then for all m ∈ M we have m |= T if and only if m |= T 0 .

   The `i relation changes the world representation of an agent, presumably to
better it. We now introduce a deduction relation that uses a representation of
the world to reason about the truth of arbitrary statements in the language.

Definition 2. (Deduction relation) A deduction relation `d on the logic L is a
relation ⊆ P(SL ) × L that represents a sound proof procedure for L. Namely, if
T `d ϕ then for all m ∈ M , we have m |= T implies m |= ϕ.

    In addition to being truth preserving, an introspection relation should, in
order to be useful, reduce the difficulty of reasoning. We capture this intuition
as follows. Given T ∈ Con and ϕ ∈ L such that T |= ϕ, we measure the difficulty
of proving ϕ from T by the number of introspection steps needed to reach a set
T 0 ∈ Con such that T 0 `d ϕ.

Definition 3. (Distance to provability) Assume `i ⊆ Con × Con is an introspec-
tion relation, T |= ϕ, and that `d is a deduction relation. Then we let:
                                                 
n
                dist`i ,`d (ϕ, T ) = min{n | T `i T 0 and T 0 `d ϕ}

    We aim to prove that introspection steps always make proving easier, or at
least not more difficult. This implies a reasoning on all possible proofs, as is
the case for unfailing completion (see above). The usual orderings on proofs (for
example, a well-founded ordering on the clauses occurring in the proof [2, 3]) are
not strictly decreasing, and the distance provides an admittedly coarser ordering
sufficient for our purpose.
    We capture the relation between introspection and deduction outlined previ-
ously by defining reasoning connections. These impose the constraints that can
be summarized as follows:
 – a completeness constraint (first point in the definition below) by imposing,
   when T |= ϕ that at least one sequence of introspection steps will lead to a
   theory T 0 such that T 0 `d ϕ;
 – a uniform not-going-back constraint imposing that whatever introspection
   step is taken from T , the distance of the resulting T 0 to any formula ϕ will
   be less than or equal to the distance between T and ϕ;
 – a progress constraint stating that once a formula ϕ is chosen but not im-
   mediately provable, there exists an introspection step that will reduce the
   distance to provability.

      These points are stated formally in the following definition.

Definition 4. (Reasoning connection) A reasoning connection is a couple (`i
, `d ) where `i is an introspection relation, `d is a deduction relation, and such
that:

1. completeness:

                    ∀ϕ ∈ L, ∀T ∈ Con, T |= ϕ ⇒ dist`i ,`d (ϕ, T ) < +∞

2. not-going-back:

           ∀ϕ ∈ L, ∀T, T 0 ∈ Con, T `i T 0 ⇒ dist`i ,`d (ϕ, T 0 ) ≤ dist`i ,`d (ϕ, T )

3. progress:

          ∀T ∈ Con, ∀ϕ ∈ L, 0 < dist`i ,`d (ϕ, T ) < +∞ ⇒
                            (∃T 0 , dist`i ,`d (ϕ, T 0 ) < dist`i ,`d (ϕ, T ) ∧ T `i T 0 )

The role of Def. 4 is to provide one with simple conditions that are sufficient to
define reasoning agents in an arbitrary logic L who:

 – start with imperfect reasoning yet are able to increase their reasoning power;
 – and at the same time have a bounded deduction capacity as expressed by
   the (presumably incomplete in general) deduction relation.


3.2     Agent State and Trajectory

We now proceed to define an agent state. We consider a naive model of agent
whose beliefs are statements considered satisfiable, i.e. that were not proven
invalid. This choice of accepting all non-refuted statements transforms a sound
but incomplete reasoning procedure into an unsound yet complete one, that will
accept all valid entailments, but also may accept in the set of beliefs unsatisfiable
statements.

Definition 5. (Agent state) Let (`i , `d ) be a reasoning connection. A (`i , `d )-
agent state is a couple (T, B) where T ∈ Con and B ⊆ L, and for all ϕ ∈ B we
have T ¬ `d ¬ϕ.
   In order to simplify notations in relation with this definition, we note Ref `d (T )
the set of statements ϕ that can be refuted from T given `d . That is,

                             Ref `d (T ) = {ϕ | T `d ¬ϕ}

We present in this paper a first agent model that does not react to outside events
nor with other agents. Accordingly, an agent evolves either by receiving a new
aceptable belief or by changing her world’s view through introspection.

Definition 6. (Evolution of an agent) Let A = (T, B) be a (`i , `d )-agent. An
evolution of A is either:
 – the reception of a new belief,
                                          ?ϕ
                            (T, B) −−−−−−−−→ (T, B ∪ {ϕ})
                                     ϕ∈Ref
                                      /    `d
                                              (T )

 – an introspection step,
                                         i
                              (T, B) −−−
                                       i
                                         →, B \ Ref `d (T 0 ))
                                       (` T

We note (T, B)      (T 0 , B 0 ) if there exists one evolution of (T, B) into (T 0 , B 0 ).

     We define trajectories as finite or infinite sequences of evolutions π = (πi =
(Ti , Bi ))0≤i . A trajectory is finite if one also has i < n for some n ∈ N in the
preceding definition. In that case it is said to be of length n, otherwise it is of
infinite length. Finally, the domain of a trajectory π is the set of integers i for
which πi is defined, and is denoted dom(π).

Definition 7. (Fair trajectories) A trajectory

                  π = (T0 , B0 )     (T1 , B1 )      . . . (Tn , Bn )   ...

is fair if:

     ∀ϕ ∈ L, ∀n ∈ dom(π), +∞ > dist`i ,`d (ϕ, Tn ) > 0 ⇒
                      ∃m > n ∈ dom(π), dist`i ,`d (ϕ, T )n > dist`i ,`d (ϕ, Tm )

    Given the unusual definition of fairness, we prove that fair trajectories always
exist.

Lemma 1. Let (`i , `d ) be a reasoning connection and (T, B) be a (`i , `d )-agent.
Then there exists a fair trajectory starting from (T, B).

Proof. Let ϕ0 , . . . , ϕn , . . . be an enumeration of all statements in L such that
T |= ϕn . By property 1. (completeness) we know that ∀n ∈ N, dist`i ,`d (ϕn , T ) <
+∞. Let ψ0 , ψ1 , . . . be any sequence in which each ϕn appears distdiϕn T times.
Let T0 , . . . , Tn , . . . be constructed inductively as follows:
 – T0 = T
 – if Ti−1 constructed, dist`i ,`d (ϕj , Ti−1 ) > 0, and ψi = ϕj , then by property
   3. (progress) choose Ti such that dist`i ,`d (ϕj , Ti ) < dist`i ,`d (ϕj , Ti−1 ).

By property 3. (not-going-back) one easily proves that for all i the sequence
(dist`i ,`d (ϕi , Tj ))j∈N is decreasing and thus if ϕi has been selected k times in
the construction of Tj then dist`i ,`d (ϕi , Tj ) ≤ dist`i ,`d (ϕi , T0 ) − k.

   The interest of fair trajectories lies in the fact that they eventually prove any
entailment.

Proposition 1. Let T ∈ Con and ϕ ∈ L be such that T |= ϕ, and let π be a
fair trajectory starting with (T0 = T, B0 ). Then there exists N ≥ 0 such that for
all n ≥ N we have Tn `d ϕ.

Proof. Let π = ((Ti , Bi )i≥0 and un = dist`i ,`d (ϕ, Tn ). The sequence of integers
u0 , u1 , . . . contains only positive integers, and is decreasing by the not-going-
back property. Furthermore, since the trajectory is fair, for each n ∈ dom(π)
such that dist`i ,`d (ϕ, Tn ) > 0 there exists m > n such that dist`i ,`d (ϕ, Tn ) >
dist`i ,`d (ϕ, Tm ). Thus there is a finite strictly decreasing subsequence of un
which must converge to 0 at some indice N . By the not-going-back property, for
each n > N we have dist`i ,`d (ϕ, Tn ) = 0, i.e. Tn `d ϕ.

                          ?ϕ
    Note that since −−−−−−−−→ steps have no impact on the first member of the
                     ϕ∈Ref
                      /    `d
                              (T )
couple, we have roundly ignored them. Prop. 1 can be applied to prove that
any belief varphi ∈ B inconsistent with T is eventually removed, and never
reintroduced. The proof simply consists in applying Prop. 1 on ¬ϕ for all ϕ ∈ B
inconsistent with T , and is thus omitted. It is however one of the main result of
this paper, and is thus stated as a theorem.
    Let (T, B) be a (`i , `d )-agent and let π be any fair trajectory starting from
(T, B). Then there exists N ≥ 0 such that for all n ≥ N and all ϕ ∈ B such that
T |= ¬ϕ, we have ϕ ∈  / Bn .


4    Example of Reasoning Connection

We continue in this section the example of subterm local deductions in first-order
logic, and add to it ordered resolution. It is well known [2] that if a set of clauses
is saturated for ordered resolution then linear order resolution is refutationally
complete. The proof of this fact is based on the notion notion of redundancy
employed in that article: a clause obtained by ordered resolution or factorisation
is redundant if it is entailed by instances of clauses smaller than the premisses
of the rule applied. Hence, intuitively, if a proof by ordered resolution and fac-
torisation (denoted using `o of T, ¬ϕ `o ∅ contains an inference between two
clauses of T , this inference can be replaced by first, applying it on T to obtain
T 0 , and second, a case reasoning on the obtained clause: if it is redundant, then
one can replace it in the original proof of T, ¬ϕ `o ∅ by the proof of redundancy,
and if it is not redundant, one can use the newly obtained clause to simplify the
original proof.
    Thus, in the original result, the completeness of linear ordered resolution
for refutation is based on an ordering on proofs in which proofs are viewed as
multisets of clauses. Thus, for every formula ϕ entailed by T , a saturation step
can be translated into a decrease in the proof of ϕ. This approach is however
not practical for our purpose, as we would to prove that the decrease happens
for all formulas, and is strict for at least some. To prove this we need to consider
the infinite number of minimal proofs, one for each entailed clause, and the
order on this object is no longer well-founded. Hence our previous introduction
of a distance with the not-going-back and progress properties. We also weaken
slightly the redundancy criterion by considering the multiset of atoms resolved
or factored upon in the redundancy proof, instead of the set of instances of
clauses. If a proof is minimal in the sense of [2] then the multiset of atoms
resolved or factored upon is minimal. However the converse does not hold: If
T = {a ∨ b, a ∨ c, b, c} and a > b > c then we have {a ∨ b, c} > {a ∨ c, b} though
were these two sets usable interchangeably in a redundancy proof, they would
yield the same multiset {a, b, c} of atoms resolved upon.
    In Sect. 4.1 we make this discussion more precise by introducing the orderings
on terms, atoms, etc. In Sect. 4.2 we introduce the ordered resolution, factori-
sation, and redundancy rules we consider, and construct a (`i , `d ) reasoning
connection based on these rules for introspection and linear ordered resolution
for deduction. We prove that this is indeed a reasoning connection.

4.1   Orderings on Terms and Clauses
Let <t be a total, well-founded ordering on ground terms that extends the sub-
term relation, i.e. if t is a subterm of t0 then t <t t0 .
    An atom ordering is a total, well-founded ordering <a on all ground atoms
of the signature. The atom ordering <a is compatible with the term ordering
<t if p(r1 , . . . , rn ) <a q(s1 , . . . , sm ) implies that for 1 ≤ j ≤ n there exists
1 ≤ i ≤ m such that rj <t si . Terms and atoms ordering can be lifted into a
partial ordering on terms and atoms with variables by setting a ≺a b if, for all
substitution σ grounding both A and B we have Aσ <a Bσ. Since this order is
necessarily partial (variables don’t compare, for example), we say that an atom
A is (strictly) maximal wrt a set Γ of atoms if for every B ∈ Γ we have A 6≺a B
(A 6 B). Since a well-founded total ordering on a set E can always be extended
to well-founded total ordering on multisets of elements of E, we extend atom
orderings on literals by mapping a positive literal A to the multiset {| A |} and
a negative literal to the multiset {| A, A |}. Ground clauses are then ordered as
multisets of multisets of atoms.

4.2   Ordered Resolution and Factorisation
Ordered resolution was introduced in [4]. We consider in this paper post-ordered
resolution with an ad hoc redundancy rule. In short, post-ordered means that
once a unifier has been computed in the resolution of factorisation rule, we check
that the instance of the atom that will be eliminated is maximal wrt to the other
instantiated atoms (post ordered resolution). Regarding redundancy, if there is
a proof π of T \ ¬C `o ∅ such that the multiset Mπ of atoms resolved or factored
upon is smaller than the multiset of atoms occurring in C we say that C is
redundant in T , and introduce an introspection rule T `i T \ {C}.
    The other introspection rules are presented formally in Fig. 2. In the ordered
factorisation rule, Γ is the subset of negative literals while ∆ is the subset of
positive literals in the clause.


  Γ ∨ A ¬B ∨ ∆ σ = mgu(A, B)                     Γ ∨ A ∨ B σ = mgu(A, B)
     (Γ ∨ ∆)σ                                    (Γ ∨ A)σ
         ordered resolution                        ordered factorisation
  Aσ strictly maximal wrt Γ σ and Aσ          Aσ strictly maximal wrt Γ σ and Aσ
  maximal wrt ∆σ. In this case we             maximal wrt ∆σ. In this case we
  have T `i T ∪ {(Γ ∨ ∆)σ} whenever           have T `i T ∪ {(Γ ∨ A)σ} whenever
  Γ ∨ A, ¬B ∨ ∆ ∈ T                           Γ ∨A∨B ∈T

            Fig. 2. Ordered resolution and factorisation inference rules


    Ordered resolution is complete for refutation: if T |= ϕ, then T, ¬ϕ |=
emptyset, and in this case there exists a deduction sequence from T ∪ {¬ϕ}
to ∅. We denote T `o ϕ the fact that such a sequence exists. Ordered resolution
is complete for refutation: If T is an inconsistent theory then T `o ∅.
    In this section we consider for simplicity reasons only first-order theories
presented by a finite set of clauses, and note that it suffices to prove ground
clauses ϕ. For such clauses we let ¬ϕ be the set of the negation of the literals
occurring in ϕ. Finally we denote T `lin ∅ the existence of a deduction sequence
produced by linear ordered resolution and factorisation ending with the empty
clause.
    That is, in the rest of this section, we let:

 – `d be the relation T `d ϕ if and only if T, ¬ϕ `lin ∅;
 – `i be the relation T `i T 0 if T 0 can be obtained from T by either:
    • the addition of the conclusion of an ordered factorisation or ordered
       resolution rule;
    • the removal of a clause C such that T \ {C} `d C with a deduction
       sequence for linear ordered resolution in which the multiset of atoms
       resolved or factored upon is smaller than the multiset of atoms occuring
       in C.

    It is trivial that `i is truth preserving and `d is sound. So the rest of this
section is devoted to proving that (`i , `d ) is a reasoning connection. We assume
from now on that T is a satisfiable set of clauses. We let _g be a grounding
operator mapping all variables of a clause to distinct constants not occurring
in T . In that case, it is well-known that T |= ϕ if, and only if, T |= ϕg . As a
consequence and in order to simplify notation, we consider only the entailment
of ground Horn clauses, though the results lift to all clauses in the language.
    First, let us note that we have taken an apparently weaker notion of redun-
dancy than the one which is usually considered (e.g. in [3]) as usually there is no
constraint on the atoms of C in the local proof. Requiring the proof redundancy
to be linear implies in particular that we do not allow the application of an or-
dered factorisation on the instances of clauses of T . This constraint is necessary
to prove the not-going-back property, and can always be enforced by preliminary
saturation steps on T before eliminating the clause C by redundancy. That is,
it may make dist`i ,`d (ϕ, T ) greater than if it were not imposed, but has the
advantage of ensuring a monotonous decrease of dist`i ,`d (ϕ, T ) for all ϕ when
performing an introspection step.
    Since the definition employed are not exactly standard, we first prove that
we still have refutational completeness, that is that the reasoning connection has
the completeness property.

Lemma 2. Let ϕ be a ground Horn clause, and assume T |= ϕ. Then dist`i ,`d (ϕ, T ) <
+∞.

Proof. For T ∈ Con and ϕ such that T, ¬ϕ |= ∅, let ΠT,ϕ = {[C1 , . . . , Cn ] | Cn =
∅} be the set of ground deduction sequences by ordered resolution and factor-
ing from T ∪ ¬ϕ that ends with the empty clause. By completeness of ordered
resolution and factoring, we know this set is not empty.
    Also, let ΘT,ϕ be the function mapping a proof to the multiset of atoms oc-
curing in the proof and eliminated by ordered factorisation or resolution between
clauses of T :
         ΘT,ϕ :                                          ΠT,ϕ (→ A ∪ ⊥) × N
                  π 7→ {| a | a resolved or factored in π from clauses in T |}

By definition if ΘT,ϕ (π) = ∅ then π is a linear proof by ordered resolution and
factorisation that T, ¬ϕ |= ∅, and thus T, ϕ `i ∅.
    By contradiction let’s assume there exists T, ϕ such that T, ¬ϕ |= ∅ but
dist`i ,`d (ϕ, T ) is not finite. The extension to multisets of the well-founded order-
ing on atoms is a well-founded ordering on the set ΘT,ϕ (ΠT,ϕ ). By refutational
completeness of ordered resolution and factoring this set is not empty, and thus
has a minimal element π. If ΘT,ϕ (π) = ∅ then by definition pi is also a linear
proof, and thus T, ¬ϕ `i ∅, and thus dist`i ,`d (ϕ, T ) = 0, a contradiction.
    Thus ΘT,ϕ (π) 6= ∅. It is finite, and thus contains a maximal element a with
at least 1 occurrence. By definition a is an atom either resolved upon or factored
upon from clauses in T . Since this inference is by ordered resolution its result is
an instance of a clause C with T `d T ∪ {C}.
    If C is redundant in T , in which case there exists a proof of redundancy
of C in which the multiset of atoms resolved or factored upon is smaller than
the multiset of atoms occurring in C. Since a is maximal among the atoms
occurring in C none of these atoms are greater than a, and thus replacing C
with the redundancy proof yields a proof pi0 with ΘT,ϕ (π 0 ) < ΘT,ϕ (π), thus
contradicting the minimality of π.
   Thus C is not redundant in T . Let π 0 be the proof obtained from pi by
replacing the inference on a by the introduction of C. We have:

                                ΘT 0 ,ϕ (π 0 ) < ΘT,ϕ (π)

Let M0 = ΘT,ϕ (π), M1 = ΘT 0 ,ϕ (π 0 ), . . . be the sequence of multisets that can
be obtained by iterating this construction. The ordering on multisets is well-
founded, so this sequence is finite. Thus there exists n such that T = T0 (`i )n Tn
and Tn , ¬ϕ `i ∅. But then this means that dist`i ,`d (ϕ, T ) ≤ n, a contradiction
with the assumption that dist`i ,`d (ϕ, T ) is not finite.

    The proof of the preceding lemma can be adapted as follows. For each formula
ϕ, order partially the set of theories T 0 reachable from T with the minimal
number n(T 0 ) of steps that will lead to a theory in which ϕ is provable with
`d . Lemma 2 tells us that this number is always defined. Now, from T , instead
of choosing the saturation step that will minimize the number of occurrences
of the maximal atoms not occurring in ϕ, choose a T1 with a minimal n(T1 ).
By definition we have n(T1 ) = n(T ) − 1. Hence we have the following progress
lemma.

Lemma 3. Let ϕ be a ground Horn clause, and assume T |= ϕ and and T 6`d ϕ.
Then there exists T 0 such that T `i T 0 and dist`i ,`d (ϕ, T 0 ) < dist`i ,`d (ϕ, T ).

  Finally we prove the not-going-back property by proving that even the re-
moval by redundancy of a clause in T does not increase the distance

Lemma 4. Assume T |= ϕ and T `i T 0 . Then dist`i ,`d (ϕ, T 0 ) ≤ dist`i ,`d (ϕ, T ).

Proof. Since ordered resolution and factorisation simply add a new clause, the
proof is trivial if T0 is obtained from T using one of these inferences. Therefore,
let us consider only the case T `i T \ {C} = T 0 where C is a redundant clause in
T , i.e. is such that T `d C. LetπC be a deduction sequence witnessing T 0 `d C
in which the mulstiset of atoms factored or resolved upon is smaller are equal to,
for the atom ordering <a , the multiset of atoms occurring in C. , and in which
the multiset of atoms factored or resolved upon is smaller than the multiset of
atoms occuring in C.
    Given a deduction sequence π, let RC (π) be the deduction sequence in which
every position in which a ground instance Cσ is introduced is replaced by the
sequence of introductions of instances of clauses of T 0 in πC . Since the multiset
of atoms occurring in πC is less or equal to the multiset of atoms in C, it is
clear that for any proof π we have T hetaT 0 ,ϕ (RC (π)) ≤ ΘT 0 ,ϕ (π). Let T0 = T `i
T1 `i . . . `i Tn be a minimal sequence of introspections such that Tn `d ϕ. We
can perform the replacement on all proofs in ΠTi ,ϕ in this sequence and obtain
a sequence of the same length from T 0 = T00 to Tn0 . Thus dist`i ,`d (ϕ, T 0 ) ≤
dist`i ,`d (ϕ, T ).
5    Conclusion and Future Works
The main contribution is the definition of an abstract reasoning couple that
captures an interplay between introspection (as a change in the representation
of the world not triggered by an external input) and deduction as a judgement on
one’s beliefs, a set of statements assumed satisfiable. The framework presented
is a first step towards more interesting agent models, for which one would need
at least:
 – the possibility to change the knowledge, for example to reflect the agent’s
   experience;
 – the possibility for the agent to perform some actions, that is to influence the
   world based on her beliefs and knowledge.
    Furthermore, there is no reasoning based on beliefs in the proposed frame-
work. The proper extension in this case consists in introducing a generic structure
such as a directed acyclic graph in which vertices or members are labelled with
theories, and the couples (T, B) introduced in this paper would be modeled by
a binary relation on vertices.
    Also, on a more technical note, this works stems from previous work on
the compilation of cryptographic protocols, that is from giving an operational
semantics in a precise agent model to agents that will implement a protocol
specification as well as possible. In that context, we hope that further extensions
of the framework presented in this paper will be used as target agent models.

Acknowledgements. We would like to thank Philippe Besnard and Michal Rusi-
nowitch for insightful comments on a first draft of this paper.


References
 1. Armando, A., Ranise, S., Rusinowitch, M.: Uniform derivation of decision pro-
    cedures by superposition. In: Fribourg, L. (ed.) Computer Science Logic: 15th
    International Workshop, CSL 2001 10th Annual Conference of the EACSL Paris,
    France, September 10–13, 2001, Proceedings. pp. 513–527. Springer Berlin Heidel-
    berg, Berlin, Heidelberg (2001)
 2. Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with se-
    lection and simplification. J. Log. Comput. 4(3), 217–247 (1994)
 3. Basin, D., Ganzinger, H.: Automated complexity analysis based on ordered reso-
    lution. J. ACM 48(1) (Jan 2001)
 4. Besnard, P., Quiniou, R., Quinton, P.: A theorem-prover for a decidable subset of
    default logic. In: Proceedings of the National Conference on Artificial Intelligence.
    Washington, D.C., August 22-26, 1983. pp. 27–30 (1983)
 5. Dershowitz, N., Jouannaud, J.P.: Rewrite systems. In: Handbook of Theoretical
    Computer Science, Volume B, pp. 243–320. Elsevier (1990)
 6. Knuth, D.E., Bendix, P.B.: Simple word problems in universal algebras. In: Siek-
    mann, J.H., Wrightson, G. (eds.) Automation of Reasoning: 2: Classical Papers on
    Computational Logic 1967–1970. pp. 342–376. Springer Berlin Heidelberg, Berlin,
    Heidelberg (1983)
 7. Konolige, K.: A deduction model of belief and its logics. Tech. Rep. 326, AI Center,
    SRI International, 333 Ravenswood Ave., Menlo Park, CA 94025 (Aug 1984)
 8. Kowalski, R., Kuehner, D.: Linear resolution with selection function. Artificial
    Intelligence 2 (1971)
 9. Lynch, C., Morawska, B.: Automatic decidability. In: Proceedings of the Logic in
    Computer Science Conference. pp. 7–17. IEEE Computer Society (2002)
10. McAllester, D.A.: Automatic recognition of tractability in inference relations. J.
    ACM 40(2), 284–303 (1993)
11. de Nivelle, H.: Ordering refinements of resolution. Ph.D. thesis, Technische Uni-
    versiteit Delft (1996)
12. Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal
    of the Association for Computing Machinery 12, 23–41 (1965)

</pre>