This paper introduces a formal framework for relating learning 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 reasoning/deduction connection and we show how this-and related-definition apply to a setting in which agents are modeled by first-order logic theories. 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.
We consider in this paper a framework in which an agent is described by statements 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 (usually 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 [
In contrast with these more recent approaches, the dynamicity of reasoning
that we consider is closer to the unfailing completion procedure [
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
2.1
First-order objects. We assume the reader is familiar with the basics of firstorder 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 function 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 2 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. Accordingly 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 j= ; if it has no model.
Unifier, resolution and factorization. A substitution is an idempotent function from variables to terms of finite support, i.e. (x) = x for all but a finite number of variables. Substitutions are extended homomorphically (using (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 fC1; : : : ; Ci 1g. Whenever one such sequence exists we write T ` Cn. Resolution is complete for refutation, i.e. if T j= ; then T ` ;. If is a clause and T is not inconsistent, we have that T j= is equivalent to T; : j= ;, and thus by completeness for refutation T; : ` ;. Trivially, if is an atomic formula, i.e. contains only one literal, this implies T ` .
_ A :B _ ( _ ) ( resolution
factorisation 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 2 M we have m j= T if and only if m j= 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 2 M , we have m j= T implies m j= '.
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 2 Con and ' 2 L such that T j= ', we measure the difficulty of proving ' from T by the number of introspection steps needed to reach a set T 0 2 Con such that T 0 `d '.
Definition 3. (Distance to provability) Assume `i Con Con is an introspection relation, T j= ', and that `d is a deduction relation. Then we let: dist`i;`d ('; T ) = minfn j T `i n T 0 and T 0 `d 'g
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 [
We capture the relation between introspection and deduction outlined previously 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 j= ' 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 immediately provable, there exists an introspection step that will reduce the distance to provability.
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: 2. not-going-back:
8' 2 L; 8T 2 Con; T j= ' ) dist`i;`d ('; T ) < +1 8' 2 L; 8T; T 0 2 Con; T `i T 0 ) dist`i;`d ('; T 0) dist`i;`d ('; T ) 8T 2 Con; 8' 2 L; 0 < dist`i;`d ('; T ) < +1 )
(9T 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
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 2 Con and B L, and for all ' 2 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 ) = f' j T `d :'g 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, – an introspection step, (T; B) '2=Re?f'`d (T !) (T; B [ f'g)
(T; B) (`ii!T; B n Ref`d (T 0)) We note (T; B)
(T 0; B0) if there exists one evolution of (T; B) into (T 0; B0).
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 2 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: 8' 2 L; 8n 2 dom( ); +1 > dist`i;`d ('; Tn) > 0 )
9m > n 2 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 j= 'n. By property 1. (completeness) we know that 8n 2 N; dist`i;`d ('n; T ) < +1. Let 0; 1; : : : be any sequence in which each 'n appears distdi'nT 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 ))j2N 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 2 Con and ' 2 L be such that T j= ', 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-goingback property. Furthermore, since the trajectory is fair, for each n 2 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 '2=Re?f'`d (T !) steps have no impact on the first member of the couple, we have roundly ignored them. Prop. 1 can be applied to prove that any belief varphi 2 B inconsistent with T is eventually removed, and never reintroduced. The proof simply consists in applying Prop. 1 on :' for all ' 2 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 ' 2 B such that T j= :', we have ' 2= Bn. 4
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 [
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 [
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, factorisation, 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
Let <t be a total, well-founded ordering on ground terms that extends the subterm 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 2 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 fj A jg and a negative literal to the multiset fj A; A jg. Ground clauses are then ordered as multisets of multisets of atoms. 4.2
Ordered resolution was introduced in [
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) ( _ )
ordered resolution A strictly maximal wrt and A maximal wrt . In this case we have T `i T [ f( _ ) g whenever _ A; :B _ 2 T (
Ordered resolution is complete for refutation: if T j= ', then T; :' j= emptyset, and in this case there exists a deduction sequence from T [ f:'g 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 n fCg `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 j= ' if, and only if, T j= '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
redundancy than the one which is usually considered (e.g. in [
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 j= '. Then dist`i;`d ('; T ) < +1.
Proof. For T 2 Con and ' such that T; :' j= ;, let T;' = f[C1; : : : ; Cn] j Cn = ;g be the set of ground deduction sequences by ordered resolution and factoring 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 occuring in the proof and eliminated by ordered factorisation or resolution between clauses of T :
T;' : 7! fj a j a resolved or factored in
T;'(! A [ ?) N from clauses in T jg By definition if T;'( ) = ; then is a linear proof by ordered resolution and i . factorisation that T; :' j= ;, and thus T; ' ` ;
By contradiction let’s assume there exists T; ' such that T; :' j= ; but dist`i;`d ('; T ) is not finite. The extension to multisets of the well-founded ordering 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 [ fCg.
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: 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 wellfounded, so this sequence is finite. Thus there exists n such that T = T0(`i)nTn 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 j= ' 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 removal by redundancy of a clause in T does not increase the distance Lemma 4. Assume T j= ' 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 n fCg = 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 ).
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 framework. 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 Rusinowitch for insightful comments on a first draft of this paper. 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 Universiteit 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)