ファイル置き場 Sendai Logic Homepage He20121109

(1)

Outline Backgrounds A problem related to this topic Abstract Preliminaries GR-calculus and Some Related Conclusions Main Results References

Generalized R-Calculus

Qingyu He, Jie Ding

School of Mathematical Science, School of Information Engineering,

Yangzhou University

Nov. 9, 2012

(2)

1 Backgrounds

2 A problem related to this topic

3 _Abstract 4 Preliminaries

5 GR-calculus and Some Related Conclusions

6 Main Results

Soundness of GR-calculus Completeness of GR-calculus

7 _References

Qingyu He, Jie Ding Generalized R-Calculus

(3)

Backgrounds

Inference system for belief revision, plays a significant role in the description of the process of software evolution and scientific discovery.

(4)

Backgrounds

In 1985, the theory of changes [1], called the AGM theory, was introduced by G¨ardenfors and his colleagues.

The AGM theory contributes to build axiomatic systems of postulates for expansion, contraction and revision.

(5)

Backgrounds

In 1985, the theory of changes [1], called the AGM theory, was introduced by G¨ardenfors and his colleagues.

The AGM theory contributes to build axiomatic systems of postulates for expansion, contraction and revision.

A basic problem of the AGM theory was how to accomplish a task: A new sentence that is inconsistent with a belief system K is added, but in order to maintain consistency in the resulting belief system, some of old sentences in K are deleted.

(6)

Backgrounds

To solve this problem above on basis of only the syntax and semantics of classical first-order logic.

In 1994, a logic inference system named R-calculus was first defined by Li [4, 5], which is employed to derive all maximal contractions of a base of a formal theory for its given refutations.

(7)

Backgrounds

The R-calculus consisting of : an axiom

R-logical connective symbol rules R-quantifier symbol rules

R-cut rules

(8)

Backgrounds

The R-calculus consisting of : an axiom

R-logical connective symbol rules R-quantifier symbol rules

R-cut rules

Subsequently, reachability, soundness and completeness of R-calculus were first defined and proved [7].

(9)

A problem related to this topic

We start from a problem.

(10)

A problem related to this topic

Noting that there is a restriction in the most work on R-calculus, i.e. the formula set Γ in a R-configuration ∆ | Γ is assumed to be consistent.

(11)

A problem related to this topic

Noting that there is a restriction in the most work on R-calculus, i.e. the formula set Γ in a R-configuration ∆ | Γ is assumed to be consistent.

Remark

This restriction is relaxed in the basic theorem of testing [8], this assumption limits the wider application.

If it is so wide, that starting definition-Model of R-refutation is not strict enough, and a counterexample can give easily.

(12)

(13)

A problem related to this topic

From this question, we will establish a generalized R-calculus (GR-calculus for short) without the restriction of consistency for the formula set Γ.

We find that GR-calculus is also sound and complete. But, there are also some basic problems to be solved, and the suitable algorithm to be discussed.

(14)

abstract

This paper presents a generalization of the local inference system R-calculus by allowing the formula set Γ in a R-configuration ∆ | Γ to be inconsistent. Four sets of rules, i.e. GR-axioms, GR-logical

connective symbol rules, GR-quantifier symbol rules, and GR cut rules, are analogously defined in this paper, on the basis of the R-calculus language. Moreover, this generalized R-calculus is proved sound and complete.

(15)

The set of terms LT is defined inductively as below: t ::= c | x | f (t1, t2, · · · , tn). The (logical) formulas are defined inductively as follows:

A ::= t₁= t^. ₂| P(t₁, · · · , tn) | ¬A | A∧B | A∨B | A → B | A ↔ B | ∃xA | A Gentzen style logical inference system G is built on sequent [8] the form of Which is Γ ⊢ ∆, Γ is called the antecedent of the sequent, ∆ is called the succedent of the sequent and ⊢ denotes the deductive relation.

A sequent is called provable if its proof tree [8] exists. Otherwise, the sequent Γ ⊢ ∆ is unprovable.

(16)

(Consistency of Γ ) Let Γ be a set of formulas. If there does not exist a formula A, such that Γ ⊢ A and Γ ⊢ ¬A hold, then Γ is said to be consistent. Otherwise, we say that Γ is inconsistent.

