1: \documentstyle[11pt]{article}
2:
3: \newtheorem{example}{Example}[section]
4: \newtheorem{lemma}{Lemma}[section]
5: \newtheorem{theorem}{Theorem}[section]
6: \newtheorem{definition}{Definition}[section]
7:
8: \newtheorem{notation}{Notation}[section]
9: \newtheorem{corollary}{Corollary}[section]
10:
11: %%%%\textheight=19.8cm
12: %%%%\textwidth=13.2cm
13:
14: \hoffset=-0.5cm
15: \voffset=1cm
16:
17: %\input{macro.tex}
18:
19: %\textheight=19.3cm
20: %\textwidth=12.2cm
21:
22:
23: \textheight=22cm
24: \textwidth=15cm
25: \oddsidemargin=0.9cm
26: \evensidemargin=0.9cm
27:
28:
29:
30:
31:
32:
33:
34: \begin{document}
35:
36:
37:
38: \begin{center}
39: {\huge \bf A Development Calculus \\[3mm]
40: for Specifications }
41: \end{center}
42:
43: \begin{center}
44: Wei \hspace{5mm} LI
45:
46: \end{center}
47:
48: \begin{center}
49: liwei@nslde.buaa.edu.cn\\
50: State Key Laboratory of Software Development Environment\\
51: Beihang University \\
52: 100083 Beijing, P.R. China
53: \end{center}
54:
55: \vspace{5mm}
56:
57: \noindent {\bf Abstract}
58:
59: A first order inference system, named R-calculus, is defined to
60: develop the specifications. This system intends to eliminate the
61: laws which is not consistent with user's requirements. The
62: R-calculus consists of the structural rules, an axiom, a cut rule,
63: and the rules for logical connectives. Some examples are given to
64: demonstrate the usage of the R-calculus. Furthermore, the
65: properties regarding reachability and completeness of the
66: R-calculus are formally defined and proved.
67:
68: \vspace{3mm}
69:
70: \noindent {\bf Keywords: Specification, Revision, Necessary
71: premise, R-calculus, R-condition}
72:
73:
74: \section{ Motivation}
75:
76: During the development of the specifications, two situations are
77: encountered commonly: First, the specification is not consistent;
78: as a result, a program to satisfy it does not exist. Second, the
79: specification is consistent, but users and designers refuse to
80: accept it since the running results of the generated program does
81: not meet their requirements. Under both circumstances, the
82: specification should be redesigned. If it was indeed the case, the
83: elimination of inconsistent laws and the introduction of new laws
84: become very important; this paper will address this concerns
85: principally. For example, consider the following specification:
86:
87: \[
88: \Gamma \equiv \{ A, A \supset B, B \supset C, E\supset F\}
89: \]
90: where $A$, $B$, $C$, $E$, and $E$ denote some equations. It is
91: obviously that $\Gamma \vdash C$ holds. Users, however, reject
92: $C$ and prefer $\neg C $. In this case, we have to redesign the
93: specification.
94:
95: The purpose of this paper, therefore, concerns principally to
96: build an inference system, named R-calculus to revise the
97: specifications. The nature of R-calculus differentiates it from
98: many well known inference systems of specifications. The purpose
99: of the latter aims to deduce the correct programs to satisfy a
100: given specification[10,11,12,13]. However, R-calculus emphasizes
101: on revising the specifications, and eliminating the laws which are
102: not consistent with user's requirements.
103:
104: The R-calculus is indeed a transition system which consists of the
105: structural rules, an axiom, an cut rule, and the rules of logical
106: connectives. Some examples are given to demonstrate how the
107: R-calculus can be used to develop specifications. Furthermore, the
108: properties of the R-calculus, such as reachability and
109: completeness, are formally defined and proved.
110:
111:
112: \section{The Necessary Premise}
113:
114: In order to avoid the syntactical details, in this paper,
115: the first order languages are chosen to be the specification languages
116: [1]. Briefly, a first order language $\cal L$ has two sets of
117: symbol strings. They are the set of terms and the set of formulas.
118: The set of terms is defined on the set of variable symbols {\bf V}
119: ranged over by $x,y,z \cdots $, the set of function symbols {\bf
120: F} ranged over by $f,g,h \cdots $, and the set of constants
121: symbols {\bf C} ranged over by $a,b,c \cdots$, and it is defined
122: inductively as below:
123: \[
124: t~ ::=~ c~ | ~x~ |~ f(t_1, t_2, \cdots, t_n)
125: \]
126: The set of formulas are defined on the set of predicates $\bf P$
127: ranged over by $P,Q, R, \cdots$,
128: and the set of logical connectives including:
129: $\neg$, $\land$, $\lor$, $\supset$, $\forall$, $\exists$,
130: and it is defined inductively as the following,
131: \[
132: A~::=~P(t_1, t_2, \cdots, t_n)~|~ \neg A~|~A \land B~|~A\lor B~|~
133: A \supset B~| \forall x.A ~|~ \exists x. A
134: \]
135:
136: In this paper, $\Gamma$ is used to denote a formal theory,
137: which is a finite set of formulas. $Th(\Gamma)$ denotes
138: the set of all logical consequences of $\Gamma$.
139: $\Gamma \vdash A$ is called a sequent, where
140: $A$ is a logical consequence of $\Gamma$ [1,2],
141: $\vdash $ is the deductive relation.
142: A Gentzen style inference system, such as {\bf G} system [1] is
143: employed for the logical analysis of the specifications.
144: Each inference rule of LK is described by a fraction of number of sequents.
145: A proof tree {\bf T} of the sequent $\Gamma \vdash A$ is a finite tree structure,
146: where every node of {\bf T} is a sequent, the node and its direct sons
147: forms an application of an inference rule of the {\bf G} system,
148: the root of {\bf T} is $\Gamma \vdash A$, and every leaf of {\bf T} is
149: an axiom.
150:
151: \begin{definition}
152: \rm
153: Necessary premise
154:
155: Let $\Gamma \vdash A$, and {\bf T} be its proof tree. Let $P$, $Q$,
156: and $R$ be formulas in {\bf T}. $P$ is
157: premise of $Q$, if and only if the following items hold:
158:
159: \begin{enumerate}
160:
161: \item If $\Gamma',P \vdash P$ is a leaf of {\bf T},
162: then the $P$ on the left hand side of $\vdash$ is the
163: premise of the $P$ on the right hand.
164:
165: \item If the node of {\bf T} is an application of a right rule,
166: $Q$ is one of $A\land B$, $A \lor B$,$A \supset B$, $\neg A$,
167: $\forall x.A$, and $\exists x.A$, which is a principal formula [1]
168: in the denominator of the inference rules, and $P$ is one of
169: $A$,$B$,$A[t/x]$, and $A[y/x]$, which is a side formula [1] in the
170: numerator of the corresponding inference rule,then $P$ is
171: the premise of $Q$.
172:
173: \item If the node of {\bf T} is an application of a left rule, and
174: $Q'$ is one of $A\land B$, $A \lor B$,$A \supset B$, $\neg A$,
175: $\forall x.A$, and $\exists x.A$,
176: which is a principal formula in the denominator of the inference rules,
177: then $Q'$ is the premise of $A$,$B$, $A[t/x]$, and
178: $A[y/x]$, which is a side formula in the numerator of the
179: corresponding inference rule.
180: Every one of $A$,$B$, $A[t/x]$, and $A[y/x]$ is
181: necessary premise of the formula on the right hand side of
182: $\vdash$ in the denominator.
183:
184: \item If $P$ is $Q$'s premise, and $Q$ is $R$'s necessary,
185: then $P$ is $R$'s necessary premise.
186:
187: \end{enumerate}
188:
189: Let ${\cal P}_{\mbox{\small \bf T}}(\Gamma, A)$ be the set of premise of $A$ in the proof tree {\bf T}. If $P \in
190: \Gamma$ holds and $P$ is the premise of $A$ in {\bf T}, precisely, $P \in \Gamma \cap {\cal P}_{\mbox{\small \bf T}}(\Gamma, A)$,
191: $P$ is the {\b necessary} premise of $A$ in {\bf T}, which can be
192: written as $P \mapsto_{\mbox{\small \bf T}} A$. \hfill $Box$
193:
194: \end{definition}
195:
196: According to definition 2.1, for any given $\Gamma \vdash A$, the necessary premise of $A$ depends on the proof tree {\bf T}. However, whenever $\Gamma \vdash A$ holds, its proof tree exists.
197: Thus, for the reason to simplify the writings, sometimes the tree {\bf T} is omitted from $\mapsto $ and the related notation will be written as $P \mapsto A$
198: when there does not exist confusion in the context.
199:
200:
201: \begin{example}
202: \rm $\land$- right rule:
203: \[
204: \frac{\Gamma \vdash A~~~\Gamma \vdash B}{\Gamma \vdash A\land B}
205: \]
206: $A$ and $B$ are the necessary premise of $A \land B$.
207:
208: \end{example}
209:
210: \begin{example}\
211:
212: \rm
213: Consider the sequent: $C,A,\forall x ( A \supset
214: B(x))\vdash \exists x B(x)$. Its proof tree is the following:
215:
216: \vspace{3mm}
217:
218: \noindent \mbox{}\hspace{-2mm} {\small $
219: \begin{array}{c}
220: \underline{C,A^{\ast 4},(\forall x(A\supset B(x)))^{\ast 2},(A
221: \supset B[t/x] )^{\ast 2} \vdash A^{\ast 3}\ \ \ \ \ C,A,(\forall
222: x(A\supset B(x)))^{\ast 2},(B[t/x])^{\ast 3}
223: \vdash B[t/x]^{\ast 1}}\\
224: \hspace{2.5cm}\underline{ C,A,(\forall x (A\supset B(x)))^{\ast
225: 2},(A\supset B[t/x] )^{\ast 2}
226: \vdash B[t/x]^{\ast 1}} \\
227: \hspace{3cm}\underline{ C,A,(\forall x (A\supset B(x)))^{\ast 2 } \vdash B[t/x]^{\ast 1}} \\
228: \hspace{3.5cm} C,A,\forall x(A\supset B(x)) \vdash \exists x B(x)
229: \end{array}
230: $ }
231:
232: \vspace{2mm}
233:
234:
235: The first node is an application of the $\exists$-right rule.
236: $B[t/x]$ is premise of $\exists x B(x)$. We use
237: superscript $\ast$ to denote the premise, and use
238: number $1$ to denote the first node. The second node is an
239: application of the $\forall$-left rule. According to
240: definition 2.1, $(\forall x (A\supset B(x)))^{\ast 2}$ on the left
241: hand of $\vdash $ in the denominator of the node 2 is the
242: premise of $(A \supset B[t/x])^{\ast 2}$ on the left hand of
243: $\vdash$ in the numerator, and $(A\supset B[t/x])^{\ast 2}$ is
244: also the premise of $ B[t/x]^{\ast 1}$. The third node
245: of the proof three is an application of $\supset$-left rule.
246: According to definition 2.1, $(A\supset B[t/x])^{\ast 2}$ is
247: the premise of $A^{\ast 3}$ on the right hand of
248: $\vdash$ of the first sequent in the numerator, and is also the
249: premise of $ B[t/x]^{\ast 3}$ on the left hand of
250: $\vdash$ of the second t in the numerator. $A^{\ast 3}$ and
251: $B[t/x]^{\ast 3}$ are the premise of $ B[t/x]^{\ast 1}$
252: on the right hand of $\vdash$ in the denominator of the node 3.
253: The forth node is an application of the axiom. $A^{\ast 4}$ on the
254: left hand of $\vdash$ is the premise of $A^{\ast 3}$ on
255: the right hand. The fifth node is also an application of the
256: axiom. $ B[t/x]^{\ast 3}$ on the left hand of $\vdash$ is the
257: premise of $ B[t/x]^{\ast 1}$ on the right. Thus, the
258: set of numbers of the premise of the proof three is
259: \[
260: \{ B[t/x] ,\forall x (A\supset B(x)),A\supset B[t/x],A \}
261: \]
262: According to the definition 2.1, the necessary premise of $\exists x.B(x)$
263: of the sequent $C,A,\forall x( A\supset B(x))\vdash \exists x.B(x)$ is:
264: \[
265: \{A,\forall x (A\supset B(x))\}
266: \]
267: \hfill $\Box$
268:
269: \end{example}
270:
271: \begin{lemma}
272: \rm
273:
274: Let $\Gamma \vdash A$ and {\bf T} be its proof tree.
275: The set ${\cal P}(\Gamma, A)$ is decidable.
276: \end{lemma}
277:
278:
279: \noindent {\bf Proof.} According the definition of the
280: necessary premise, an algorithm can be designed in the following way:
281: Its input is the proof tree, and its output is the set ${\cal P}(\Gamma, A)$.
282: The algorithm computes the premise from the root of {\bf T} to the leaves of
283: {\bf T} as shown in the above example2.2.
284: Since the proof tree {\bf T} is finite, the algorithm will be halt. \hfill $\Box$
285:
286:
287: In this paper, the finite formal theories of $\cal L$ are used to describe the
288: specifications.
289:
290: \begin{definition}
291:
292: Specification
293:
294: \rm
295:
296: A finite consistent set $\Gamma$ of the sentences is called a
297: specification. The sentences contained in $\Gamma$ are called the
298: laws of the specification.
299:
300: \end{definition}
301:
302: We assume that two sentences $P$ and $Q$ are the same sentence
303: if and only if $P \equiv Q$ (that is ($P \supset Q) \land (Q\supset P$)
304: is a tautology).
305:
306: A model ${\bf M}$ is a pair $<M,I>$, where $M$ is a non
307: empty set and it is called domain,
308: $I$ is a map and it is called interpretation.
309: The form ${\bf M} \models A$ means that
310: for the given domain $M$ and the interpretation $I$, $A$ is true in $M$.
311: ${\bf M} \models \Gamma $ mean that for every $A \in \Gamma$, ${\bf M} \models A$.
312:
313: \begin{definition}
314: \rm
315:
316: $A$ is called a logical consequence of $\Gamma$
317: and is written as $\Gamma \models A$,
318: if and only if for every {\bf M}, if ${\bf M} \models \Gamma$, then
319: ${\bf M} \models A$ holds.
320:
321: \end{definition}
322:
323:
324:
325: \section{The User's rejections}
326:
327: As we mentioned before, the users reject a specification when they
328: have found its counter example. In the first order logic, the user's
329: rejection can be defined by the models.
330:
331: \begin{definition}
332: \rm
333: User's rejection
334:
335:
336: Let $\Gamma \models A$. A model ${\bf M}$ is called a
337: user's rejection of $A$ if and only if ${\bf M} \models \neg A$. Let
338: \[
339: \Gamma_{M(A)}\equiv \{ A_{i} \mid A_{i} \in
340: \Gamma, \hspace{3mm} {\bf M} \models A_{i}, \hspace{3mm}
341: {\bf M} \models \neg A \}
342: \]
343:
344: {\bf M} is called an {\em ideal} user's rejection of $A$ if and only if
345: $\Gamma_{M(A)}$ is {\em maximal} in the sense that there does not
346: exist another user's rejection ${\bf M'}$ of $A$,
347: such that $\Gamma_{M(A)} \subset \Gamma_{M'(A)}$.
348:
349: \end{definition}
350:
351: The above definition describe the following situation that $\Gamma
352: \vdash A$, but the users or designers have found a counter
353: example ${\bf M}$ that makes $\neg A$ true. $\Gamma_{M(A)}$ is a
354: subset of $\Gamma$ which does not contradict to $\neg A$. The
355: user's rejection meets the intuition that whether a specification
356: is accepted, depends only on whether its logical consequences
357: agree with user's requirements. The ideal user's rejection meets
358: the Occam's razor, which says: {\em Entities are not to be
359: multiplied beyond necessity}[3]. Here, it means that if a logical
360: consequence deduced from a specification is rejected by the users,
361: then the maximal subsets of the specification which is consistent
362: with the user's rejection must be retained and are assumed to be
363: true in the current stage of the development of the specification,
364: but the rest of laws contained in the specification must be
365: removed because they lead to the user's rejection.
366:
367: In the rest of the paper, we consider ideal user's rejections
368: only, and simply call them user's rejections. Sometimes, we even
369: say that $\neg A$ is a user's rejection of $\Gamma$, it means that
370: $\Gamma \vdash A$ and there is an ideal user's rejection {\bf M}
371: and ${\bf M} \models \neg A$.
372:
373:
374: \begin{definition}
375: \rm
376:
377: (Maximal contraction).
378:
379: Let $\Gamma \vdash A$ and $\Lambda \subset \Gamma$. $\Lambda$ is
380: called a maximal contraction of $\Gamma$ by $\neg A$ if it is a maximal
381: subset of $\Gamma$ and is consistent with $\neg A$.
382:
383: \end{definition}
384:
385:
386:
387: \begin{example}\
388:
389: \rm
390:
391: Let $\Gamma \equiv \{ A, A \supset B, B \supset C, E\supset F\} $.
392: It can be proved that $\Gamma \vdash C$ holds.
393: Let $\neg C $ be a user's rejection. It cab be verified that
394: there are three maximal contractions:
395:
396: \[
397: \{ A, A \supset B, E\supset F \},~~
398: \{ A, B \supset C, E\supset F \},~~
399: \{ A \supset B, B \supset C, E\supset F \}.
400: \]
401:
402: \end{example}
403:
404: \begin{lemma}\
405:
406: \rm
407:
408: If $\Gamma \vdash A$ and $\Lambda$ is a maximal
409: contraction of $\Gamma$ by $\neg A$, then
410: there exists a user's rejection {\bf M} of
411: $\Gamma$ by $A$ and ${\bf M} \models \neg A$ holds.
412:
413: \end{lemma}
414:
415: \noindent {\bf Proof:} The proof is directly from the definition.
416:
417: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
418:
419: \section{ The R-calculus}
420:
421: The purpose of this section is to build an inference system about
422: logical connectives to remove the laws which is not consistent
423: with a given user's rejection.
424: It is called R-calculus. For a given $\Gamma \vdash A$,
425: the R-calculus is used to derive all maximal contractions of $\Gamma$ by $\neg A$.
426: In fact, if $\Gamma$ is not consistent,
427:
428:
429: the R-calculus is still employed to derive all maximal subsets of $\Gamma$
430: that is consistent with $\neg A$.
431:
432: In order to define the calculus, for a formal theory $\Gamma$,
433: a concept called R-condition of $\Gamma$ is to be introduced.
434: The R-condition is a kind of mirror reflection of the concept of T-condition
435: used in the forcing theory [8].
436:
437:
438: \begin{definition}
439: \rm
440: R-condition of $\Gamma$
441:
442: Let $\Gamma$ be a specification and $\Delta$ be a finite consistent
443: set of atomic formulas and the negations of atomic formulas.
444: $\Delta$ is called an R-condition of $\Gamma$,
445: if and only if for every $A \in \Delta$, $\Gamma \vdash \neg A$ holds.
446:
447: \end{definition}
448:
449: \begin{lemma}\
450:
451: Let $\Gamma$ be a specification and $\Delta$ be a R-condition of $\Gamma$.
452: If $A \in \Delta$, then $A$ is a user's rejection of $\Gamma$.
453:
454: \end{lemma}
455:
456: \noindent {\bf Proof.} The proof is directly from the definition.
457:
458:
459: \begin{definition}
460: \rm
461: R-configuration
462:
463: \[
464: \Delta|\Gamma
465: \]
466: is called a R-configuration, if and only if $\Gamma$ is
467: a specification and $\Delta$ is a R-condition of $\Gamma$.
468: The R-configuration
469: $\Delta|\Gamma$ is read as $\Delta$ overrides $\Gamma$.
470:
471: \end{definition}
472:
473:
474: $\Delta$ and $\Gamma$ can be written as sequences, such as
475: $A,B,\Delta_1$ and $A,B, \Gamma'$, etc.
476: Let $Delta$ be $A_1, A_2,\cdots, A_n$.
477: According to the above definitions, the R-configuration
478: $\Delta|\Gamma$ implies that
479: $\Gamma \vdash \neg A_1 \land \neg A_2, \cdots, \land A_n$ holds.
480: Let its proof tree be denoted by {\bf T}.
481:
482:
483:
484: \begin{definition}
485: \rm
486: R-transition
487:
488: \[
489: \Delta\mid\Gamma \Longrightarrow \Delta'\mid\Gamma'
490: \]
491: is called a R-transition. It means that the configuration
492: $\Delta\mid\Gamma$ is transformed to $\Delta'\mid\Gamma'$.
493:
494: $\Longrightarrow^{*}$ denotes a sequence of the transitions.
495: $*$ denotes finite times of transitions but also infinite
496: times and 0 times of transitions. The following R-transition
497: \[
498: \Delta\mid A, \Gamma \Longrightarrow \Delta\mid\Gamma
499: \]
500: means that $\Delta\mid\Gamma, A$ is transformed to $\Delta\mid\Gamma$,
501: and $A$ is deleted during the transition.
502:
503: \end{definition}
504:
505: R-calculus contains four kinds of transformation rules.
506: They are structural rules, the R-axiom, the R-cut rule
507: and the rules of logical connectives. As mentioned before,
508: for the writing simplicity, the proof tree is omitted from
509: $\mapsto$ and $\Longrightarrow $.
510:
511: \vspace{3mm}
512:
513: \noindent {\bf Structural rules}
514:
515: \begin{definition}\
516: \rm
517:
518: Contraction
519:
520:
521: \[
522: \Delta \mid A, A, \Gamma \Longrightarrow \Delta \mid A, \Gamma
523: \hspace{10mm}
524: A, A, \Delta \mid \Gamma \Longrightarrow A, \Delta \mid \Gamma
525: \]
526:
527: Exchange
528: \[
529: \Delta \mid A, B, \Gamma \Longrightarrow \Delta \mid B, A, \Gamma
530: \hspace{10mm}
531: A, B, \Delta \mid \Gamma \Longrightarrow B, A, \Delta \mid \Gamma \]
532: \end{definition}
533:
534: The contraction rules mean that the same formulas occurring on one side
535: can be contracted to one. The exchange rules say that
536: a formula can be moved from one position to another
537: within one side of a configuration.
538:
539:
540: \begin{definition}
541:
542: \rm
543: R-axiom
544:
545: \[
546: A, \Delta \mid \neg A, \Gamma \Longrightarrow A, \Delta \mid \Gamma
547: \]
548:
549: \end{definition}
550:
551: The R-axiom means that if $A$ (the atomic formula or the negation of
552: atomic formula) occurs on the left hand side and its negation $ \neg A $
553: occurs on the right hand side, then $ \neg A $ must be deleted.
554:
555: \begin{definition}
556: \rm
557: R-cut rule
558: \[
559: \frac{\Gamma_{1},A \vdash B~~~A \mapsto B~~~B,\Gamma_{2} \vdash C~~~\Delta \mid
560: C,\Gamma_{2}\Longrightarrow \Delta \mid \Gamma_{2} }{ \Delta
561: \mid \Gamma_1, A, \Gamma_2 \Longrightarrow \Delta \mid \Gamma_1,
562: \Gamma_2}
563: \]
564: \end{definition}
565:
566:
567: Where $\Gamma = \Gamma_1, A, \Gamma_2$ and $ \Delta =\neg C,
568: \Delta'$. The R-cut means that $C$ is an atomic formula or the
569: negation of an atomic formula, and $C$ is not consistent with
570: $\Delta$. Furthermore, $B$ is a lemma used in the proof of $C$,
571: $A$ is contained in $\Gamma$ and is the necessary premise of
572: $B$. In this circumstance, $A$ must be eliminated.
573:
574: \vspace{3mm}
575:
576: \noindent {\bf Logical rules}
577:
578: \vspace{2mm}
579:
580: \begin{definition}
581: \rm
582: R-$\land$ rule
583:
584: \[
585: \frac{\Delta \mid A, \Gamma \Longrightarrow \Delta \mid \Gamma}{
586: \Delta \mid A \land B, \Gamma \Longrightarrow \Delta \mid \Gamma}
587: \hspace{1cm} \frac{\Delta \mid B, \Gamma \Longrightarrow \Delta
588: \mid \Gamma}{ \Delta\mid A \land B, \Gamma \Longrightarrow \Delta
589: \mid \Gamma}
590: \]
591: \end{definition}
592:
593: $A$ occurring in the numerator of the R-$\land$ rule means
594: that $\Delta \vdash \neg A$ holds. According to the $\land$ rule of
595: {\bf G} system, $\Delta \vdash \neg A \lor \neg B$ holds. That is
596: $\Delta \vdash \neg (A \land B)$ holds. Therefore, if $A$ is deleted,
597: then $A \land B$ must be deleted. Similarly, for the rule on the right,
598: if $B$ is deleted, then $A \land B$ must be deleted.
599:
600:
601: \begin{definition}
602: \rm
603:
604: R-$\lor$ rule
605:
606: \[
607: \frac{\Delta \mid A, \Gamma \Longrightarrow \Delta \mid \Gamma \hspace{1cm}
608: \Delta \mid B, \Gamma \Longrightarrow \Delta \mid \Gamma }{\Delta
609: \mid A \lor B, \Gamma \Longrightarrow \Delta \mid \Gamma }
610: \]
611:
612: \end{definition}
613:
614: Since $A$ and $B$ occurring in the numerator of R-$\lor$ rule
615: are going to be deleted, $\Delta \vdash \neg A$ and $\Delta \vdash
616: \neg B$ hold. According to the $\lor$ rule of the {\bf G} system,
617: $\Delta \vdash \neg A \land \neg B$ holds. The later implies $\Delta \vdash
618: \neg (A \lor B)$. Therefore, $A \lor B$ must be deleted.
619:
620:
621: \begin{definition}\
622: \rm
623: R-$\supset$ rule
624:
625: \[
626: \frac{\Delta \mid \neg A, \Gamma \Longrightarrow \Delta \mid
627: \Gamma \hspace{1cm} \Delta \mid B, \Gamma \Longrightarrow \Gamma}{
628: \Delta \mid A \supset B, \Gamma \Longrightarrow \Delta \mid
629: \Gamma}
630: \]
631: \end{definition}
632:
633: The R-$\supset$ rule holds since $(A \supset B ) \equiv (\neg A
634: \lor B)$.
635:
636:
637: \begin{definition}
638: \rm
639:
640: R-$\forall$ rule
641:
642: \[
643: \frac{\Delta \mid A[t/x], \Gamma \Longrightarrow \Delta \mid \Gamma}{\Delta
644: \mid \forall x A, \Gamma \Longrightarrow \Delta \mid \Gamma}
645: \]
646:
647: where $t$ is a term and is free in $A$ for $x$.
648: \end{definition}
649:
650:
651:
652: Since $ A[t/x]$ occurring in the numerator of the R-$\forall$ rule
653: is to be deleted, $\Delta \vdash \neg A[t/x]$ holds. It implies $\Delta
654: \vdash \neg \forall x A[x]$. Thus, $\forall x A[x]$ must be deleted.
655: R-$\forall$ means that if $ A[t/x]$ is not consistent with
656: $\Delta$, then $\forall x A(x)$ can not be consistent with $\Delta$.
657:
658:
659: \begin{definition}
660: \rm
661: R-$\exists$ rule
662:
663: \[
664: \frac{\Delta \mid A[y/x], \Gamma \Longrightarrow \Delta \mid
665: \Gamma}{\Delta \mid
666: \exists x A, \Gamma \Longrightarrow \Delta \mid \Gamma}
667: \]
668: $y$ is an eigenvariable and it does not occur in the denominator
669: of the rule.
670:
671: \end{definition}
672:
673:
674: If $A[y/x]$ is to be deleted in the numerator of the R-$\exists$ rule, then
675: $\Delta \vdash \neg A[y/x]$. According to the $\exists$ rule of the
676: {\bf G} system, $\Delta \vdash \neg \exists x A(x)$ holds.
677: Therefore, $\exists x A(x)$ must be deleted.
678: This rule means that for any eigenvariable $y$,
679: if $ A[y/x]$ is not consistent with
680: $\Delta$, then $\exists x A(x)$ is not consistent with $\Delta$.
681:
682: \begin{definition}
683: \rm
684: R-$\neg$ rule
685:
686: \[
687: \Delta \mid A, \Gamma \Longrightarrow \Delta \mid A', \Gamma
688: \]
689:
690: $A$ and $A'$ are defined as below:
691:
692: \vspace{3mm}
693:
694: \begin{tabular}{|c|c|c|c|c|c|c|} \hline
695: $A$ & $\neg (B \land C)$ & $\neg (B \lor C)$ & $\neg \neg B$ &
696: $\neg (B \supset C)$ & $\neg \forall x. B$ & $\neg \exists x. B$
697: \\ \hline $A'$ & $\neg B \lor \neg C$ & $\neg B \land \neg C$ &
698: $B$ & $ B \land \neg C $ & $ \exists x. \neg B$ & $\forall x. \neg
699: B$ \\\hline
700: \end{tabular}
701: \end{definition}
702:
703:
704: R-$\neg$ rule is an expansion rule. $\neg A$ occurring on the
705: left of the long right arrow is substituted by its equivalent
706: $A'$, and the "$\neg$" goes to the next level.
707:
708: \begin{definition}
709: \rm
710:
711: R-calculus
712:
713: R-calculus is the set which consists of the structural rules, the
714: R-axioms, the R-cut rule, the R-$\land$ rule, the R-$\lor$ rule,
715: the R-$\supset$ rule, the R-$\forall$ rule, the R-$\exists$ rule,
716: and the R-$\neg$ rule.
717:
718: An R-configuration $\Delta \mid \Gamma$
719: is called an
720: R-termination if there does not exist an R-rule
721: that can be applied to $\Delta \mid \Gamma$
722: with the exception of the structural rules.
723:
724: \end{definition}
725:
726: In summary, every R-configuration $\Delta | \Gamma $ consists two
727: parts: the left part $\Delta$ is a finite consistent set of atomic
728: formulas and the negations of atomic formulas, the right part
729: $\Gamma$ is a finite set of sentences which may not be
730: consistent. For every $A \in \Delta$, $A$ is a user's rejection of
731: $\Gamma$. The R-calculus is an inference system. It can be used to
732: eliminate those laws which are not consistent with
733:
734: ¡¡¡¡¡¡¡¡$\Delta$.
735: The principles of eliminating are as below: The
736: law $A$ of $\Gamma$ (on the right hand side of $|$) is
737: to be eliminate if its negation $ \neg A$ occurs in $\Delta$ (on
738: the left hand side of $|$). If $A$ of $\Gamma$ is a
739: compound sentence, then whether $A$ is to be eliminated depends on
740: the eliminations of the components of $A$ and the meaning of the
741: logical connective occurring in $A$. The rule for a logical
742: connective of R-calculus is a mirror reflection of the rule for
743: the same logical connective of the first order inference system.
744:
745:
746: \section{Some Examples}
747:
748: The following three examples are given to show how the R-calculus
749: can be used to delete the laws of $\Gamma$ which is not consistent
750: with its user's rejection.
751:
752: \begin{example}\
753:
754: \rm
755:
756: Let $\Gamma \equiv\{ \forall x. A(x), \Gamma'\}$ and
757: $\Delta \equiv \{\neg A[c]\}$ holds. The latter means that we must accept
758: $\neg A[c]$, where $c$ is a constant. According to the R-axiom,
759:
760: \[
761: \neg A[c]~ |~ A[c], \Gamma' \Longrightarrow
762: \neg A[c]~ |~ \Gamma'
763: \]
764: holds. By the R-$\forall$ rule,
765: \[
766: \frac{ \neg A[c]~ |~ A[c], \Gamma' \Longrightarrow
767: \neg A[c]~ |~ \Gamma'}{ \neg A[c]~|~ \forall x A(x), \Gamma'
768: \Longrightarrow \neg A[c]~ |~ \Gamma'}
769: \]
770: holds. Thus, it is proved by the R-calculus that
771: $\forall x A(x)$ is not consistent with $\neg A[c]$.
772: and it should be eliminated from $\Gamma$. \hfill $\Box$
773:
774: \end{example}
775:
776:
777: The following example demonstrates how to use the R-cut rule.
778:
779: \begin{example}
780: \rm
781:
782: Consider the example given in the beginning of the paper. Let
783:
784: $$
785: \Gamma \equiv \{ A, A \supset B, B \supset C, E\supset F\}
786: $$
787:
788:
789: $\Gamma \vdash C$ holds. Suppose $\neg C$ is a user's rejection.
790: According to the definition, there exists three maximal
791: contraction of $\Gamma$ by $\neg C$:
792: \[
793: \{ A, A \supset B, E\supset F \}, \hspace{5mm}
794: \{ A, B \supset C, E\supset F \} \hspace{5mm}
795: \{ A \supset B, B \supset C, E\supset F \}.
796: \]
797:
798: In fact, each one of the above three can be derived by the R-calculus.
799: Consider $\{ A, A \supset B, E\supset F \}$ first. Let
800: \[
801: \Gamma_1 \equiv \{ A, A \supset B\}~~~
802: \Gamma_2 \equiv \{ E\supset F\}.
803: \]
804: By the {\bf G} system, both
805: \[
806: \Gamma_1,B\supset C \vdash C~~\mbox{and}~~C,\Gamma_2 ~ \vdash C
807: \]
808: hold. According to the definition 2.1, $B\supset C$ is the necessary premise of $C$
809: and $B\supset C \mapsto C$ holds.
810: \[
811: \neg C \mid C, \Gamma_2 \Longrightarrow \neg C \mid \Gamma_2
812: \]
813: holds by the R-axiom. the R-cut rule is then applied and
814: \[
815: \neg C \mid \Gamma_1, B\supset C, \Gamma_2 \Longrightarrow
816: \neg C \mid \Gamma_1,\Gamma_2
817: \]
818: hold. Here $\Gamma_1,\Gamma_2$ is just $\{ A, A \supset B, E\supset F \}$.
819:
820: Consider the second maximal contraction $\{ A, B \supset C, E\supset F \}$. Let
821:
822: \[
823: \Gamma_1 \equiv \{ A\}~~~
824: \Gamma_2 \equiv \{ B \supset C,E\supset F\}.
825: \]
826: By the {\bf G} system,
827: \[
828: \Gamma_1,A\supset B~ \vdash ~ B~~\mbox{and}~~B,\Gamma_2 ~ \vdash C~~\mbox{hold.}
829: \]
830: Notice that $A\supset B$ is the premise of $B$ and
831: is in $\Gamma$. Thus, $A\supset B \mapsto B$ holds. According to the R-axiom,
832: \[
833: \neg C \mid C, \Gamma_2 \Longrightarrow \neg C \mid \Gamma_2
834: \]
835: holds. Thus, the R-cut rule is applied and
836: \[
837: \neg C \mid \Gamma_1, A\supset B, \Gamma_2 \Longrightarrow
838: \neg C \mid \Gamma_1,\Gamma_2
839: \]
840: holds. Here $\Gamma_1,\Gamma_2$ is $\{ A, B \supset C, E\supset F \}$.
841: Finally, Let
842: \[
843: \Gamma_1 \equiv \emptyset~~~
844: \Gamma_2 \equiv \{ A\supset B, B \supset C,E\supset F\}.
845: \]
846:
847: Using the similar proof strategy, the third maximal contraction
848: $\{ A \supset B, B \supset C, E\supset F \}$ can derived by
849: the R-calculus. \hfill $\Box$
850:
851: \end{example}
852:
853: In the above two examples, $\Gamma$ is a finite consistent set of laws.
854: The following example shows that if $\Gamma$ is not consistent,
855: the R-calculus still works to deduce all of maximal subset
856: of $\Gamma$ which is consistent with $\Delta$.
857: :
858:
859: \begin{example}\
860:
861: \rm
862:
863: Let $\Delta =\{x=x\}$ and $\Gamma=\{f(x)=y,~f(y)=z,~\neg
864: (f(f(x))=z)\}$. Obviously, $\Gamma$ is not consistent. But the R-cut
865: rule can be applied to deduce the maximal subsets which is consistent
866: with $\Delta$. For example, let $\Gamma_1=\{f(x)=y\}$,
867: $\Gamma_2=\{\neg (f(f(x))=z)\}$.
868: First,
869: \[
870: \Gamma_1,~(f(y)=z) \vdash f(f(x))=z~~\mbox{and}~~(f(f(x))=z),
871: ~\Gamma_2 \vdash \neg (x=x)
872: \]
873: holds. It is proved that $(f(y)=z)$ is the necessary premise of
874: $f(f(x))=z$. According to the R-axiom,
875: \[
876: (x=x)~| \neg (x=x) \Longrightarrow (x=x) | \emptyset
877: \]
878: holds. Therefore, by the R-cut rule,
879: \[
880: (x=x)|~\{f(x)=y,~f(y)=z,~\neg (f(f(x))=z)\} \Longrightarrow
881: (x=x)|~\{f(x)=y,~\neg (f(f(x))=z)\}
882: \]
883: holds. It can be verified that $\{f(x)=y,~\neg (f(f(x))=z)\}$ is a maximal subset of $\Gamma$ and is consistent with $x=x$.
884: \hfill $\Box$
885:
886: \end{example}
887:
888: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
889: \section{ The Reachability and Completeness }
890:
891: >From the examples given in the last section, we have found that
892: for the given $\Gamma$ and $\Delta$, every maximal contraction of
893: $\Gamma$ by $\Delta$ can be deduced by the R-calculus. This fact
894: is called the reachability of the R-calculus.
895:
896: \begin{definition}
897: \rm
898:
899: R-reachabilty
900:
901: Let $\Delta \mid \Gamma$ be any given R-configuration, $\Gamma$ be
902: a specification, and $\Delta$ be an R-condition of $\Gamma$. The
903: R-calculus is reachable, if and only if for any given maximal
904: contraction $\Gamma'$ of $\Gamma$ by $\Delta$, there exists an
905: R-transition sequence such that
906: \[
907: \Delta \mid \Gamma \Longrightarrow^{*} \Delta \mid \Gamma'
908: \]
909: holds, where $\Delta \mid \Gamma'$ is an R-termination.
910:
911: \end{definition}
912:
913: \begin{lemma}\
914: \rm
915:
916: Let $\Delta \mid \Gamma$ be a given R-configuration,
917: $\Gamma$ be a specification, and $\Delta$ be
918: an R-condition of $\Gamma$.
919: If $\Gamma_1$ is a maximal contraction of $\Gamma$ by $\Delta$,
920: then there exists a sequence of R-transitions, such that
921: \[
922: \Delta \mid \Gamma \Longrightarrow^{*} \Delta \mid \Gamma_1
923: \]
924: holds.
925:
926: \end{lemma}
927:
928: \noindent {\bf Proof.} Consider the simple case that $\Delta$
929: contains only one element, $\Delta \equiv \{ \neg A \}$, and $A $
930: is an atomic formula or the negation of atomic formula.
931: $\Gamma \vdash A$ holds. Let
932: $\Gamma_1$ be a maximal contraction of $\Gamma$ by $\neg A $, and
933: let $\Gamma_2 \equiv \Gamma - \Gamma_1$.
934:
935: The aim is to prove that for any $B \in \Gamma_2$, $B$ will be
936: eliminated by the R-calculus. To do so, let $\Gamma_3 \equiv
937: \Gamma_2-\{B\}$. Thus, $\Gamma=\Gamma_3,B,\Gamma_1$.
938: First, $\Gamma_3,B \vdash B$ holds. Second, $B$ on the left of
939: $\vdash$ is the necessary premise of $B$ on the right of
940: $\vdash$. Since $\Gamma_1$ is a maximal contraction
941: of $\Gamma$ by $\neg A$, $\Gamma_1,B \vdash A$ holds.
942: \[
943: \neg A \mid A, \Gamma_1 \Longrightarrow \neg A~\mid \Gamma_1
944: \]
945: is an application of the R-axiom. By the R-cut rule,
946:
947: \[
948: \frac{\Gamma_3,B \vdash B~~~B \mapsto B~~~\Gamma_1,B \vdash A~~~
949: \neg A \mid A, \Gamma_1 \Longrightarrow \neg A~\mid \Gamma_1}
950: {\neg A \mid \Gamma_3,B, \Gamma_1 \Longrightarrow \neg A~\mid
951: \Gamma_3, \Gamma_1}
952: \]
953:
954: Thus, $B$ is eliminated. Therefore, every law
955: of $\Gamma_2$ should be eliminated by the R-calculus.
956: \hfill $\Box$
957:
958: The converse of the lemma is not true. For every sequence of R-transitions:
959: \[
960: \Delta \mid\Gamma \Longrightarrow^{*} \Delta' \mid \Gamma'
961: \]
962: where $\Delta' \mid \Gamma'$ is an R-termination, $\Gamma'$ may
963: not be a maximal contraction of $\Gamma$ by $\Delta$. Consider the
964: following example:
965:
966: \begin{example}
967: \rm
968: Let
969: $$
970: \Gamma \equiv \{ A, A \supset B, B \supset C, A \supset E, E\supset C\}
971: $$
972:
973: $\Gamma \vdash C$ holds. Suppose that $C$ is rejected by the
974: users. Using the R-cut rule, We can eliminate $A\supset B$. And
975: then, since
976: $$
977: A, A \supset E, E\supset C \vdash C
978: $$
979: we apply the R-cut rule again and eliminate $A$. Thus, we have:
980: $$
981: \{ B \supset C, A \supset E, E\supset C \}.
982: $$
983: The above set is not a maximal contraction of $\Gamma$ by $\neg
984: C$. The maximal contraction is
985: \[
986: \{ A \supset B, B \supset C, A \supset E, E\supset C \}.
987: \]
988: \hfill $\Box$
989:
990: \end{example}
991:
992:
993: \begin{lemma}\
994: \rm
995:
996: Let $A~ |~ \Gamma$ be an R-configuration, $A$ be an atomic formula
997: or the negation of an atomic formula. If $\Gamma$ is consistent
998: with $A$, then $A | \Gamma$ is an R-terminated configuration.
999:
1000: \end{lemma}
1001:
1002: \noindent {\bf Proof:} Since $\Gamma$ is finite, $\Gamma$ can be
1003: written as $A_1 \land \cdots \land A_n$. Let $r(\Gamma)$ be the
1004: rank of $\Gamma$ [1]. The proof is given by induction on $r(A_1
1005: \land \cdots \land A_n)$ as below:
1006:
1007: If $r(\Gamma)=1$, $\Gamma$ is an atomic formula. It can not be
1008: eliminated since it is consistent with $A$. By the definition, $A
1009: | \Gamma$ is R-termination.
1010:
1011: Suppose that the lemma holds for $r(\Gamma)<k$. Consider the case
1012: of $r(\Gamma)=k$. Let $\Gamma$ be $B,\Gamma'$, where
1013: $r(\Gamma')<k$, and $\Gamma'$ is consistent with $A$. $B$ can be
1014: one of the following cases:
1015:
1016: \begin{enumerate}
1017:
1018: \item $B$ is an atomic formula. $B$ can not be $\neg A$ since
1019: $\Gamma$ is consistent with $A$. Therefore, $A | \Gamma$ is an
1020: R-termination.
1021:
1022: \item $B$ is $B_1 \lor B_2$. According to the $R-\lor$ rule, $B$
1023: is eliminated if and only if $B_1$ in $A | B_1,\Gamma'$ is to be
1024: eliminated, and $B_2$ in $A | B_2,\Gamma'$ is also to be
1025: eliminated. Since $ B_1,\Gamma'$ with $A$, and $
1026: r(B_1,\Gamma')<k$ holds. According to the inductive hypothesis,
1027: $B_1$ in $A | B_1,\Gamma'$ can not be eliminated. Similarly, $B_2$
1028: in $A | B_2,\Gamma'$ is also not eliminated. Therefore, $A |
1029: \Gamma$ is an R-termination.
1030:
1031: \item Similarly, we can prove the cases that $B$ is $B_1 \land
1032: B_2$ and $B$ is $B_1 \supset B_2$.
1033:
1034: \item $B$ is $\forall x B_1$. According to the $R-\forall$ rule,
1035: $B_1$ is eliminated if and only if $B_1[t/x]$ in $A |
1036: B_1[t/x],\Gamma'$ is to be eliminated. Since $\{
1037: B_1[t/x],\Gamma'\}$ is consistent with $A$, And $
1038: r(B_1[t/x],\Gamma')<k$ holds. According to the inductive premise,
1039: $B_1[t/x]$ in $ B_1[t/x],\Gamma'$ can not be eliminated. Thus, $A
1040: | \Gamma$ is an R-termination.
1041:
1042: \item Similarly, we can prove the case of that $B$ is $\exists x.
1043: B_1$.
1044:
1045: \item Finally, we prove that every one of $A_1,\cdots,A_n$ in
1046: $\Gamma$ can not be eliminated by the R-cut rule. For each $A_k$,
1047: $k=1,\cdots,n$, the R-cut rule is applied only in the circumstance
1048: that there exists $B$, such that $A_1,\cdots,A_{k-1},A_k \vdash
1049: B$, $A_k \mapsto B$, and $B, A_{k+1},\cdots, A_{n} \vdash P$
1050: holds, and $P$ in $A | P$, and $A_{k+1},\cdots, A_{n}$ is to be
1051: eliminated. Since $\Gamma$ is consistent with $A$,
1052: $\{P,A_{k+1},\cdots, A_{n} \}$ is also consistent with $A$,
1053: Furthermore, $P$ is an atomic formula or the negation of an atomic
1054: formula. We know that $r(P, A_{k+1},\cdots, A_{n})\leq k$ holds.
1055: According to the item 1, we know that $A | P, A_{k+1},\cdots,
1056: A_{n}$ is an R-termination. So $P$ can not be eliminated.
1057: Therefore, the R-cut rule can not be applied. \hfill $\Box$
1058: \end{enumerate}
1059:
1060: \begin{theorem}\
1061: \rm
1062:
1063: The R-calculus is reachable.
1064:
1065: \end{theorem}
1066:
1067: \noindent {\bf Proof:} Let $\Delta \mid \Gamma$ be a given
1068: R-configuration, where $\Gamma$ is a finite set of sentences,
1069: and $\Delta$ is an R-condition of $\Gamma$.
1070: Consider the simple case that $\Delta$ contains only
1071: one element $A$. Let $\Gamma'$ be a maximal
1072: contraction of $\Gamma$ by $A$.
1073: For every $B$ in $\Gamma -\Gamma'$, by the lemma 6.1, there exists
1074: a sequence of R-transitions at the end of which $B$ is eliminated.
1075: Since $\Gamma -\Gamma'$ is a finite set of sentences, the above
1076: the sequences can be concatenated to form a sequence of
1077: R-transitions:
1078: \[
1079: A~ |~\Gamma \Longrightarrow^{*} A~|~\Gamma
1080: \]
1081: where $A~ |~\Gamma'$ is an R-termination by the lemma 6.2. \hfill
1082: $\Box$
1083:
1084:
1085:
1086: \begin{definition}
1087: \rm
1088:
1089: R-completeness
1090:
1091: Let $\Delta \mid \Gamma$ be any R-configuration, where
1092: $\Gamma$ is a specification and $\Delta$ is R-condition of $\Gamma$.
1093:
1094: The R-calculus is R-complete, if and only if for a given
1095: R-configuration $\Delta \mid \Gamma$ and every ideal user's
1096: rejection {\bf M}, if ${\bf M} \models \Delta$, then there exists
1097: a transition sequence:
1098: $$
1099: \Delta \mid\Gamma \Longrightarrow^{*} \Delta \mid \Gamma',
1100: $$
1101: where $\Delta \mid \Gamma'$ is a termination and
1102: \[
1103: \Gamma'= \{ A ~~ | M \models A~~ and ~~ A \in \Gamma \}
1104: \]
1105: holds. \hfill $\Box$
1106:
1107: \end{definition}
1108:
1109:
1110: \begin{theorem}\
1111:
1112: \rm
1113:
1114: The R-calculus is R-complete.
1115:
1116: \end{theorem}
1117:
1118: \noindent {\bf Proof:} This theorem is a corollary of the lemma
1119: 3.1 and the theorem of R-reachability. \hfill $\Box$
1120:
1121: \section{Related works}
1122:
1123: In 1985, G\"ardenfors and his colleagues introduced their theory
1124: of changes [4]. The theory addresses the proof-theoretic concepts
1125: of the expansion, the contraction, and the revision in the scope
1126: of propositional logic. The maximal contraction given here can be
1127: viewed a special kind of AGM's contraction, but in the scope of
1128: the first order logic. The user's rejection is a corresponding
1129: model-theoretic concept of the maximal contractions [6,9].
1130:
1131: The AGM's theory focuses on building the systems of the
1132: propositions of the expansion, the contraction and the revision,
1133: and on studying the properties of these systems [4,5]. The
1134: principal difference between the AGM's theory and The R-calculus
1135: is as the following: the aim of designing the R-calculus is to
1136: build a transition system that can deduce all maximal contractions
1137: from a given formal theory $\Gamma$ and its user's rejection $A$.
1138:
1139: Finally, it is believed that using the methods given in [2],
1140: certain proper type theories based on the R-calculus can be
1141: constructed and the corresponding interactive tools can be
1142: implemented to develop the specifications .
1143:
1144: \vspace{5mm}
1145:
1146: \noindent { \bf Acknowledgement:} The author would like to take
1147: this chance to thank Dr. Zhang Yuping. His counter examples helped
1148: the author to find the current version of the definition of the
1149: necessary premise.
1150:
1151: \vspace{5mm}
1152:
1153: \noindent { \bf References}
1154:
1155: \smallskip
1156:
1157: \begin{description}
1158:
1159: \item{[1]} Gallier, J.H., Logic for Computer
1160: Science, foundations of automatic theorem proving.
1161: John Wiley \& Sons, 1987, 147-158, 162-163, 197-217.
1162:
1163: \item{[2]} Paulson, L., Logic and Computations,
1164: Cambridge University Press, 1987, 38-50.
1165:
1166: \item{[3]} Flew, A., A Dictionary of Philosophy,
1167: Pan Books Ltd, 1979.
1168:
1169: \item{[4]} Alchourr\'on, C.E., G\"ardenfors, R. and Makinson, D.,
1170: On the logic of theory change: partial meet contraction and revision
1171: functions, The Journal of Symbolic
1172: Logic, Vol.50, No.2, June, 1985.
1173:
1174: \item{[5]} G\"ardenfors, P., Knowledge in Flux,
1175: The MIT Press, 1988.
1176:
1177: \item{[6]} Li, W., An Open Logic System, Science in China, Series A, March, 1993.
1178:
1179: \item{[7]} Shoenfield, J.R., Mathematical Logic, Addison-Wesley,
1180: Reading, Mass, 1967, 74-75.
1181:
1182: \item{[8]} Forcing, Burgess, Handbook of mathematical logic,
1183: edited by J., Barwise, North-Holland Publishing Company, 1977.
1184:
1185:
1186: \item{[9]} Li W., A Logical Framework for the evolution of
1187: Specifications. ESOP'94, LNCS 788, 1994, Springer-Verlag.
1188:
1189: \item{[10]} Burstall, R. and Goguen J.A., Putting
1190: theories together to make specifications, Proc. 5th. IJCAI
1191: Cambridge, Mass, 1045-1058 (1977).
1192:
1193:
1194: \item{[11]} Bj{\o}rner, D., and Jones, C., Formal
1195: specification and Software Development, Prentice Hall
1196: International, 1983.
1197:
1198: \item{[12]} Nordstr\"{o}m, B., and Smith, J.,
1199: Propositions and specifications of programs in
1200: Martin-L\"{o}f's type theory, BIT 24 (1984),
1201: pp 288-301.
1202:
1203: \item{[13]} D. Sannella and A. Tarlecki,
1204: Toward formal development of programs from algebraic
1205: specifications: implementations revisited.
1206: Acta Informatica 25,233-281(1988).
1207:
1208: \end{description}
1209:
1210: \end{document}
1211: