International Journal of Intelligence Science
Vol.3 No.2(2013), Article ID:30636,8 pages DOI:10.4236/ijis.2013.32012
The Sound and Complete R-Calculi with Respect to Pseudo-Revision and Pre-Revision*
1State Key Laboratory of Software Development Environment, Beijing University of Aeronautics and Astronautics, Beijing, China
2Key Laboratory of Intelligent Information Processing, Institute of Computing Technology, Chinese Academy of Sciences, Beijing, China
Email: liwei@nlsde.buaa.edu.cn, yfsui@ict.ac.cn
Copyright © 2013 Wei Li, Yuefei Sui. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
Received January 18, 2013; revised February 20, 2013; accepted March 15, 2013
Keywords: Belief Revision; R-Calculus; Maximal Consistent Set; Pseudo-Revision; Pre-Revision
ABSTRACT
The AGM postulates ([1]) are for the belief revision (revision by a single belief), and the DP postulates ([2]) are for the iterated revision (revision by a finite sequence of beliefs). Li [3] gave an R-calculus for R-configurations where Δ is a set of literals, and Γ is a finite set of formulas. We shall give two
-calculi such that for any consistent set Γ and finite consistent set
of formulas in the propositional logic, in one calculus, there is a pseudo-revision Θ of Γ by Δ such that
is provable and
and in another calculus, there is a pre-revision Ξ of Γ by Δ such that
is provable,
and
for some pseudo-revision Θ; and prove that the deduction systems for both the
-calculi are sound and complete with the pseudo-revision and the pre-revision, respectively.
1. Introduction
The AGM postulates ([1],[4-6]) are for the revision of a theory
by a formula
and the DP postulates ([2]) are for the iterated revision
The -calculus ([3]) gave a Gentzen-type deduction system to deduce a consistent theory
from any theory
where
should be a maximal consistent subtheory of
which includes
as a subset, where
is an
-configuration,
is a consistent set of formulas, and
is a consistent sets of literals (atomic formulas or the negation of atomic formulas). It was proved that if
is deducible and
is an
-termination, i.e., there is no
-rule to reduce
to another
-configuration
then
is a pseudo-revision of
by
The -calculus has the following features:
● is a finite set of literals (propositional variables or the negation of propositional variables);
● is a set of formulas;
● are not sufficient for pseudo-revision, and
is introduced to deduce
into a consistent set
of formulas including
● the soundness theorem holds, that is, if is provable then
is a pseudo-revision of
by
and
● the completeness theorem holds, that is, if is a pseudo-revision of
by
then
is provable.
Because each rule in the -calculus consists of the statements of form
the -calculus is based on pseudo-revision, i.e., to contract
from
if
is inconsistent, which makes the
-calculus not preserve the minimal change principle.
Given two theories and
a pseudo-revision
of
by
is a consistent subset of
including
(if
is inconsistent; otherwise,
).
We shall give two -calculi such that
● in one -calculus, say
for any consistent formula set
and finite formula set
there is a consistent formula set
such that
is provable and
is a pseudo-revision of
by
(the soundness theorem); and conversely, given any pseudo-revision
of
by
is provable (the completeness theorem);
● in another -calculus, say
for any consistent formula set
and finite formula set
there are consistent formula sets
and
such that
◦ is provable
◦ is a pseudo-revision of
by
◦ and
◦ there is no subformula of
contradictory to
(the soundness theorem);
and conversely, given any pseudo-revision of
by
there is a consistent formula set
such that
is provable,
and
is contradictory to no subformula
of
(the completeness theorem).
The -calculi are different from the
-calculus in [3] as follows:
◊ is any set of formulas;
◊ The cut-rule in the -calculus is eliminated in the
-calculi;
◊ Because -rule in the
-calculus is not sufficient for reducing
to either or
the
- calculus is not complete with respect to the pseudorevision of
by
In the new
-calculi, we split
into two deduction rules
and
according to whether
is consistent with
or not. The reason is given as follows.
Given a consistent theory and formulas
is inconsistent if and only if
and
are inconsistent; and if either
or
is inconsistent then
is inconsistent; and if
is inconsistent then we cannot deduce that either
or
is inconsistent, and what we have is that
is inconsistent if and only if either
is inconsistent or
is inconsistent. Formally,
(1)
(2)
(3)
where and
denote that
is consistent and inconsistent, respectively. Therefore, we use
in and
instead of
in the -calculus.
In we use a rule
to deduce to
if
are consistent. In
, we shall give a deduction rule to reduce
to the atomic cases where
with a cost that we cannot prove that if is provable then
is a pseudo-revision of
by
Instead we shall prove that if
is provable then
is a pre-revision of
by
that is, there is a consistent theory
such that 1)
is a pseudo-revision of
by
2)
and 3) no subformula
of
is contradictory to
The paper is organized as follows: the next section gives the -calculus in [3] and basic definitions; the third section defines an
-calculus
for the pseudorevision and proves that
is sound and complete with respect to the pseudo-revision; the fourth section defines another
-calculus
for the pre-revision and prove that
is sound and complete with respect to the pseudo-revision, and the last section concludes the whole paper.
2. The -Calculus
The -calculus is defined on a first-order logical language. Let
be a logical language of the first-order logic;
formulas and
sets of formulas (theories), where
is a set of atomic formulas or the negations of atomic formulas, and
is called an R-configuration.
The -calculus consists of the following axiom and inference rules:
where in means that
occurs in the proof tree
of
from
and
and in
is a term, and is free in
for
.
The -calculus is in the first-order logic. In the following we discuss the
-calculi in the propositional logic.
Let be a logical language of the propositional logic which contains the following symbols:
propositional variables:
logical connectives:
Formulas are defined as follows:
Definition 2.1. Given a consistent set of formulas and a finite consistent set
of formulas, a consistent set
of formulas is a pseudo-revision of
by
if
(if
is consistent), or (if
is inconsistent then)
satisfies the following conditions:
1)
2) and 3) there is a
such that
is inconsistent.
Each pseudo-revision can be generated by the following procedure: given any consistent set
and finite consistent set
assume that
is ordered by a linear ordering
(without loss of generality, assume that
), define
Let Then,
is a subset of
such that
and
is consistent.
Lemma 2.2. is a pseudo-revision of
by
Moreover, Let
be the least
such that
Then,
Definition 2.3. Given a consistent set of formulas and a finite consistent set
of formulas, a consistent set
of formulas is a pre-revision of
by
if there is a pseudo-revision
of
by
such that 1)
2) and 3) no subformula
of
is contradictory to
Each pre-revision can be generated by the following procedure: given any consistent set
and finite consistent set
assume that
define
where
where is the empty string.
Let and
be the pseudo-revision of
by
in the same ordering as
Then, we have the following Lemma 2.4. Let
be the least
such that
Then, for any
and for any
is a subformula of
Lemma 2.5. is a pre-revision of
by
such that
and no subformula of
is contradictory to
Proof. Let be the least
such that
Then,
We prove that for any with
and
by induction on
Let and
Then,
We prove by induction on the structure of
that
and
If and
then
is inconsistent, a contradiction to the choice of
If and
then
and
If and
is consistent then
and
are consistent, and by the induction assumption,
and hence,
If and
is consistent then either
or
is consistent.
If and
are consistent. then by the induction assumption,
and hence,
If is inconsistent and
is consistent. then
and by the induction assumption,
and hence,
because
and
(
is inconsistent, and hence, for any formula
).
Similar for the case that is consistent and
is inconsistent.
Similarly we can prove that for any with
3. The -Calculus
In this section we give an -calculus
which is sound and complete with respect to the pseudo-revision, where the decision of whether
is consistent is needed so that if
is consistent then
is provable; otherwise,
is provable.
Let be any consistent sets of formulas.
Definition 3.1. is a term; and
is a statement, where
and
; and
is a deduction rule, where are statements.
has the following deduction rules:
Definition 3.2. is provable if there is a sequence
of statements such that 1)
2) and 3) for each
is either an axiom or deduced from the previous statements by the deduction rules.
For example, the following
is a proof and so is provable.
Also, the following
is a proof and so is provable.
Theorem 3.3. For any consistent sets of formulas and formula
if
is provable then
is inconsistent; and if
is provable then
is consistent.
Proof. If is provable then
is used and
is consistent.
If is provable then we prove that
i.e.,
is inconsistent, by the induction on the length of a proof of
and the cases that the last inference rule is used.
If the last rule used is then
and
i.e.,
If the last rule used is then
and
i.e.,
If the last rule used is then
, and
. By the induction assumption,
, and hence,
i.e.,
If the last rule used is then
and
By the induction assumption,
and hence,
i.e.,
If the last rule used is then
and
By the induction assumption, ,
, and hence,
i.e.,
Theorem 3.4. For any consistent sets of formulas and formula φ, if
is inconsistent then
is provable; and if
is consistent then
is provable.
Proof. If φ is consistent with then by
,
is provable;
Assume that φ is inconsistent with Δ. We prove by the induction on the structure of φ that is provable.
If φ = p then and by
,
is provable.
If then
and by
is provable.
If then there are two subcases:
is inconsistent with
or
is consistent with
In the first subcase, by the induction assumption,
is provable, and by
is provable; and in the second subcase,
is consistent and
is inconsistent. By the induction assumption,
is provable, and by
If then both
and
are inconsistent. By the induction assumption, both
and
are provable, and by
is provable.
Theorem 3.5. For any consistent sets of formulas, if
is finite then there is a set
of formulas such that
is provable Proof. Let
We prove the theorem by the induction on
If then by theorem 3.3, let
and satisfies the theorem.
Assume that the theorem holds for that is, there is a set
such that
is provable. Let
If is consistent with
then
is provable, where
If is inconsistent with
then
because the last formula
is inconsistent with
Theorem 3.6 (The soundness theorem for). If
is provable then
is a pseudo-revision of
by
Proof. Firstly we prove that if is provable then
is a pseudo-revision of
by
Assume that is provable.
If then
is consistent with
and
is a pseudo-revision of
by
If then
is inconsistent with φ,
is provable, and
is a pseudo-revision of
by
Similarly, by the induction on the number of formulas in we can prove that if
then
is a pseudo-revision of
by
.
Theorem 3.7 (The completeness theorem for). If
is a pseudo-revision of
by
then
is provable.
Proof. Let be a pseudo-revision of Γ by
under the ordering
of Γ.
We prove by induction on that there is a formula set
such that
is provable, where
and
If is consistent then let
, and
is provable, where
Assume that is inconsistent. Then,
and let
by theorem 3.4,
is provable.
Let Then,
is provable.
4. The -Calculus
In this section we give an -calculus
which is sound and complete with respect to the pre-revision, where the decision of whether
is consistent is deduced by a set of
-rules.
R1 is used to reduce to
when
is inconsistent. When
is consistent, there are subformulas in
which is inconsistent with
we hope to reduce those subformulas into the empty string. For example, let
Then, by we have the following reduction:
and by we shall have the following one:
For the two reductions, we have
Let be a consistent set of formulas and
a finite consistent set of formulas.
consists of two parts:
which we use to decompose formula
in
if
is inconsistent; and
-deduction rules, which we use to decompose
if
is consistent.
has the following
-deduction rules to reduce
when
is consistent:
where if is consistent then
and if is inconsistent then
The deductions for the inconsistent are the same as in
minus
Definition 4.1. is provable if there is a sequence
of statements such that 1)
2) and 3) for each
is either an axiom or deduced from the previous statements by the deduction rules.
We call the sequence a proof of statement.
For example, the following
is a proof and is provable.
Theorem 4.2. For any consistent sets of formulas and formula
if
is provable then
is inconsistent; and if there is a formula
such that
is provable then
is consistent.
Proof. If is provable then similar to the proof of theorem 3.3,
is inconsistent.
Assume that there is a formula such that
is provable. We prove by the induction on the length of a proof of
and the cases that the last inference rule is used that
is consistent.
If the last rule used is then
and
is provable, where
Hence,
is consistent.
If the last rule used is then
and
is provable, where
. Hence,
is consistent.
If the last rule used is then
and there are formulas
such that
and
By the induction assumption, if θ1 ≠ λ and θ2 ≠ λ then is consistent and
is consistent, and therefore,
is consistent.
If the last rule used is then
and
where either or
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption, and
are consistent, and so is
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption, is consistent, and so is
If θ1 ≠ λ and θ2 ≠ λ then by the induction assumption, is consistent, and so is
By the proof of the theorem, we have
Theorem 4.3. For any formula sets and formula
if
is consistent then
Proof. We prove the theorem by the induction on the structure of Assume that
If then
and
Hence,
If then
and
By the induction assumption,
Hence, we have
If then either
is consistent or
is consistent.
If and
are consistent then
and
By the induction assumption,
Hence, we have
If is inconsistent and
is consistent then
By the induction assumption,
Hence, by Lemma 2.5, we have
If is consistent and
is inconsistent then
By the induction assumption,
Hence, by Lemma 2.5, we have
Theorem 4.4. For any consistent sets of formulas and formula
if
is inconsistent then
is provable; and if
is consistent then there is a formula
such that
is provable.
Proof. If is inconsistent with
then similar to theorem 3.5,
is provable.
Assume that φ is consistent with We prove the theorem by the induction on the structure of φ.
If φ = p then and by
is provable, where
If then
and by
is provable, where
If then φ1 is consistent with
and φ2 is consistent with
By the induction assumption, there are formulas
such that
and
are provable. By
we have
is provable, where
If then either
or
is consistent. By the induction assumption, if
is consistent then there is a formula
such that
and if
is consistent then there is a formula
such that
Then, by
is provable, where
Remark. In fact, in theorem 4.3, if is consistent then there is a formula
such that
is provable.
By Theorem 4.3, we have the following Theorem 4.5. (The soundness theorem for). If
is provable then
is a pre-revision of
by Δ.
Proof. We only prove that no subformula ξ of Ξ is contradictory to Δ.
Assume that there is a subformula ξ of some formula in Ξ such that
Let
such that
If is inconsistent then
a contradiction.
If is consistent then by Lemma 3.5,
and for any subformula ξ of θ, if then, by the definition of θ, ξ is replaced by
in θ, a contradiction to the assumption that ξ is a subformula of θ.
Theorem 4.6. (The completeness theorem for Γ). If Ξ is a pre-revision of Γ by Δ then is provable.
Proof. The proof is similar to theorem 3.7 and omitted.
5. Conclusion
This paper gave two -calculi which are sound and complete with respect to the pseudo-revision and prerevision, respectively. The calculi are of Gentzen-type, in which each statement is of form
Different orderings of
give different results of revision
Correspondingly, if
is irreducible, that is, no deduction rule can be used to reduce
then
may be a minimal change of
by
A further work is to give an
-calculus such that if
is irreducible then
is consistent and
is a minimal change of
by
that is, for any
with
is inconsistent.
REFERENCES
- C. E. Alchourrón, P. Gärdenfors and D. Makinson, “On the Logic of Theory Change: Partial Meet Contraction and Revision Functions,” The Journal of Symbolic Logic, Vol. 50, No. 2, 1985, pp. 510-530. doi:10.2307/2274239
- A. Darwiche and J. Pearl, “On the Logic of Iterated Belief Revision,” Artificial Intelligence, Vol. 89, No. 1-2, 1997, pp. 1-29. doi:10.1016/S0004-3702(96)00038-0
- W. Li, “R-Calculus: An Inference System for Belief Revision,” The Computer Journal, Vol. 50, No. 4, 2007, pp. 378-390. doi:10.1093/comjnl/bxl069
- E. Fermé and S. O. Hansson, “AGM 25 Years, TwentyFive Years of Research in Belief Change,” Journal of Philosophical Logic, Vol. 40, No. 2, 2011, pp. 295-331. doi:10.1007/s10992-011-9171-9
- N. Friedman and J. Y. Halpern, “Belief Revision: A Critique, to Appear in J. of Logic, Language and Information,” In: L. C. Aiello, J. Doyle and S. C. Shapiro, Eds., Proceedings of the 5th Conference of Principles of Knowledge Representation and Reasoning, 1996, pp. 421-431.
- P. Gärdenfors and H. Rott, “Belief Revision,” In: D. M. Gabbay, C. J. Hogger and J. A. Robinson, Eds., Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 4, Epistemic and Temporal Reasoning, Oxford Science Pub., Oxford, 1995, pp. 35-132.
NOTES
*This work was supported by the Open Fund of the State Key Laboratory of Software Development Environment under Grant No. SKLSDE-2010KF-06, Beijing University of Aeronautics and Astronautics, and by the National Basic Research Program of China (973 Program) under Grant No. 2005CB321901.