In the paper new logics oriented on hierarchical data are developed. Algebras of partial predicates over such data with special compositions as operations form a semantic base for constructed logics. Characteristic property of such logics is the usage of composite names in their languages. Semantic properties of these logics are studied; corresponding sequent calculi are defined, their soundness and completeness are proved for logics of renominative level.
Research,
MathematicalModel,
FormalMethods, Mathematical logic is widely used in formal program development, analysis, and verification. Still, some discrepancies can be admitted between traditional logic and problems to be solved. For example: semantics of programs is presented by partial functions, whereas in traditional logic total functions and predicates are usually considered; programming languages have a developed system of data types, whereas traditional logic prefers to operate with simple unstructured types (sorts); semantic aspects of programs prevail over syntactical aspects, whereas in traditional logic we have the inverse situation.
Discrepancies mentioned above complicate the usage of logic for program development and verification. In this paper we propose to take program models as an initial point and construct logics semantically based on such models.
To realize this idea we should first construct adequate models of programs. To
tackle this problem we use composition-nominative approach to program
formalization [
The intensional aspects in this integrity play a leading role. Principle of priority of semantics over syntax: program semantic and syntactical aspects should be first studied separately, then in their integrity in which semantic aspects prevail over syntactical ones. Compositionality principle: programs can be constructed from simpler programs (functions) with the help of special operations, called compositions, which form a kernel of program semantics structures. Nominativity principle: nominative (naming) relations are basic ones in constructing data and programs.
Here we have presented only principles relevant to the topic of the article; richer
system of principles is developed in [
Functional algebra is the main semantic notion in program formalization. Terms of this algebra define syntax of programs (descriptive system), and ordinary procedure of term interpretation gives a denotation system.
CNS can be used to construct formal models of various programming,
specification, and database languages [
CNS are classified in accordance with levels of abstraction of their parameters: data, functions, and compositions. In this article levels of program models are induced by abstraction levels of data.
Data are considered at three levels: abstract, Boolean, and nominative. At the abstract level data are treated as "black boxes", thus no information can be extracted. At the Boolean level to abstract data new data considered as "white boxes" are added. Usually, these are logical values T (true) and F (false) from the set Bool. At the nominative level data are considered as "grey boxes", constructed of "black" and "white boxes" with the help of naming relations. The last level is the most interesting for programming. Data of this level are called nominative data. The class of nominative data over a set of names V and class of basic values W can be defined inductively or as the least fixed point of the recursive definition ND(V ,W ) W (V m ND(V ,W )) , where
partial multi-valued (non-deterministic) functions.
To present nominative data we use the form d = [vI ai | iI]. Nominative membership relation is denoted by . Thus, vi ai d means that the value of vi in d is defined and is equal to ai.
The class ND(V,W) \ W is called the class of proper nominative data, or hierarchical nominative data; data from the class V mW will be called flat nominative data.
Concretizations of nominative data can represent various data structures, such as
records, arrays, lists, relations, etc. [
The levels of data abstraction formulated above may be treated as data
intensionals. They respectively specify three levels of semantics-based program
models: abstract, Boolean, nominative. The models of each level constitute
extensionals of that level intensional. Program models of abstract level are very poor
(actually, only sequencing compositions can be defined). Program models of Boolean
level are richer and permit to define structured programming constructs (sequence,
selection, and repetition). This level is still too abstract and does not explicitly specify
data variables. At last, models of nominative level permit to formalise compositions
of traditional programming. This level (its intensional) involves variables of different
types. Consider, for example, a simple educational programming language WHILE
[
Example 1. Consider a Boolean expression x<y. Its semantics is formalized as a partial quasiary predicate less : VZBool. This predicate is undefined on flat nominative data [x5, u4] (we write less([x5, u4])), is defined on [x5, u4, y2] with value F (we write less([x5, u4, y2])= F). Note that if a value of less is defined on some data, then the predicate is defined with the same value on any extension of this data. Thus, less([x5, u4, y2, v4])=F, x, u, y, vV. This property is called equitonicity (a special case of monotonicity). A specific new composition is renomination Rxv11,,......,,vxnn , e.g. (R xy,,vy (less))([x5, u4, y2, v4]) = less([x2, u4, y4, v4]) = T.
More elaborated programming languages work with hierarchical nominative data.
In such languages composite names like x1.x2. … .xn are used to access data
components. The details can be found in [
Having described program models of various abstraction levels, we can now start
developing semantics-based logics which correspond to such models. Such logics will
be called composition-nominative logics (CNL). Analysis of constructed program
models shows that the main semantic notion of mathematical logic – the notion of
predicate – can be defined at the Boolean level. At this level predicates are considered
as partial functions from a class of abstract data A (with abstract intensional) to Bool.
In this case such compositions as disjunction , negation , etc, can be defined. These
compositions are derived from Kleene’s strong connectives [
Three kinds of logics can be constructed from program models at the flat nominative data level: logics, which use only partial quasiary predicates (pure predicate logic); logics, which use additionally partial quasiary functions (predicate-function logics); logics, which use also bi-quasiary functions (program logics).
The first type of logics will generalize classical pure predicate logics, the second type – classical predicate logic (with functions and equality), and the third type can present various logics, which use program constructs.
Here we give a short characteristic only to composition-nominative pure predicate
logics; predicate-function logics are described in [
From semantic point of view the main distinction of CNL from classical first-order logics is usage of partial quasiary predicates instead of total n-are predicates; this leads to algebras of quasiary predicates with compositions as operations. From syntactical point of view formulas of CNL are simply terms of algebras of quasiary predicates.
The main compositions that can be additionally specified at the nominative level are renomination (denoted also R vx ) and quantification x. These
Rxv11,,......,,vxnn compositions use subject names as parameters. CNL of renominative level are based on algebras of the type <VABool; , , R vx >, CNL of quantifier level – <VABool; , , R vx , x>. Properties of these algebras determine calculi for corresponding logics.
Note, that renomination (primarily in syntactical aspects) is widely used in classical logic, lambda-calculus, and specification languages like Z-notation [10], B [11], TLA [12], etc. Here we will give explicit semantic definition of this operation (cf. with [13]).
To preserve properties of classical first-order logic we should restrict the class
VABool of quasiary predicates. Namely, we introduce a class of equitone predicates
and its different variations such as maxitotal equitone, local-equitone, equicompatible,
and local-equicompatible classes [
The current article continues investigations of pure predicate logics over hierarchical nominative data initiated in [14]. Here we prove soundness (correctness) and completeness of the constructed logics. The distinctive feature of such logics is the usage of composite names of the form x1.x2. … .xn as parameters of renomination and quantification compositions.
The article is structured as follows: the first section is introduction, in the second section operations over hierarchical data are introduced and their properties are studied, the third section is devoted to compositions over predicates. In the fourth section semantic models and corresponding languages of logics are described, and the fifth section is devoted to definition of sequent calculi for some of the described logics.
Notions not defined here we interpret in sense of [
Class of hierarchical nominative data ND(V, A) over classes of basic names V and basic values A is defined inductively: 1) ND0(V, A) = A – nominative data of rank 0; 2) NDk+1(V, A) = A (V n NDk (V , A)) – nominative data of rank less or equal to k+1.
Then ND(V, A) = (V n NDk (V , A)) .
k 0
Here V n NDk (V , A) is the set of all finite single-valued mappings from V to NDk(V, A). Note, that we restrict nominative data to be single-valued mappings. This guaranties unambiguity of naming for data components. An empty nominative data has rank 0.
The set of hierarchical nominative data is defined as follows: HD(V, A) = ND(V, A) \ A.
The value of name u in data d is equal to d(u), but we also write u:d in style of denaming operation. For a composite name u = y1.y2. … .yn notation u:d means yn:(…(y2:(y1:d))…). We drop a component xu:, if u: is undefined.
Hierarchical data can be represented also as oriented trees with edges labeled by basic names and leafs labeled by basic values.
Any hierarchical data d can be represented as a flat nominative data with composite names – elements of the set V+. These composite names are non-empty words in the alphabet V formed by concatenation “.” of basic names along the path from the root to leafs in the tree representing d.
Example 2. Let [x [ y 1, z 2], y [ x 3, y [ x 0, y 0, z 1]], z 2, u [ x [ x 0, u 1], z 3]] be hierarchical data. Its flat representation is [x.y 1, x.z 2, y.x 3, y.y.x 0, y.y.y 0, y.y.z 1, z 2, u.x.x 0, u.x.u 1, u.z 3].
Such representations are called flat normal forms (FNF) of hierarchical data. Due to the unambiguity of naming all (composite) names of FNF must be different; moreover, they should be incomparable. Now it is possible to write [x.y , x.u,…] in place of [x [y , u,…]].
Let us formulate some definitions and properties of hierarchical data used in further proofs. From now on, names are considered as composite names from V+ unless explicitly stated that they belong to V.
A prefix of a word uV+ is any word x such that u = x.y for some yV*. If u x, we call x a strict prefix. We write x u (x u), if x is a prefix (strict prefix) of u. Words x and u are comparable (xu), if x u or u x; otherwise they are incomparable (x u). Sets of names X and Y are incomparable (X Y), if x y for all xX and yY.
We call a composite name as a full name of d, if it coincides with some path from a root in the tree determined by d. If this path reaches a leaf, then the name is called terminal. We define the set of full names by fn(d) = {u | u:d}; the set of terminal names by tn(d) = {u | u:dA}.
Hierarchical data d1 and d2 are disjoint, if x y for any xtn(d1) and ytn(d2). The union of disjoint data we denote by “+”.
Parametric operation of deletion of data components, the names of which are comparable with given names x1,..., хn, is defined via FNF as follows: || x1,...,xn (d ) = [ ua d | u is terminal and x1 u,..., хn u].
Example 3. Let d be a hierarchical data from example 2. Then: d ||–х, u = [y.x 3, y.y.x 0, y.y.y 0, y.y.z 1, z 2]; d ||–х.z, y.y, z.y, u.x,u = [x.y 1, y.x 3, u.x.x 0, u.z 3].
When using the symbol “+” we drop brackets “[” and “]”, e.g. instead of d ||–u + [uu:d ||–v] we write d ||–u + uu:d ||–v .
Proposition 1. 1) d || z,u,x1,...,xn d ||z,x1,...,xn , if z u; 4) (d1 + d2)||–u = d1||–u + d2||–u ; 2) d = d ||– x + x x:d, if xV ; 3) (d ||–х)||–х.y = (d ||–х.y)||–х = d ||–х ; 5) d ||–u.v = d ||–u + u u:d ||–v ; 6) d d ||–u + u u:d.
For a composite u the property d = d ||–u + u u:d may fail.
Example 4. Let d = [ u 0, z.x 0, z.y 1]. Then d ||–u.v = [ z.x 0, z.y 1], and d ||–u.v + u.vu.v:d = d ||–u.v d, because u:d is a basic value and u.v:d is undefined. Proposition 2. Let u {х1,..., хn}, then d ||u,x1,...,xn (d ||u ) ||x1,...,xn . In particular, if z u, then d ||–u, z = (d ||–u)||–z = (d ||–z)||–u .
In the general case we have that d ||u1,...,um ,x1,...,xn (d ||u1,...,um ) || x1,...,xn if {u1,..., um} {х1,..., хn}.
Proposition 3. 1) x : (d || z1,...,zn x h) h ; in particular, x : (x h) h ; 2) x : (d || z1,...,zn ) x : d , if x {z1,..., zn}; 3) x : (d || x,z1,...,zn ) .
Using the propositions 1–3, it is possible to represent d ||x1,...,xn , where x1,..., xnV+, with an expression in some standard form, which uses only operations of deletion ||v1,...,vm with simple names v1,..., vmV, union +, naming y1.y2. … .yk and denaming u1:u2:... ul: (here y1,..., yk, u1,..., ulV). Details are omitted here.
Example 5. d ||–z.x, z.y, u.x.y = d ||–z, u + zz:d ||–x, y + uu:d ||–x + u.xx:u:d ||–y . Operation of renomination rxv11,,......,,xvnn : HD(V, A) HD(V, A) we define as follows: rxv11,,......,,xvnn (d ) d ||v1,...,vn v1 x1 : d ... vn xn : d .
Here all names v1,..., vn should be pairwise incomparable. We see that the result of renomination can be presented uniquely in the standard form.
Example 6. ruv..yx,,yv..xy,,vu..xx.y (d ) d ||–v, u + vv:d ||–x, y + uu:d ||–x + + u.xx:u:d ||–y + v.xy:u:d + v.yx:y:d + u.x.yx:v:d.
Note, that renomination is monotone: if d h, then rxv11,,......,,xvnn (d ) rxv11,,......,,xvnn (h) . To present convolution of renominations we use the standard form.
Example 7. ruz (rxu.v (d )) ruz (d ||u.v u.v x : d ) ruz (d ||u u u : d ||v u.v x : d ) d ||u,z u.v x : d z u : d ||v z.v x : d .
Thus, situation for hierarchical data is more difficult than for flat data for which
convolution of renominations can be presented as one new renomination [
Example 8. rzx..yv (rux,.vx,.zy (d )) rzx..yv (d ||u.z u u : d ||v u.v x : d z y : x : d ) d ||u.z, x u u : d ||v u.v x : d z y : x : d x x : d ||v x.v y : y : x : d. 3
Compositions of Predicates over Hierarchical Data From semantic point of view the notion of predicate is one of the basic concepts of logic.
By a predicate P on D we understand a single-valued partial function of the type D Bool. The truth and falsity domains of P are respectively T(P) = {dD | P(d) = T} and F(P) = {dD | P(d) = F}. A predicate P is irrefutable, or partially true, if F(P) = .
Compositions determine universal methods of predicate construction; they form the kernel of logic of corresponding type.
At the propositional level data are treated as abstract, therefore predicates are interpreted as functions from A to Bool, where A is an abstract class. Basic propositional compositions are disjunction and negation ( P, QA Bool, d A ): T , if P(d ) T or Q(d ) T , (P Q)(d ) F , if P(d ) F and Q(d ) F , undefined in other cases.
At the nominative level data are constructed from a set of subject names and a class of subject values. In this work logics of partial predicates over hierarchical nominative data at renominative and quantifier level are investigated.
A function of the form Р : HD(V, A) Bool is called a hierary predicate on HD(V, A). We denote the class of hierary predicates on HD(V, A) by PrHV_А.
The name xV is strictly unessential for a hierary predicate P on HD(V, A), if for arbitrary d, HD(V, A) we have P(d ||–x + x) = P(d ||–х). The notion of unessential name is an analogue of fresh name in classical and nominal logics [15].
A predicate P : HD(V, A) Bool is called equitone, if for arbitrary d, d'HD(V, A) conditions d d' and P(d) imply P(d') = P(d).
At the renominative level to propositional compositions we add renomination composition Rv1,...,vn defined by the formula
x1,...,xn Rxv11,,......,,xvnn (Q)(d ) Q(rxv11,,......,,xvnn (d )) Q(d ||v1,...,vn v1 x1 : d ... vn xn : d ) . Using vector notation, we can formulate the following properties of renomination: R) Rxv (P Q) Rxv (P) Rxv (Q) ; R) Rxv (P) Rxv (P) .
The properties of R, R&, R can be written down analogously.
RR) Rxv (Ryu (P)(d ) P(ryu (rxv (d ))) for each dHD(V, A).
In the case of equitone predicates for composite names we have:
Contrary to traditional case quantified names can be composite; quantification is possible both over all hierarchical or only over basic data. In this work we consider quantification over hierarchical data. Composition of existential quantification is defined in the following way:
T , if there exists ND(V , A) : P(d ||x x ) T , xP(d ) F , if P(d ||x x ) F for all ND(V , A),
undefined in all other cases.
Composition of universal quantification is defined by formula хР=хР.
Theorem 1. The class of equitone predicates over hierarchical data is closed under compositions , , Rxv , x, х.
Main properties of compositions x and x are the following. 1. If x and y are incomparable then xуР = ухР and xуР = ухР. 2. Absorption of external quantifier by internal with the same name:
xхР = хР; xхР = хР; xхР = хР; xхР = хР. 3. Absorption of external quantifier by internal with more general name: x.ухР = хР; x.ухР = хР; x.ухР = хР; x.ухР = хР.
At the same time xх.уР, xх.уР, хР, х.уР are all different;
xх.уР, xх.уР, хР, х.уР are all different. 4. Absorption of the quantified name by more general upper name of renomination: x.y(Rzx,,vu P) Rzx,,vu (P), if x.y {z, u , v}. 5. Absorption of the upper name of renomination by more general quantifier:
Rzy,,vu (xP) Rvu (xP), if x is a prefix of names from y and x {u}.
At the same time x.y(Rzx P) Rzx (x.yP) and x.y(Rxx.y.v P) Rx.y.v (P); x Rux.y (xP) x(Rux.y (P)), Rux.y (xP) Rux.y (P), x(Rxz.u P) Rxz.u (xP). 6. z(Rvu P) Rvu (zP), if z {u , v}.
Properties 4–6 can be rephrased for universal quantification.
Let us note that some properties valid in classical logic fail for the class of equitone predicates over hierarchical data.
Example 9. Let predicate х be defined by the following formula:
T , if d (x) A, x (d ) F , if d (x) A,
undefined in all other cases.
It is clear that х is equitone. By definitions of compositions x and хР we have that x.v х(d) = x.v х(d) = F for each dHD(V, A) such that xad, where aA. At the same time х(d) = T for such d. So, (х x.v х)(d) = F. 4 Semantic Models and Languages of Logics over Hierarchical Data Semantic models of composition-nominative logics over hierarchical nominative data (CNLH) are predicate algebras with class PrHV_А of hierary predicates as carriers and class C of compositions as operations of algebras. The class C is determined by a level intensional; for a quantifier level C consists of compositions , , Rxv , and x; v for renominative level these are , , and Rx . Thus, algebras of the form AHD(V, A) = <PrHV_А; , , Rv , x > are semantic base of constructed logics. With a fixed x sets V and C such algebras are determined by the set A.
Alphabet of a language of quantifier level includes symbols of basic compositions, a set Ps of predicate symbols, and a set of basic subject names (variables) V.
The set Fr of formulas for a quantifier level is defined inductively: 1) every predicate symbol from Ps is an (atomic) formula; 2) if and are formulas, then and are formulas; 3) if is a formula, then Rxv is a formula; 4) if is a formula, then x is a formula.
For CNLH of renominative level we drop item 4 in this definition.
Let nm() be the set of all names, which appear in the symbols of renomination and quantification in .
To distinguish symbols of compositions from their interpretations we use for the latter bold font (only in the following definitions). Let I : Ps PrHV_А be a total single-valued interpretation mapping, then a pair (AHD(V, A), I) is called a model of CNLH language. To simplify notation we will denote models as (A, I) Interpretation J : FrPrHV_А we define as follows: 1) J(р) = I(p) for each рPs; 2) J() = J()J(), J() = (J()); 3) J (Rxv ) = R vx (J()); 4) J(x) = x(J()).
For renominative level we drop item 4.
Predicate J(), which is the value of a formula interpreted on A = (A, I), we denote by A. A formula is partially true on A = (A, I) (denoted by A |= ), if A is partially true (irrefutable) predicate. is everywhere (partially) true, or irrefutable (denoted by |= ), if is partially true on every model of a language.
A formula is a logical consequence of a formula ( |= ), if formula is irrefutable. is a weak logical consequence of ( ||= ), if for each A = (A, I) the condition A |= implies A |= .
Formulas and are logically equivalent ( ), if |= and |= . Formulas and are logically strictly equivalent ( TF ), if T(A) = T(A) and F(A) = F(A) for each AS A. The relation of logical consequence can be extended to arbitrary sets , Fr. is a logical consequence of in the model A ( A|= ) if for all dHD(V, A) the condition A(d) = T for all implies that it is impossible that A(d) = F for all . is a logical consequence of ( |= ), if А|= for all model A = (А, I). Relation |= is reflective but not transitive.
For CNLH the following statements hold.
Theorem 2 (semantic equivalence). Suppose that ' is obtained from by substitution of some occurrences of 1,..., n with 1,..., n respectively. If 1 1, ... , n n, then '.
Theorem 3 (semantic equivalence, strong form). Suppose that ' is obtained from by substitution of some occurrences of 1,..., n with 1,..., n respectively. If 1 TF 1 ,..., n TF n, then TF '.
Theorem 4 (substitution of equivalents). Suppose that . Then , |= , |= and |= , |= , .
A name xV is strictly unessential for (xsun()), if x is strictly unessential for a predicate A for every A = (A, I).
Proposition 4. Let уsun(). Then x TF yRyx .
For each рPs the set of strictly unessential subject names is fixed by a total function : Ps2V. For CNLH we postulate infinity of the set VT = ( p) of pPs totally strictly unessential names.
The following properties of formulas are representations of corresponding semantic properties of predicate algebras.
RsN) Rzy,,xv () TF Rxv () , if ysun().
RT) Rzz,,xv () TF Rxv () , if zV; in particular, Rzz () TF .
R) Rxv ( ) TF Rxv () Rxv () .
R) Rxv () TF Rxv () .
Generalizing R and R, we get RR and RR.
RR) Rxu (...Rzw ( )...) TF Rxu (...Rzw ()...) Rxu (...Rzw ()...) .
RR) Rxu (Ryv (...Rzw ()...)) TF Rxu (Ryv (...Rzw ()...)) .
Similarly, we can write down the properties R&, R, R, RR&, RR, RR. RR_C) Rxv (Ryu ( A )(d ) A (ryu (rxv (d ))) for each A = (A, I), dHD(V, A). ANQ) x.y(Rzx,,vu ) TF Rzx,,vu () and x.y(Rzx,,vu ) TF Rzx,,vu (), if x.y {z, u , v}.
ANR) Rzy,,vu (x) TF Rvu (x) and Rzy,,vu (x) TF Rvu (x), if x is a prefix of all names in y and x {u}.
R) Rxv (y) TF y(Rvu ) , if y {u , v}.
R) Rxv (y) TF zRxv (Rzy ()) if zVT and znm(R vx (y)).
Similarly, we can formulate R and R. Properties R, R, R, R can be generalized to RR, RR, RR, RR; R and R to RR and RR.
For equitone predicates RT can be changed to RTE: RTE) Ruu,,xv () Rxv () ; in particular Ruu () .
For logics of equitone predicates we introduce the notion of primitive formula. A formula Rxu (Ryv (...Rzw ( p)...)) is primitive, if pPs and in renominations identical pairs of names are removed.
With every primitive Rxu (Ryv (...Rzw ( p)...)) we connect an expression of the form р(), where represents a convolution of renominations rxu (ryv (...rzw ()...)) given in the standard form, VPs is a special symbol, which denotes arbitrary data. To take into account strictly unessential subject names, we delete all components that have z(р) as a prefix. An expression р() is called a renominant of the above primitive formula. The set of longest incomparable names occurred in a renominant is called its naming scheme.
Example 10. To construct the renominant of a primitive formula Rxu.v (Ruz (q)) we specify corresponding standard form of renomination convolution (see Example 7) obtaining renominant q( d ||u,z u.v x : d z u : d ||v z.v x : d ). Its naming scheme is {u.v, x, z.v}.
Now we point out basic properties of quantification compositions for CNLH. Q1. xy TF yx and xy TF yx, if x and у are incomparable. Q2. x TF x and x TF x.
Q3. x TF xx, x TF xx; x TF xx, x TF xx. Q4. x TF x.уx, x TF x.уx; x TF x.уx, x TF x.уx. Q5. xx TF x() and x&x TF x(&).
Q6. x(&)|= x&x and xx|= x().
Q7. yx |= xy; and not always xy|= yx.
Q8. ||= x and ||= x.
Q9. |= x (x) and |= x (x); |= x (x) and |= x (x).
Properties Q2, Q3, Q5–Q9 are analogous to the corresponding properties of logics of quasiary predicates.
At the propositional level the properties of |= for sets of formulas are identical to
corresponding properties of logic of quasiary predicates [
Now we formulate basic properties of renomination compositions.
RTE|–) Ruu,,xv (), А|= Rxv (), А|= .
RTE–|) А|= , Ruu,,xv () А|= , Rxv () . .
RsN|–) Rzy,,xv (), А|= Rxv (), А|= , where уV is strictly unessential for . RsN–|) А|= , Rzy,,xv () А|= , Rxv () , where уV is strictly unessential for RR|–) Rxu (...Rzw ( )...), А|= Rxu (...Rzw ()...) Rxu (...Rzw ()...), А|= . RR–|) , Rxu (...Rzw ( )...) А|= , Rxu (...Rzw ()...) Rxu (...Rzw ()...) А|= . RR|–) Rxu (Ryv (...Rzw ()...)), А|= Rxu (Ryv (...Rzw ()...)), А|= . RR–|) , Rxu (Ryv (...Rzw ()...)) А|= , Rxu (Ryv (...Rzw ()...)) А|= . Properties RR|– , RR–| , RR&|– , RR&–| are analogous.
R|–) Rxv (y), А|= yRxv (), А|= if y {u,v}.
R–|) А|= , Rxv (y) А|= , yRxv () if y {u,v}.
R|–) Rxv (y), А|= zRxv (Rzy ()), А|= .
R–|) А|= , Rxv (y) А|= , zRxv (Rzy ()) .
For R|– and R–| z is totally strictly unessential and znm(R vx (y)).
Properties R|– , R–| , R|– , R–| are analogous. Properties of type R, R, R, R can be generalized to properties of type RR, RR, RR, RR. 5 The Sequent Calculus of Logics of Predicates over Hierarchical Data For logics of equitone hierary predicates we will build a calculus of sequent type. We will consider here only logics of renominative level. Sequents are interpreted as sets of labeled formulas marked by one of two symbols – |– or –|. Such sequents are also denoted by |––|, where all formulas of are labeled by the symbol |– , of – by the symbol –| .
Sequent is closed, if there exists such that |– and –| or if there exist primitive and with identical renominants such that |– and –|. Consequently, if |––| is closed then |= .
Derivation in the sequent calculus has the form of tree, the vertices of which are
sequents. Such trees [
Semantic properties of relation |= have their syntactic analogues – sequent forms (rules). For renominative logics of equitone hierary predicates these forms are the following. | | A, | A B,
| B, | |–RTE |–RR | A, | A, | Rxv ( A), | Ruu,,xv ( A), | | A, |B,
| A B, | | A,
| A, –|RTE –|RR | Rxv ( A), | Ruu,,xv ( A), | Rxu (...Rzw ( A)...) Rxu (...Rzw (B)...),
| Rxu (...Rzw ( A B)...)), |–RR | Rxu (...Rzw ( A)...), | Rxu (...Rzw (A)...), | Rxu (...Rzw ( A)...) Rxu (...Rzw (B)...),
| Rxu (...Rzw ( A B)...), –|RR | Rxu (...Rzw ( A)...), | Rxu (...Rzw (A)...),
Sequent calculus with basic sequent forms shown above we will call RID-calculus. For RID-calculus theorems of soundness and completeness hold.
Theorem 5 (soundness). Let sequent |––| be derivable. Then |= . The proof can be conducted by induction over shape of a sequent tree for |––|.
For proving completeness we will use Hintikka's method of model sets. The set Н of labeled formulas with W = nm(Н) is a model set, if:
HC) For every non-primitive formula it is impossible that |–H and –|H.
HCR) For primitive formulas and with identical renominants it is impossible that |– , –|H and it is impossible that |–, –|H. H) If |–H, then |–H or |–H; if –|H, then –|H and –|H. H) If |–H, then –|H; if –|H, then |–H.
HRT) If |– Ruu,,xv () H, then |– Rxv () H; if –| Ruu,,xv () H, then –| Rxv () H. HR) If |– Rxu (...Rzw ( )...) H, then |– Rxu (...Rzw ()...) Rxu (...Rzw ()...) H; if –| Rxu (...Rzw ( )...) H, then
–| Rxu (...Rzw ()...) Rxu (...Rzw ()...) H.
HR) If |– Rxu (...Rzw ()...) H, then |– Rxu (...Rzw ()...) H;
if –| Rxu (...Rzw ()...) H, then –| Rxu (...Rzw ()...) H.
Procedure of construction of a tree for is split into stages. Every application of sequent form is performed only for the finite set of accessible formulas. At the beginning of every stage we perform the step of access: to the list of accessible formulas one formula from each of lists of |–-formulas and –|-formulas is added. We start the construction with a pair of first formulas from the lists.
Suppose that k stages of procedure have already been performed. On the stage k+1 we check whether all terminal nodes are closed. If yes, the procedure is completed positively, and we have got a closed sequent tree. If no, for every unclosed leaf we undertake a next step of access, whereupon we finish building of finite subtree with a vertex as follows.
We activate all accessible non-primitive formula . Then to every active formula we apply the proper sequent form. We remove all repetitions of formulas in a sequent.
During the construction of sequent tree the following cases are possible: 1. Procedure is completed positively; we have the finite closed tree.
2. Procedure is completed negatively, or is not completed; we have a finite or infinite unclosed tree. Such tree has at least one path all vertices of which are unclosed sequents. Such path is unclosed. Every formula of will be in and will become accessible.
Theorem 6. Let be an unclosed path in sequent tree. Then there exists AS A = (A, I) and HD(V, A): |–Н A() = T and –|Н A() = F.
The set Н of labeled formulas of sequents of the path is a model set.
Let W be a combination of naming schemes of the set of renominants of primitive formulas of sequents of the path . Such W includes longest incomparable names, which are involved in renominations of formulas of sequents of the path .
We duplicate elements of W obtaining A = {u | uW}; then put = [uu | uW].
We specify the values of basic predicates on and on data of the form rxu (...rzw ()...) in the following way: if |–рН, then set рA() = T; if –|рН, then set рA() = F; if |– Rxu (...Rzw ( p)...) Н, then set pA (rxu (...rzw ()...)) = T; if –| Rxu (Ryv (...Rzw ( p)...) Н, then set pA (rxu (...rzw ()...)) = F.
In all other cases for dHD(V, A) the value of рA(d) can be set arbitrarily, taking into account equitonicity and strict inessentiality of names.
Theorem holds for atomic and primitive formulas due to above definitions of basic predicates. Then the proof is carried out by induction over the complexity of a formula in accordance with construction of a model set.
Theorem 7 (completeness). Let |= . Then a sequent |––| is derivable.
Suppose contrary: |= and a sequent |––| is not derivable. Then sequent tree for = |––| is not closed. Consequently, in there is unclosed path . The set H of all labeled formulas of sequents of this path is a model set. According to the theorem 5 there exists AS А = (А, І) and HD(V, A) such that |–H A()= T and –|H A()= F. Due to H we have |– А() = T and –| А() = F. But it contradicts |= . 6
In the paper new logics oriented on hierarchical data are developed. Algebras of partial predicates over such data with special compositions as operations form a semantic base for constructed logics. These logics may also be treated as generalization of classical logic. First of all, this generalization concerns types of predicates: while classical logic is semantically based on total n-ary predicates, we have constructed logics based on partial quasiary and hierary predicates, defined on special types of hierarchical nominative data. Importance of such data is explained by their representational power, which permits to model data structures of specification and programming languages. Characteristic feature of such languages is usage of composite names to access data components. The constructed logics also use composite names. Semantic properties of such logics have been studied; corresponding sequent calculi have been defined, their soundness and completeness have been proved for logics of renominative level. Authors plan to present more developed logics at hierarchical nominative level in forthcoming papers.