(Formal refutation) If Γ ⊢ ¬A holds and ¬A is not a valid sentence, then we call A a formal refutation of Γ.

Lemma 1 (satisfiability) If Γ is a consistent formula set, then Γ is satisfiable. This means that there is a model hM, σi such that M|=^σ Γ holds.

Lemma 2 A formula set Γ is inconsistent, if and only if Γ ⊢ A and Γ ⊢ ¬A hold for every formula A.

(17)

GR -calculus and Some Related Conclusions

Definition

(GR-refutation). Let Γ be a countable formula set and ∆ a formal theory consisting of finitely many atomic formulas or negations of atomic

formulas. If there exists a formal theory Γ^′ ⊆ Γ such that ∆ is inconsistent with Γ^′, then we call ∆ a generalized R-refutation of Γ, or GR-refutation for short.

Remark

Let Γ^′ be a formal theory and Γ a countable formula set.

(1) If ∆ is a GR-refutation of Γ^′, then ∆ is an R-refutation of Γ^′. (2) If ∆ is inconsistent with Γ^′ ⊆ Γ, then ∆ is inconsistent with Γ.

(18)

GR -calculus and Some Related Conclusions

Definition

(Model of GR-refutation). Let Γ be a countable formula set and

∆ = {A₁, · · · , A_n} be a formal theory consisting of finitely many atomic formulas or negations of atomic formulas. If there exists a maximal consistent subset Γ of Γ and a model M such that Γ |= ¬A₁∨ · · · ∨ ¬An

and M |= ∆, then we call M the model of refutation of Γ by facts with respect to ∆.

