We investigate algorithms for solving the satisfiability problem in composition-nominative logics of quantifier-equational level. These logics are algebra-based logics of partial predicates constructed in a semantic-syntactic style on the methodological basis, which is common with programming; they can be considered as generalizations of traditional logics on classes of partial predicates that do not have fixed arity. We show the reduction of the problem in hand to the satisfiability problem for classical first-order predicate logic with equality. The proposed reduction requires extension of logic language and logic models with an infinite number of unessential variables. The method developed in the paper enables us to use existent satisfiability checking procedures also for quantifier composition-nominative logic with equality.
Research,
MathematicalModel,
FormalMethods,
Last years the interest to the satisfiability problem [
These principles specify a hierarchy of new logics that are semantically based on
algebras of predicates. Predicates are considered as partial mappings from a certain
class of data D into the class of Boolean values Bool. Operations over predicates are
called compositions. They are treated as predicate construction tools. Data classes are
considered on various abstraction levels, but the main attention is paid to the class of
nominative data. Such data consist of pairs name–value. Nominative data can
represent various data structures such as records, arrays, lists, relations, etc. [
CNL can be considered as generalization of classical predicate logic but for all that many methods developed within classical logic can also be applied to CNL. Here we confirm this statement for the satisfiability problem in CNL. In this paper we consider composition-nominative logic of quantifier-equational level and construct an algorithm that reduces the satisfiability problem in this logic to the same problem in classical first-order predicate logic with equality. The reduction proposed requires the logic language to be extended with an infinite number of unessential variables.
The paper is structured in the following way. In section 2 we give an overview of the composition-nominative logics classification; then in section 3 we give formal definitions of the logics that we consider in this paper, and define the satisfiability problem. In section 4 we describe the reduction method for solving the satisfiability problem. In section 5 we discuss related work. In section 6 we summarize our results and formulate directions for future investigations.
Proofs are omitted here and will be provided in an extended version of the paper.
Notions and notations not defined in the paper are understood in the sense of [
Classification of composition-nominative logics is based on classification of their
parameters: data, predicates, and compositions. The main semantic notion of
mathematical logic – the notion of predicate – can be defined as a partial function from a
data class D to Bool. For the most abstract level of data consideration such
compositions as disjunction ∨, negation ¬, etc., can be defined. These compositions are
derived from Kleene’s strong connectives [
The obtained logics may be 3. called propositional logics of partial predicates. Such logics are rather abstract, therefore their further development is required at the nominative level. At this level we have two sublevels determined respectively by flat and hierarchic nominative data.
Three kinds of logics can be constructed from program models on the flat nominative data level: 1. pure quasiary predicate logics based on algebras with one sort: PrV,А; 2. quasiary predicate-function logics based on algebras with two sorts: Pr V,А and FnV,А; quasiary program logics based on algebras with three sorts: PrV,А, FnV,А, and PrgV,А.
For logics of pure quasiary predicates we identify renominative, quantifier, and quantifier-equational levels.
Renominative logics [
At the quantifier level, all basic (object) values can be used to construct different nominative sets to which quasiary predicates can be applied. This allows one to introduce the compositions of quantification ∃x in style of Kleene’s strong quantifiers. The basic compositions of logics of the quantifier level are ∨, ¬, R vx , and ∃x.
At the quantifier-equational level, new possibilities arise for equating and differentiating values using special 0-ary compositions, i.e., parametric equality predicates =xy . Basic compositions of logics of the quantifier-equational level are ∨, ¬, R vx , ∃x, and =ху .
All specified logics (renominative, quantifier, and quantifier-equational) are based on algebras which have only one sort: a class of quasiary predicates.
For quasiary predicate-function logics we identify function level and functionequational levels.
At the function level, we have extended capabilities of formation of new arguments
for functions and predicates. In this case it is possible to introduce the superposition
composition S x (see [
At the function-equational level a special equality composition = can be introduced
additionally [
This means that two-sorted algebras (with sets of predicates and functions as sorts and above-mentioned compositions as operations) form a semantic base for first-order CNL.
The level of program logics is quite rich. First, program compositions should be defined that describe the structure of programs. In the simplest case these are: t 1. assignment composition ASx: FnV,А → PrgV,А, t 2. composition of sequential execution •: PrgV,А×PrgV,А → PrgV,А, t 3. conditional composition IF: PrV,А×PrgV,А×PrgV,А → PrgV,А, t 4. cycling composition WH: PrV,А×PrgV,А → PrgV,А.
Then we should define compositions specifying program properties. Here we only mention a composition which formalizes the notion of assertion in Floyd-Hoare logic. From a semantic point of view an assertion scheme of the form {P}prog{Q} may be considered as composition FH, which given two quasiary predicates P (precondition), Q (postcondition), and a bi-quasiary function (a program) prog produces new quasiary predicate denoted by FH(P, prog, Q). At this level we obtained a three-sorted predicate-function-program algebra. Classes of terms of this algebra may be considered as sets of formulas (or their components) of corresponding logics.
Having described classification of composition-nominative logics we can formulate
a task of investigation of logics presented in this classification. For many of such
logics axiomatic calculi were constructed and their properties were investigated [
In this paper we will consider the satisfiability problem for logics of
quantifierequational level. This problem for logics of the previous levels (propositional,
renominative, and quantifier) was considered in [
At first, we describe a general mechanism of specifying composition-nominative logics and then provide definitions for the logics considered in this paper. To do this we should specify three logic components that reflect the semantic-syntactic scheme of logic definition: − semantic component: a class of algebras of quasiary predicates that forms a semantic base for a logic. In our case we consider algebras of the form AQE(V, A)=<PrV,A, ∨, ¬ , Rxv , ∃x, =xy> for various sets of atomic values A (recall that PrV,А= VA p→ Bool is a class of partial predicates over VA); syntactic component: a logic language specified by a class of logic formulas. This class is determined by the logic signature Σ, which includes the infinite set of names V, a set Ps of predicate symbols and a set Cs of composition symbols; the set of formulas Fr(Σ) is constructed inductively over the set of atomic formulas AFr(Σ) with the help of symbols of compositions; interpretational (denotational) component: a parametric total mapping that prescribes to a formula its meaning as a predicate. Parameters are algebra AQE(V, A) t and interpretation for atomic formulas I: AFr(V,Ps) → PrV,A called σinterpretation. A pair (AQE(V, A), I) is called a model of the logic. Given a model M = (AQE(V, A), I) an interpretational mapping for each formula Φ specifies its meaning as a quasiary predicate in AQE(V, A) denoted ΦM. Usually models are represented in simplified form, say J=(V, A, I), called π-interpretations; then the meaning of the formula is denoted ΦJ.
A logic defined according to this scheme is denoted L(Σ). 3.1
Semantic base of composition-nominative logics is specified by classes of data, predicates, and compositions. The latter are determined by the abstraction level of logic under consideration and are the same for all logics of the level. As was formulated earlier, for the logics of quantifier-equational level (QE-level) the class of compositions consists of basic propositional connectives, renomination composition, quantifiers, and equality predicate. The compositions (except propositional connectives) are parametric with parameters from an infinite set of names V.
Therefore we consider the following set of composition symbols:
v
CsQE(V)= { ∨, ¬ } ∪{ Rx | v = (v1,..., vn ) , x = (x1,..., xn ) , v is a list of distinct names, vi , xi ∈V for all i ∈{1,..., n} , n ≥ 0} ∪{ ∃x| x∈V}∪{ =xy | x,y∈V}.
For the sake of simplicity we will write CsQE(V)={ ∨, ¬ , Rxv , ∃x, =xy }.
Given an algebra AQE(V, A)=<PrV,A, ∨, ¬ , Rxv , ∃x, =xy> we now define interpretation of composition symbols. Again, for simplicity’s sake we will use the same notations for compositions (as operations in the algebra) and their symbols.
In definitions of compositions we will use the following notation: − p(d ) ↓ means that a predicate p is defined on data d ; − − − p(d ) ↓= b means that a predicate p is defined on data d with a Boolean value b; p(d ) ↑ means that a predicate p on d is undefined; for nominative data representation we use the form d = [vi aai | i∈I]. Nominative membership relation is denoted by ∈n. Thus, vi aai ∈n d means that the value of vi in d is defined and is equal to ai; this can be written in another form as d(vi)↓=a.
Propositional compositions are defined by the following formulas (p, q∈ PrV,A, d∈VA): 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.
T , if p(d ) ↓= F , (¬p)(d ) = F , if p(d ) ↓= Т , undefined if p(d ) ↑ .
v
Rx Unary renomination composition is a mapping
Rxv : PrV,A t → PrV,A, where v = (v1,..., vn ) and x = (x1,..., xn ) are lists of names from a set V; names from v are called upper names of renomination composition and should be distinct, n ≥ 0. Please note that Rxv is a parametric composition which represents a class of renomination compositions with different parameters, which are elements of V. This composition is defined by the following formula (p∈PrV,A, d∈VA): (Rxv11,,......,,vxnn p) (d ) = p([v a a ∈n d | v ∉{v1,..., vn}] ∇ [vi a d (xi ) | d (xi ) ↓, i ∈{1,..., n}]).
The ∇ operation is defined as follows: if d1 and d2 are two nominative sets, then d = d1∇d2 consists of all named pairs of d2 and only those pairs of d1, whose names are not defined (do not have values) in d2.
Unary parametric composition of existential quantification ∃x with the parameter x∈V is defined by the following formula (p∈PrV,A, d∈ VA): T , if b ∈ A exists : p(d∇x a b) ↓= T , (∃x p)(d ) = F , p(d∇x a a) ↓= F for each a ∈ A,
undefined in other cases.
Here d∇x a a is a shorter form for d∇[x a a] .
Finally, null-ary parametric equality composition =ху (x, y∈V) is defined as follows: T , if d (x) ↓ , d ( y) ↓ and d (x) = d ( y), =ху (d) = T , if d (x) ↑ and d ( y) ↑,
F otherwise
Now we will give definitions for all logics with a fixed infinite set of names V and a fixed set of predicate symbols Ps. Note that according to the tradition elements of V are also called variables. As semantic components for all logics are the same, we need to define only syntactic and interpretational components.
Composition-Nominative Logic LQE(ΣQE) of Quantifier-Equational Level
1. Syntactic component. A tuple ΣQE= (V, {∨, ¬, Rxv , ∃x, =xy}, Ps) is called a signature of composition-nominative logic of QE-level. Taking into consideration that a set of composition symbols is determined by the set of variables V, we will use for a signature a simplified notation (V, Ps). Language of LQE(ΣQE) is represented by a class of formulas FrQE (V, Ps), which is defined inductively: − If P ∈ Ps then P ∈ FrQE(V, Ps). Such formulas are called atomic and belong to the class AFrQE(V, Ps) of atomic formulas. − If x, y ∈V then =ху ∈ FrQE(V, Ps). Such formulas are called atomic and belong to − − the class AFrQE(V, Ps) of atomic formulas.
If Φ, Ψ∈ FrQE(V, Ps) then (Φ∨Ψ)∈FrQE(V, Ps) and ¬Φ∈ FrQE(V, Ps). If v = (v1,..., vn ) , x = (x1,..., xn ) , v is a list of distinct variables, vi , xi ∈V for all i ∈{1,..., n} , n ≥ 0, Φ ∈ FrQE (V, Ps) then Rxv Φ ∈ FrQE (V, Ps). − If x∈V, Φ∈FrQE(V, Ps) then ∃xΦ∈ FrQE(V, Ps).
Note, that predicate symbols and symbols of null-ary compositions are atomic formulas.
2. Interpretational component. Let AQE(V, A)=<PrV,A, ∨, ¬ , Rxv , ∃x, =xy> be an algebra of quasiary predicates of quantifier-equational level. In this algebra composition symbols obtain their interpretations as operations over predicates. In particular, atomic formulas for null-ary compositions =ху are interpreted as equality predicates in this algebra. Thus, we need to specify interpretation mappings for predicate symbols only.
t This is done with a mapping IQPEs :Ps → PrV,A called a σ-interpretation. Having the interpretational mapping for predicate symbols, we can compositionally construct interpretational mapping for all formulas. A pair (AQE(V, A), IQPEs ) is called a model for LQE(ΣQE). A model is determined by a tuple JQPEs =(V, A, IQPEs ) called π-interpretation. In simplified form interpretations will be denoted J. For interpretation J and a formula Φ the meaning of Φ is denoted ΦJ.
with Unessential Variables Unessential variables play a role of additional memory and are used for “storing” values during formula transformations. We assume that a set U of unessential variables is an infinite subset of V (U ⊆V). Informally speaking, logic with unessential variables is a logic LQE (ΣQE) with restriction on interpretations of predicate symbols specified by the set U.
1. Syntactic component. A tuple ΣQEU =(V, U, {∨, ¬, Rxv , ∃x, =xy}, Ps) is called a signature of CNL of QE-level with unessential variables. A class of formulas for LQEU is FrQEU (V, U, Ps)= FrQE (V, Ps) . 2. Interpretational component. Let AQE(V, A) = <PrV,A, ∨, ¬ , Rxv , ∃x, =xy> be an algebra of quasiary predicates of quantifier-equational level. By calling variables from U unessential we actually put a restriction on interpretations of predicate symbols. This t restriction asserts that in σ-interpretation IQPEsU : Ps → PrV , A for every P∈Ps and for every d∈VA the value of IQPEsU (P)(d) does not depend on values of variables from the set U in d. Formally, for every d∈VA the values IQPEsU (P)(d) and IQPEsU (P)(d \\ U) should either be equal or be undefined simultaneously. Here d \\ U= {v aa ∈n d | v∉U}. A π-interpretation will be denoted JQPEsU = (V, U, A, IQPEsU ). Indexes may be omitted if they are clear from the context.
This completes a formal definition of logic LQEU(ΣQEU).
2. Interpretational component. Let AQE(V, A)=<PrV,A, ∨, ¬ , Rxv , ∃x, =xy> be an algebra of quasiary predicates of QE-level (for classical logic we assume that A is nonempty). Note that the renomination composition is present as operation in this algebra, though it is not explicitly used in classical logic. Formulas of the language are interpreted as predicates in this algebra. Atomic formula x=y is interpreted as a predicate =ху. To give an interpretation of atomic formulas of the form Р( х1, ..., хn) we need to specify an interpretational mapping for predicate symbols. In case of classical logic it is specified by a mapping I NPAsr : Ps t → U ( An t → Bool) such that n≥0 I NPAsr (P)∈ An t → Bool if arity(P) = n for P ∈ Ps . This mapping interprets predicate symbols as total n-ary predicates. Thus, π-interpretations have the form JCPLsE =(V, A, arity, I NPAsr ). Such π-interpretation JCPLsE (or simply J) for every atomic formula Р(х1, ..., хn) defines its meaning in PrV,A as a predicate Р(х1,..., хn)J such that Р( х1, ..., хn)J (d) = I NPAsr (Р)(d(х1), …, d(хп)) for every d ∈VA; if one of the values d(х1), …, d(хп) is not defined then Р( х1, ..., хn)J is undefined on d. Let us note that in classical logic d is called variable valuation or variable assignment. The meaning ΦJ of a complex formula Φ∈ FrQECL (Ps, V, arity) is defined in a usual way.
For all three logics derived compositions (such as conjunction &, universal
quantification ∀x, negated equality ≠ xy etc.) are defined in a traditional way. In the sequel we
consider formulas in their traditional form using infix operations and brackets; brackets
can be omitted according to common rules for the priorities of operations (priority of
the binary disjunction is weaker than priory of unary operations). We will also consider
a more general case for I NPAsr permitting partial n-ary predicates as values of
predicate symbols, thus, I NPAsr (P)∈ An p→ Bool; still, this generalization does not affect
the satisfiability problem due to monotonicity of considered compositions under
predicate extensions [
To simplify notation we will often omit parameters of logic signatures and write simply LQE, LQEU, and LQECL; for classes of formulas we use notations FrQE, FrQEU , and FrQECL; formulas of these classes will be called QE-, QEU-, and CL-formulas, πinterpretations in LQE, LQEU, LQECL will also be called QE-, QEU-, CL-interpretations respectively. 3.5
For all three logics the definition of satisfiability can be given in the same way.
A formula Φ is called satisfiable in a π-interpretation J if there is d ∈ VA such that ΦJ (d)↓= T. We shall denote this by J |≈ Φ. A formula Φ is called satisfiable if there exists an interpretation J in which Φ is satisfiable. We shall denote this as |≈ Φ. We call formulas Φ and Ψ equisatisfiable if they are either both satisfiable or both not satisfiable (i.e., unsatisfiable). When needed we will underline the corresponding logic in the satisfiability sign |≈ , e.g. |≈QE , |≈QEU , or |≈QECL .
Satisfiability of a formula is related to its validity. A formula Φ is called valid in a π-interpretation J if there is no d ∈ VA such that ΦJ (d)↓= F. We shall denote this as J |= Φ, which means that Φ is not refutable in J. A formula Φ is called valid if J |= Φ for every interpretation J. We call formulas Φ and Ψ equivalent if ΦJ =ΨJ for every interpretation J.
Due to possible presence of a nowhere defined predicate (which is a valid predicate) we do not have in CNL the property that Φ is satisfiable if Φ is valid (which holds for classical first-order logic). But reduction of satisfiability to validity still holds in CNL: formula Φ is satisfiable in a π-interpretation J iff ¬Φ is not valid in J.
Reduction of Satisfiability Problem for LQE(ΣQE) The problem discussed in this paper is to check whether |≈QE Φ holds given an arbitrary formula Φ∈FrQE(W, Ps); here we choose W as an initial set of variables in the considered logic. Our main aim is to transform this QE-formula Φ to an equisatisfiable formula ΦCL of classical first-order predicate logic with equality so that we can use existent methods for solving this problem developed for classical logic. To carry out necessary equivalent transformations we need to consider Φ in an intermediate logic – CNL of QE-level with unessential variables – extending the initial set of variables W with a set U of unessential variables (W∩U=∅). For these needs we will consider a logic LQEU with the signature ΣQEU =(V, U, {∨, ¬, Rxv , ∃x, =xy}, Ps), where V=W∪U. Within LQEU we transform Φ to a formula Φ UR being in a special normal form; then the latter formula is translated to its classical counterpart Φ CL.
The overall circular reduction scheme is grounded on following statements. 1. From |≈QE Φ follows |≈QEU Φ (lemma 1).
Lemma 1. Let Φ∈FrQE(W, Ps). Then from |≈QE Φ follows |≈QEU Φ .
Consider the transformation rules (T1-T9) of the form Φl a Φ r , where Φl , T3) Rxv (Φ1 ∨ Φ 2 ) a Rxv Φ1 ∨ Rxv Φ2
T5) Rxv ∃y Φ a ∃y Rxv Φ , when y∉{ v , x } Φ r ∈ FrQEU (V ,U ) .
T1) Rxv = xy a = ~x~y T2) Rxv ¬Φ a ¬Rxv Φ T6) R zy,,xv ∃y Φ T7) Ryz,,vx ∃y Φ
a ∃y R vx ( Φ ) left hand side of the rule.
P a Rzz P .
a ∃u Ryz,,vx Ruy Φ , u∈U, u does not occur in the formula on the
T8) R uq P a R zz,,uq P (in case when vectors u , v are empty this rule is represented as
Here for the rule T1 ~x = x(v / x) , ~y = y(v / x) , for the rule T4 αi = si(v1,...,vn, w1,...,wm / x1,...,xn, y1,...,ym), β j = zj(v1,...,vn, w1,...,wm / x1,...,xn, y1,...,ym), where r(b1,...,bq / c1,...,cq) = r if r∉{b1,...,bq}, r(b1,...,bq / c1,...,cq) = ci if r = bi for some i.
The rule T4 represents explicitly the result of functional composition of parameters of two successive renominations.
The rule T7 permits to assume w.l.o.g. that all quantified variables in initial formula are different.
Lemma 2. Let Φl , Φr ∈ FrQEU (V ,U , Ps) be such formulas that Φ r is a result of application of some T1-T9 rule to Φl . Then Φl and Φ r are equisatisfiable in LQEU.
A formula Φ is said to be in unified renominative normal form (URNF) if the following requirements are satisfied: − the renomination composition is only applied in Φ to predicate symbols. It means that for every sub-formula of the form R vx Ψ we have that Ψ∈Ps; for every pair of its renominative atoms R uq P and R wy Q we have that vectors u and w coincide; so, in all renominative atoms the lists of their upper names are the same; for every renominative atom R vx P and every quantifier ∃y that occurs in the initial formula Φ we have that y ∈ v . v
When formula is in URNF we call its atomic subformula Rx P a renominative atom (P∈Ps). Note that if a formula is in URNF then every its subformula is in URNF as well.
Lemma 3. Given an arbitrary formula Φ ∈ FrQEU (V ,U , Ps) we can construct its unified renominative normal form urnf [Φ] by applying rules T1-T9. According to lemmas 2 and 3, we can think of a total multi-valued (non-deterministic) mapping urnf : FrQEU tm→ FrQEU that transforms in a satisfiability-preserving way every QEU-formula to its URNF.
In order to reduce the satisfiability problem in LQEU to that of LQECL we extend the set of basic values A with additional value ε . Informally, this value will represent undefined components of nominative sets.
We formalize the syntactical reduction
t clf : FrQEU (V ,U , Ps) → FrQECL (V , Ps, arity) of QEU-formulas in unified renominative normal form to CLformulas inductively as follows: 1. clf [P] = P
clf [= xy ] = = xy clf [Rvx11,,......,,vxnn P] = P(x1,..., xn ) clf [¬Φ] = ¬clf [Φ] 6.
clf [(Φ1 ∨ Φ 2 )] = ( clf [Φ1] ∨ clf [Φ2 ]) clf [∃xΦ] = ∃x(x ≠ e & clf [Φ]) , e ∈U , e is a predefined variable.
Note that all applications of the 6-th rule introduce the same variable e; e is some predefined variable from U in the sense that it does not occur in URNF.
This reduction transforms the formula to the language of classical logic but preserves its satisfiability.
Given a formula Φ ∈ FrQEU (V ,U , Ps) in unified renominative normal form we denote by VΦ ⊆ V the set of all variables that occur as upper names in renominative atoms of Φ .
Lemma 4. Let Φ be a formula in unified renominative normal form, Φ ∈ FrQEU(V, U, Ps). Then from |≈QEU Φ follows |≈QECL clf [Φ] .
Lemma 5. Let Φ be a formula in renominative normal form, Φ ∈ FrQEU(V, U, Ps). Then from |≈QECL clf [Φ] follows |≈QEU Φ .
Lemma 6. Let Φ∈FrQE(W, Ps). Then from |≈QEU Φ follows |≈QE Φ . Lemmas 1-6 justify all reductions described in the article and the main theorem of the article.
Theorem. Let Φ∈FrQE(W, Ps). Then |≈QE Φ if and only if |≈QECL urnf [clf [Φ]] . The theorem states the reduction of satisfiability problem in composition-nominative logic of quantifier-equational level to the satisfiability problem in classical first-order logic with equality.
Let us illustrate the method proposed on a simple example.
Example. Consider the following QE-formula Φ with one predicate symbol P : Φ = P & Rxz (= zy &∀z¬P) Let us construct its unified renominative normal form ΦUR . Φ = P & Rxz (= zy &∀z¬P) a / push the renomination down to predicate symbols/ a P & = xy &Rxz (∀z ¬P) a /renomination is removed due to T6/ a a P& = xy &(∀z¬ P) a /add Rzz to P as the predicate occurs under ∀z / a a P& = xy &(∀z ¬Rzz P) a /unify renominative atoms / a a Rz P & = xy &∀z ¬Rzz P = ΦUR .
z Note that we use derived transformation rules that handle compositions & and ∀ .
Now ΦCL = cnl[ΦUR ] = P(z) & x = y & ∀z((z ≠ e) → ¬P(z)) . Formula ΦCL is satisfiable in LCL. That means that Φ is satisfiable in LQE.
Indeed, let J = (W, A, I) be such an interpretation that W={x,y,z}, A={1,2}. Let I(P)(d)↓ = F if a pair z a a ∈n d for some a∈A and T in all other cases. In other words, the predicate P takes the value T on some data d if the variable z is undefined in d. Now we have that ΦJ ([ x a 1, y a 1 ])↓ = T.
Many different aspects of the composition-nominative approach such as partiality, compositionality, nominativity, have long history of development, which is also reflected in works in the field of logic and computer science.
The importance of partiality, for example, was already being discussed in detail by
the time of 80-ties [
Compositionality can be traced back to works of G. Frege; the history of this
principle is presented in [
Nominativity is also a fundamental aspect not only in computer science but in other
branches of science as well, especially in philosophy. This topic requires a special
treatment, but here we would like to mention nominal logic [
A thorough comparison of composition-nominative approach with other approaches that address compositionality, nominativity or allow reasoning about partial functions and predicates is by far beyond the scope of this paper, but still we would like to stress on the important differences. Our approach is based on algebras of partial predicates over nominative data, and especially, algebras of quasiary functions and predicates as opposed to traditional algebras of n-ary functions and predicates. It involves new compositions, in particular, renomination composition, which take into account nominative aspects of data structures. Composition-nominative approach also prescribes the semantic-syntactic style of logic definitions. This style simplifies construction and investigation of such logics. 6
This paper investigates the satisfiability problem for composition-nominative logic (CNL) of quantifier-equational level. As a main result we have shown that this problem can be reduced by using more powerful language to the satisfiability problem for classical predicate logic with equality. Thus, existent state-of-the-art methods and techniques for checking satisfiability in classical logics can also be applied to CNL.
Future work on the topic will include investigation of satisfiability problem for
richer CNL of predicate-function level and for CNL over hierarchic nominative data.
Hierarchic data permit to represent such complex structures as lists, stacks, arrays etc;
thus, such logics will be closer to program models with more rich data types. Another
direction is related with identification of classes of formulas in various types of CNL
for which satisfiability problem can be solved efficiently. In particular, this concerns
specialized theories, where some predicates have specific interpretations and several
axioms shall hold for such interpretations. This is often referred to as satisfiability
modulo theory (SMT) problem [