=Paper=
{{Paper
|id=None
|storemode=property
|title=Satisfiability Problem in Composition-Nominative Logics of Quantifier-Equational Level
|pdfUrl=https://ceur-ws.org/Vol-848/ICTERI-2012-CEUR-WS-paper-38-p-56-70.pdf
|volume=Vol-848
|dblpUrl=https://dblp.org/rec/conf/icteri/NikitchenkoT12
}}
==Satisfiability Problem in Composition-Nominative Logics of Quantifier-Equational Level==
https://ceur-ws.org/Vol-848/ICTERI-2012-CEUR-WS-paper-38-p-56-70.pdf
Satisfiability Problem in Composition-Nominative Logics
of Quantifier-Equational Level
Mykola S. Nikitchenko1 and Valentyn G. Tymofieiev1
1
Department of Theory and Technology of Programming
Taras Shevchenko National University of Kyiv
64, Volodymyrska Street, 01601 Kyiv, Ukraine
nikitchenko@unicyb.kiev.ua
tvalentyn@univ.kiev.ua
Abstract. 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.
Keywords: Composition-nominative logics, partial predicates, partial logics,
first-order logics, satisfiability, validity.
Key Terms. Research, MathematicalModel, FormalMethods,
MachineIntelligence.
1 Introduction
Last years the interest to the satisfiability problem [1] has risen due to practical value it
has obtained in such areas as program verification, synthesis, analysis, testing, etc. [2–
5]. In this paper we address the satisfiability problem in the context of the composition-
nominative approach [6], which aims to construct a hierarchy of logics of various ab-
straction and generality levels on the methodological basis, which is common with
programming. The main principles of the approach are principles of development from
abstract to concrete, priority of semantics, compositionality, and nominativity.
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
Satisfiability Problem in Composition-Nominative Logics … 57
nominative data. Such data consist of pairs name–value. Nominative data can repre-
sent various data structures such as records, arrays, lists, relations, etc. [6, 7]; this fact
explains the importance of the notion of nominative data. In the simplest case nomi-
native data can be considered as partial mappings from a certain set of names (vari-
ables) V into a set of basic (atomic) values A. These data are called nominative sets;
their class is denoted VA. Nominative sets represent program states for simple pro-
gramming languages (see, for example, [6, 8]). Partial predicates and functions over
p
V
A are called quasiary, their classes are denoted PrV,А= VA → Bool and FnV,А=
p p
V
A → A respectively. Partial mappings of type VA → VA are called bi-
quasiary. Such mappings represent program semantics for simple programming lan-
guages; therefore their class is denoted PrgV,A. From this follows that semantic models
of programs and logics are mathematically based on the notion of nominative set
(nominative data in general case). This fact permits to integrate models of programs
and logics and represent them as hierarchy of composition-nominative models [9, 10].
Logics developed within such approach are called composition-nominative logics
(CNL) because their predicates and functions are defined on classes of nominative
data, and logical connectives and quantifiers are formalized as predicate composi-
tions.
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 algo-
rithm that reduces the satisfiability problem in this logic to the same problem in clas-
sical 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 [10].
2 Classification of Composition-Nominative Logics
Classification of composition-nominative logics is based on classification of their
parameters: data, predicates, and compositions. The main semantic notion of mathe-
matical 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 composi-
tions as disjunction ∨, negation ¬, etc., can be defined. These compositions are de-
rived from Kleene’s strong connectives [11] when partiality of predicates is taken into
consideration. Thus, the main semantic objects for logics of this level are algebras of
p
partial predicates of the type . The obtained logics may be
58 M. S. Nikitchenko and V. G. Tymofieiev
called propositional logics of partial predicates. Such logics are rather abstract, there-
fore 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 nomina-
tive 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,А;
3. 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 [10] are most abstract among the above-mentioned logics. The
main composition for these logics is the composition of renomination (renaming),
t
which is a total mapping R vx1 ,..., vn
,..., x : Pr
V,А
→ PrV,А. Intuitively, given a quasiary
1 n
predicate P and a nominative set d, the value of R vx1 ,..., vn
,..., x (P)(d) is evaluated in the
1 n
following way: first, a new nominative set d ′ is constructed from d by changing the
values of the names v1,...,vn in d to the values of the names x1,..., xn respectively; then
predicate P is applied to d ′. The obtained value of P (if it was evaluated) will be the
result of R vx1 ,..., vn
,..., x (P)(d). For simplicity’s sake we will also use the simplified notation
1 n
R vx for renomination composition. The basic composition operations of renominative
logics are ∨, ¬, and R vx .
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 intro-
duce 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 differen-
tiating 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 function-
equational 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 [6, 10]), which formalizes substitution of functions into predi-
cate. It also seems natural to introduce special 0-ary compositions, called denaming
functions 'x. Given a nominative set, 'x yields a value of the name x in this set. Intro-
duction of such functions allows one to model renomination compositions with the
help of superposition. The basic compositions of logics of the function level are ∨, ¬,
S x , ∃x, and 'x.
Satisfiability Problem in Composition-Nominative Logics … 59
At the function-equational level a special equality composition = can be introduced
additionally [10]. The basic compositions of logics of the function-equational level
are ∨, ¬, S x , ∃x, 'x, and = . At this level different classes of first-order logics can be
presented.
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 quasi-
ary 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 consid-
ered 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 [10,
12].
In this paper we will consider the satisfiability problem for logics of quantifier-
equational level. This problem for logics of the previous levels (propositional,
renominative, and quantifier) was considered in [13]. We choose a reduction method
that reduces the satisfiability problem of composition-nominative logic to the satisfi-
ability in classical logic. To simplify this reduction we will use an intermediate logic
with unessential variables. Thus, we will define three logics of quantifier-equational
level: composition-nominative logic, logic with unessential variables, and classical
first-order logic.
3 Formal Definitions of Logics of Quantifier-Equational Level
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 se-
mantic base for a logic. In our case we consider algebras of the form
60 M. S. Nikitchenko and V. G. Tymofieiev
AQE(V, A)= for various sets of atomic values A (recall
p
that PrV,А= VA → 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 pre-
scribes 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 Algebras of Quasiary Predicates of Quantifier-Equational Level
Semantic base of composition-nominative logics is specified by classes of data, predi-
cates, 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 composi-
tions consists of basic propositional connectives, renomination composition, quantifi-
ers, 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:
CsQE(V)= { ∨, ¬ } ∪{ R xv | 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)={ ∨, ¬ , R xv , ∃x, =xy }.
Given an algebra AQE(V, A)= we now define interpreta-
tion of composition symbols. Again, for simplicity’s sake we will use the same nota-
tions 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.
Satisfiability Problem in Composition-Nominative Logics … 61
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 ) ↑ .
t
Unary renomination composition R xv is a mapping R xv : PrV,A
→ 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 R xv is a parametric composition which represents a class of renomina-
tion compositions with different parameters, which are elements of V. This composi-
tion is defined by the following formula (p∈PrV,A, d∈VA):
v ,...,v
( R x1,..., xn p) (d ) = p([v a a ∈n d | v ∉ {v1 ,..., vn }] ∇ [vi a d ( xi ) | d ( xi ) ↓, i ∈ {1,..., n}]).
1 n
The ∇ operation is defined as follows: if d1 and d2 are two nominative sets, then
d = d1∇d 2 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.
62 M. S. Nikitchenko and V. G. Tymofieiev
3.2 ΣQE) of Quantifier-Equational Level
Composition-Nominative Logic LQE(Σ
1. Syntactic component. A tuple ΣQE= (V, {∨, ¬, R xv , ∃x, =xy}, Ps) is called a signa-
ture 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 signa-
ture 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 R xv Φ ∈ 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 for-
mulas.
2. Interpretational component. Let AQE(V, A)= be an al-
gebra 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
Ps
This is done with a mapping I QE :Ps
→ PrV,A called a σ-interpretation. Having the
interpretational mapping for predicate symbols, we can compositionally construct in-
Ps
terpretational mapping for all formulas. A pair (AQE(V, A), I QE ) is called a model for
Ps Ps
LQE(ΣQE). A model is determined by a tuple J QE =(V, A, I QE ) called π-interpretation.
In simplified form interpretations will be denoted J. For interpretation J and a formula
Φ the meaning of Φ is denoted ΦJ.
3.3 Composition-Nominative Logic LQEU(ΣQEU) of Quantifier-Equational Level
with Unessential Variables
Unessential variables play a role of additional memory and are used for “storing” val-
ues 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, {∨, ¬, R xv , ∃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) .
Satisfiability Problem in Composition-Nominative Logics … 63
2. Interpretational component. Let AQE(V, A) = 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 I QEU
Ps
: Ps
→ PrV , A for every P∈Ps and
Ps
for every d∈VA the value of I QEU (P)(d) does not depend on values of variables from
Ps Ps
the set U in d. Formally, for every d∈VA the values I QEU (P)(d) and I QEU (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 J QEU
Ps Ps
= (V, U, A, I QEU ). Indexes may be
omitted if they are clear from the context.
This completes a formal definition of logic LQEU(ΣQEU).
3.4 Classical First-Order Predicate Logic L QECL(ΣQECL) with Equality
A definition of classical logic differs from definitions of CNL because it is oriented not
on quasiary but on n-ary predicates.
1. Syntactic component. A tuple ΣQECL = (V, {∨, ¬, ∃x, =}, Ps, arity) is called a sig-
t
nature of a classical logic with equality (here arity: Ps → {0,1,2, …} is a function
that for each predicate symbol yields its arity). A signature in a simplified form is de-
noted (V, Ps, arity). The language FrQECL (V, Ps, arity) is defined inductively:
− If P ∈ Ps , arity(P)=n, and х1, ..., хn ∈V, then Р( х1, ..., хn) ∈ FrQECL (V, Ps, ar-
ity). Such formulas are called atomic and belong to the class AFrQECL(V, Ps, arity)
of atomic formulas.
− If x, y ∈ V then x=y ∈ Fr QECL (V, Ps, arity). Such formulas are called atomic and
belong to the class AFrQECL(V, Ps, arity) of atomic formulas.
− If Φ, Ψ∈ FrQECL (V, Ps, arity) then (Φ∨Ψ)∈FrQECL (V, Ps, arity) and ¬Φ∈
FrQECL (V, Ps, arity).
− If x∈V, Φ∈ FrQECL (V, Ps, arity) then ∃xΦ∈ FrQECL (V, Ps, arity).
2. Interpretational component. Let AQE(V, A)= be an al-
gebra of quasiary predicates of QE-level (for classical logic we assume that A is non-
empty). Note that the renomination composition is present as operation in this alge-
bra, 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 predi-
cate =ху. 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
t t
Ps
logic it is specified by a mapping I NAr : Ps
→ U ( A n
→ Bool) such that
n≥0
t
I NAr (P) ∈ A
Ps n
→ Bool if arity ( P) = n for P ∈ Ps . This mapping interprets predi-
cate symbols as total n-ary predicates. Thus, π-interpretations have the form
Ps
J CLE Ps
=(V, A, arity, I NAr ). Such π-interpretation J CLE
Ps
(or simply J) for every
64 M. S. Nikitchenko and V. G. Tymofieiev
atomic formula Р(х1, ..., хn) defines its meaning in PrV,A as a predicate Р(х1,..., хn)J
Ps
such that Р( х1, ..., хn)J (d) = I NAr (Р)(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 mean-
ing Φ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 quantifi-
cation ∀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
Ps
a more general case for I NAr permitting partial n-ary predicates as values of predi-
p
Ps
cate symbols, thus, I NAr (P) ∈ A n → Bool; still, this generalization does not affect
the satisfiability problem due to monotonicity of considered compositions under predi-
cate extensions [13].
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 Satisfiability Problem
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.
Satisfiability Problem in Composition-Nominative Logics … 65
4 ΣQE)
Reduction of Satisfiability Problem for LQE(Σ
The problem discussed in this paper is to check whether |≈ QE Φ holds given an arbi-
trary 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 equisatisfi-
able 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 vari-
ables 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, {∨, ¬, R xv , ∃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).
2. From |≈ QEU Φ follows |≈ QEU ΦUR (lemma 2, 3).
3. From |≈ QEU ΦUR follows |≈ QECL Φ CL (lemma 4).
4. From |≈ QECL Φ CL follows |≈ QEU ΦUR (lemma 5).
5. From |≈ QEU ΦUR follows |≈ QEU Φ (lemma 2).
6. From |≈ QEU Φ follows |≈ QE Φ (lemma 6).
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 ,
Φ r ∈ FrQEU (V , U ) .
T1) R xv = xy a = ~x ~y
T2) R xv ¬Φ a ¬R xv Φ
T3) R xv (Φ1 ∨ Φ 2 ) a R xv Φ1 ∨ R xv Φ 2
v ,...,v , w ,..., w v ,...v ,u ,...,u v ,...,v , w ,..., w ,u ,...,u
T4) R x1,..., xn , y1,..., y m Rs1,...,sп , z1 ,..., zk Φ a Rα1 ,...,αn , y1 ,..., ym , β1 ,...,βk Φ
1 n 1 m 1 п 1 k 1 n 1 m 1 k
T5) R xv ∃y Φ a ∃y R xv Φ , when y∉{ v , x }
T6) R zy,,xv ∃y Φ a ∃y R vx ( Φ )
T7) R yz,,vx ∃y Φ a ∃u R yz,,vx Ruy Φ , u∈U, u does not occur in the formula on the
left hand side of the rule.
T8) R uq P a R zz,,uq P (in case when vectors u , v are empty this rule is represented as
P a Rzz P .
66 M. S. Nikitchenko and V. G. Tymofieiev
u ,..., u ,..., u ,..., u u ,..., u ,..., u ,..., u
T9) Rq1,..., q i ,..., q j ,..., q n P = Rq1..., q j,..., q i,..., q n P
1 i j n 1 j i n
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 fol-
lowing 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 ini-
tial formula Φ we have that y ∈ v .
When formula is in URNF we call its atomic subformula R xv 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)
tm
mapping urnf : FrQEU → 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.
t
We formalize the syntactical reduction clf : FrQEU (V , U , Ps )
→
FrQECL (V , Ps, arity ) of QEU-formulas in unified renominative normal form to CL-
formulas inductively as follows:
1. clf [ P ] = P
2. clf [= xy ] = = xy
v ,...,v
3. clf [ R x1 , ... , xn P] = P( x1 ,..., xn )
1 n
4. clf [¬Φ ] = ¬clf [Φ ]
Satisfiability Problem in Composition-Nominative Logics … 67
5. clf [(Φ1 ∨ Φ 2 )] = ( clf [Φ1 ] ∨ clf [Φ 2 ])
6. 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 pre-
serves its satisfiability.
Given a formula Φ ∈ FrQEU (V , U , Ps ) in unified renominative normal form we de-
note 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 & R xz (= zy &∀z¬P)
Let us construct its unified renominative normal form ΦUR .
Φ = P & R xz (= zy &∀z¬P) a / push the renomination down to predicate symbols/
a P & = xy & R xz (∀z ¬P) a /renomination is removed due to T6/ a
a P& = xy &(∀z¬ P) a /add R zz to P as the predicate occurs under ∀z / a
a P& = xy &(∀z ¬R zz P ) a /unify renominative atoms / a
a R zz P & = xy &∀z ¬R zz P = ΦUR .
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.
68 M. S. Nikitchenko and V. G. Tymofieiev
5 Related work
Many different aspects of the composition-nominative approach such as partiality,
compositionality, nominativity, have long history of development, which is also re-
flected 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 [14], and many different approaches have emerged since that time.
In [15, 16] there is a survey of some of those and a comparison of different formalisms.
Partiality receives more and more attention nowadays, the support for partial functions
is being introduced in theorem proving systems and validity checkers [17, 18].
Compositionality can be traced back to works of G. Frege; the history of this princi-
ple is presented in [19]. The importance of the compositionality principle grows due to
the necessity of investigation and verification of complex systems [20, 21], in particu-
lar, concurrent systems [22]. Our approach takes compositionality as a basic principle,
thus, the constructed formal languages are compositional by construction when we
consider functions (predicates) as meanings of expressions (of formulas).
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 [23] only, which has simi-
larities with the logic defined in this paper. Nominal logic addresses such special ques-
tions of nominativity as name bindings, swapping, and freshness. The predicates inves-
tigated in nominal logic should be equivariant (their validity is invariant under name
swapping); in our work we consider general classes of partial predicates.
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 com-
positions, in particular, renomination composition, which take into account nominative
aspects of data structures. Composition-nominative approach also prescribes the se-
mantic-syntactic style of logic definitions. This style simplifies construction and inves-
tigation of such logics.
6 Conclusions
This paper investigates the satisfiability problem for composition-nominative logic
(CNL) of quantifier-equational level. As a main result we have shown that this prob-
lem 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
Satisfiability Problem in Composition-Nominative Logics … 69
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 [24]. At last, prototypes of software systems for satisfi-
ability checking in CNL should be developed.
References
1. Mendelson E.: Introduction to Mathematical Logic, 4th ed. Chapman & Hall, London
(1997)
2. Kroening D., Strichman O.: Decision Procedures – an Algorithmic Point of View.
Springer-Verlag, Berlin Heidelberg (2008)
3. Marques-Silva J.: Practical Applications of Boolean Satisfiability. In: Workshop on Dis-
crete Event Systems (28-30 May 2008, Goteborg, Sweden), pp. 74--80 (2008)
4. Nieuwenhuis R., Oliveras A., Tinelli C.: Solving SAT and SAT modulo theories: from an
abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J ACM 53, pp. 937--
977 (2006)
5. de Moura L., Bjørner N.: Satisfiability Modulo Theories: Introduction and Applications.
COMMUN ACM 54 (9), pp. 69--77 (2011)
6. Nikitchenko, N.S.: A Composition Nominative Approach to Program Semantics. Techni-
cal Report IT−TR 1998-020, Technical University of Denmark (1998)
7. Basarab I.A., Gubsky B.V., Nikitchenko N.S., Red'ko V.N.: Composition Models of Da-
tabases. In: Eder J., Kalinichenko L.A. (eds.), East-West Database Workshop (Workshops
in Computing Series), pp. 221--231. Springer, London (1995)
8. Nielson H.R., Nielson F.: Semantics with Applications: A Formal Introduction. John
Wiley & Sons Inc (1992)
9. Nikitchenko M.S.: Composition-nominative aspects of address programming. Kibernetika
I Sistemnyi Analiz 6, pp. 24--35 (In Russian) (2009)
10. Nikitchenko M.S., Shkilnyak S.S.: Mathematical logic and theory of algorithms. Publish-
ing house of Taras Shevchenko National University of Kyiv, Kyiv, (in Ukrainian) (2008)
11. Kleene, S. C.: Introduction to Metamathematics. Van Nostrand, New York (1952)
12. Shkilniak S. S.: First-order logics of quasiary predicates. Kibernetika I Sistemnyi
Analiz 6, pp. 32--50, (in Russian) (2010)
13. Nikitchenko M.S., Tymofieiev V.G.: Satisfiability Problem in Composition-Nominative
Logics. In: Proceedings of the Eleventh International Conference on Informatics
INFORMATICS’2011, Roznava, Slovakia, November 16-18, pp. 75--80 (2011)
14. Blamey, S.: Partial Logic. In Gabbay D., Guenthner F. (eds.), Handbook of Philosophical
Logic, Volume III, D. Reidel Publishing Company (1986)
15. Jones C. B.: Reasoning About Partial Functions in the Formal Development of Programs.
ENTCS 145, pp. 3--25 (2006)
16. Owe O.: Partial Logics Reconsidered: A Conservative Approach. FORM ASP
COMPUT 5, pp. 208--223 (1997)
17. Mehta F. A.: Practical Approach to Partiality A Proof Based Approach. LNCS, vol. 5256,
pp. 238--257. Springer, Heidelberg (2005)
18. Berezin S., Barrett C., Shikanian I., Chechik M., Gurfinkel A., Dill D.L.: A Practical Ap-
proach to Partial Functions in CVC Lite. ENTCS 125, pp. 13--23 (2005)
70 M. S. Nikitchenko and V. G. Tymofieiev
19. Janssen T.M.V.: Compositionality. In van Benthem J., ter Meulen A. (eds.), Handbook of
Logic and Language, pp. 417--473. Elsevier and MIT Press (1997)
20. de Roever, W.-P., Langmaack H., Pnueli A. (eds.): Compositionality: The Significant
Difference. LNCS, vol. 1536, VIII. Springer, Heidelberg (1998)
21. Bjørner D., Eir A.: Compositionality: Ontology and Mereology of Domains. LNCS,
vol. 5930, pp. 22--59. Springer, Heidelberg (2010)
22. Dams D., Hannemann U., Steffen M. (eds.): Concurrency, Compositionality, and Cor-
rectness, Essays in Honor of Willem-Paul de Roever. LNCS, vol. 5930. Springer, Heidel-
berg (2010)
23. Pitts, A. M.: Nominal Logic, A First Order Theory of Names and Binding. INFORM
COMPUT 186, pp. 165--193 (2003)
24. Barrett C., Sebastiani R, Seshia S. A., Tinelli C.: Satisfiability Modulo Theories.
In: Biere A., Heule M., van Maaren H., Walsh T. (eds.), Handbook of Satisfiability. IOS
Press (2009)