Furthermore, we call M a model of GR-refutation of Γ with respect to ∆ if Γ_M(∆) is maximal, that is, there does not exist another model M^′ of refutation by facts with respect to ∆ such that Γ_M(∆)(Γ_M′_(∆), where

Γ_M(∆) = {B | B ∈ Γ, M |= B, M |= ∆}.

(19)

GR -calculus and Some Related Conclusions

Lemma

If ∆ = {A1, · · · , An} is a GR-refutation of Γ, then there exists a formal theory Γ ⊆ Γ such that Γ ⊢ ¬(A₁∧ · · · ∧ An) is provable.

Clearly, ∆ is a formal refutation of ¯Γ above. Proposition

Let Γ be a countable formula set and ∆ = {A₁, · · · , An} a formal theory. Then ∆ is a GR-refutation of Γ if and only if there exists a model M of GR-refutation of Γ such that M |= ∆.

(20)

GR -calculus and Some Related Conclusions

Definition

(Maximal ∆-consistent subset). Let Γ be a countable formula set and ∆ a finite formal theory. If there exists a formal theory Γ^′ ⊆ Γ such that Γ^′ is consistent with ∆, then we call Γ^′ a ∆-consistent subset of Γ.

Furthermore, Γ^′ is called a maximal ∆-consistent subset of Γ, if there is no

∆-consistent subset Γ^′′ of Γ such that Γ^′ (Γ^′′.

Definition

(GR-contraction). Let ∆ be a GR-refutation of a formula set Γ. A formal theory Λ is called a GR-contraction of Γ, if Λ is a maximal ∆-consistent subset of Γ.

(21)

GR -calculus and Some Related Conclusions

Proposition

Let Γ be a countable formula set and ∆ = {A₁, · · · , An} a formal theory. Let Γ be a consistent subset of Γ and Γ^′ a maximal ∆-consistent subset of Γ. If Γ^′ ⊆ Γ, then Γ^′ is a R-contraction of Γ.

Proposition

Let Γ be a countable formula set and ∆ a formal theory. Let Γ^′ be a maximal ∆-consistent subset of Γ, then there exists a maximal consistent subset Γ such that Γ^′ is the R-contraction of Γ with respect to ∆.

(22)

GR -calculus and Some Related Conclusions

The following example demonstrates that not every R-contraction of Γ is aGR-contraction.

Example

Let ∆ = {¬A, ¬B}, Γ = {A, B, C , ¬A, ¬B}.

We can obtain a maximal consistent subset Γ = {A, B, C } of Γ. Then we can prove that {C } is an R-contraction of Γ, while {C } is not the maximal ∆-consistent subset of Γ.

In fact, Γ₀= {¬A, ¬B, C } is a maximal ∆-consistent subset of Γ. However, we notice that {C } = Γ ∩ Γ₀.

(23)

GR -calculus and Some Related Conclusions

Lemma

Every ∆-consistent subset of Γ can be extended to a maximum

∆-consistent subset of Γ. Theorem

Let Γ be an arbitrary maximal consistent subset of Γ and Γ^′ an

R-contraction of Γ with respect to ∆. Then Γ^′ is either a GR-contraction of Γ or an intersection of Γ and a GR-contraction (namely, Γ0) of Γ.

(24)

GR -calculus and Some Related Conclusions

Definition

(GR-calculus). GR-calculus is a formal inference system on general R-configurations. It consists of four sets of rules: GR-axioms, GR-logical connective symbol rules, GR-quantifier symbol rules, GR cut rules.

Definition GR-axioms

GR-axiom I: ϕ, ∆ | ¬ϕ, Γ =⇒ ϕ, ∆ | Γ. GR-axiom II: ∆ | ϕ, ¬ϕ, Γ =⇒ ∆ | ϕ, Γ.

(25)

GR -calculus and Some Related Conclusions

The following definitions are analogously defined and proved from [6]. GR-logical connective symbol rules

GR-∧ rule

∆ | A, Γ =⇒ ∆ | Γ

∆ | A ∧ B, Γ =⇒ ∆ | Γ

∆ | B, Γ =⇒ ∆ | Γ

∆ | A ∧ B, Γ =⇒ ∆ | Γ^. GR-∨ rule

∆ | A, Γ =⇒ ∆ | Γ ∆ | B, Γ =⇒ ∆ | Γ

∆ | A ∨ B, Γ =⇒ ∆ | Γ ^. GR-→ rule

∆ | ¬A, Γ =⇒ ∆ | Γ ∆ | B, Γ =⇒ ∆ | Γ

∆ | A → B, Γ =⇒ ∆ | Γ ^.

(26)

GR -calculus and Some Related Conclusions

GR-quantifier symbol rules, GR-∀ rule

∆ | A[t/x], Γ =⇒ ∆ | Γ

∆ | ∀A[x], Γ =⇒ ∆ | Γ where t is a term, and x is not a free variable in t. GR-∃ rule

∆ | A[y /x], Γ =⇒ ∆ | Γ

∆ | ∃A[x], Γ =⇒ ∆ | Γ ^. where y is either x or an arbitrary variable.

(27)

GR -calculus and Some Related Conclusions

GR cut rules GR-cut rule I

Γ1, A, Γ2⊢ C A 7→τC ∆ | C , Γ2=⇒ ∆ | Γ2

∆ | Γ1, A, Γ2=⇒ ∆ | Γ1, Γ2

GR-cut rule II

Γ1, A ⊢ B A 7→τB B, Γ2⊢ C ∆ | C , Γ2=⇒ ∆ | Γ2

∆ | Γ1, A, Γ2=⇒ ∆ | Γ1, Γ2

.

(28)

GR -calculus and Some Related Conclusions

(GR-inference tree and GR-proof tree).

Given an R-transition ∆ | Γ =⇒ ∆ | Γ^′, a tree τ is called a

GR-inference tree of the R-transition if each node of τ is an instance of the R-transition. If τ is a finite GR-inference tree of the

R-transition ∆ | Γ =⇒ ∆ | Γ^′ and its leaf nodes are all instances of the GR-axioms, then τ is called a GR-proof tree of ∆ | Γ =⇒ ∆ | Γ^′.

(29)

GR -calculus and Some Related Conclusions

(GR-provable).

A R-transition is GR-provable if its GR-proof tree exists. Otherwise, we say that the R-transition ∆ | Γ =⇒ ∆ | Γ^′ is GR-unprovable. We call

∆ | Γ =⇒ · · · ∆ | Γn=⇒ · · · =⇒ ∆ | Γ^′

an transition sequence and denote it by ∆ | Γ =⇒^∗ ∆ | Γ^′ with =⇒^∗ denoting countable transitions.

We say that ∆ | Γ =⇒^∗ ∆ | Γ^′ is GR-provable if every R-transition in the R-transition sequence ∆ | Γ =⇒^∗∆ | Γ^′ is GR-provable.

(30)

Main Results

Lemma(Basic theorem of testing [8]).

Let Γ be an arbitrary countable formula set and ∆ arbitrary formal theory consisting of finitely many atomic formulas or negations of atomic formulas. If Γ^′ is an arbitrary maximal subset of Γ that is consistent with ∆, then there exists an R-transition sequence

∆ | Γ =⇒^∗ ∆ | Γ^′ that is provable.

Provability of the R-transition sequence mentioned above is GR-provable actually.

(31)

Soundness of GR-calculus Completeness of GR-calculus

Soundness of GR-calculus

Definition

(GR-soundness). If for any R-configuration ∆ | Γ and GR-provable

R-transition sequence ∆ | Γ =⇒^∗ ∆ | Γ^′, where Γ^′ is a GR-contraction of Γ with respect to ∆, there exists a model M of GR-refutation such that both M|= ∆ and Γ_M(∆) = Γ^′ hold, then we say that GR-calculus is GR-sound.

Theorem

(GR-soundness). GR-calculus is GR-sound.

(32)

Completeness of GR-calculus

Definition

(GR-completeness). If for any R-configuration ∆ | Γ and model M of GR-refutation of Γ with respect to ∆, there exists a GR-provable

R-transition sequence ∆ | Γ =⇒^∗∆ | Γ_M(∆), then we say that GR-calculus is GR-complete.

(33)

Soundness of GR-calculus Completeness of GR-calculus

Completeness of GR-calculus

For a countable formula set Γ and a formal theory ∆ consisting of finitely many atomic formulas or negations of atomic formulas, ∆ is a GR-refutation of Γ. Let C(Γ, ∆) denote the set of all the maximal contractions of Γ with respect to ∆, and R(Γ, ∆) denote the set {Γ_M(∆) | M is a model of GR-refutation of Γ with respect to ∆}. Then we have:

Theorem

C(Γ, ∆) = R(Γ, ∆). Theorem

(GR-completeness). GR-calculus is GR-complete.

(34)

References

[1 ] C. E. Alchour´ron, P. G¨ardenfors and D. Makingson, On the logic of theory changes: partial meet contraction and revision functions. J. Symbolic Logic, 50, 510-530 (1985)

[2 ] P. G¨ardenfors, Knowledge in Flux: Modeling the Dynamics of Epistemic States. Bradford Books, MIT Press, Cambridge MA (1988)

[3 ] P. G¨ardenfors and D. Makinson. Revisions of Knowledge Systems Using Epistemic Entrenchment. In: 2nd Conference on Theoretical Aspects of Reasoning about Knowledge, 83-95 (1988)

[4 ] W. Li, A logical framework for evolution of specifications. In: Programming Languages and Systems-ESOP’94, LNCS 788. Berlin: Springer-Verlag, 394-408 (1994)Qingyu He, Jie Ding Generalized R-Calculus

(35)

References

[5 ] W. Li, A Logical Framework for Knowledge Base

Maintenance. J of Comput. Sci. & Technol, 10(3), 193-205 (1995)

[6 ] W. Li, R-calculus: an inference system for belief revision. The Computer Journal, 50(4): 378-390 (2007)

[7 ] W. Li, A development calculus for specifications. Science in China (Series F), 46(5), 390-400 (2003)

[8 ] W. Li, Mathematical logic: foundations for information science. Basel: Birkhaeuser Publish, 1-261 (2009)

(36)

References

[9 ] J. Luo and W. Li, An algorithm to compute maximal contractions for Horn clauses. Scientia Sinica Informationis, 41(2), 129-143 (2011) (in Chinese)

[10 ] J. H. Gallier, Logic for Computer Science: Foundation of Automatic Theorem Proving. New York: Harper & Row (1986)

[11 ] Gierz, G., et al.: Continuous lattices and domains. Cambridge University Press, New York (2003)

(37)

ファイル置き場 Sendai Logic Homepage He20121109

Generalized R-Calculus

Backgrounds

Backgrounds

Backgrounds

Backgrounds

Backgrounds

Backgrounds

A problem related to this topic

A problem related to this topic

A problem related to this topic

A problem related to this topic

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

GR -calculus and Some Related Conclusions

Main Results

Soundness of GR-calculus

Completeness of GR-calculus

Completeness of GR-calculus

References

References

References

Thank You!