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.
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][3][4][5]. In this paper we address the satisfiability problem in the context of the compositionnominative approach [6], which aims to construct a hierarchy of logics of various abstraction 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 nominative data. Such data consist of pairs name-value. Nominative data can represent 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 nominative data can be considered as partial mappings from a certain set of names (variables) V into a set of basic (atomic) values A. These data are called nominative sets; their class is denoted V A. Nominative sets represent program states for simple programming languages (see, for example, [6,8]). Partial predicates and functions over A are called biquasiary. Such mappings represent program semantics for simple programming languages; therefore their class is denoted Prg V,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 compositions.
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 [10].
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 [11] when partiality of predicates is taken into consideration. Thus, the main semantic objects for logics of this level are algebras of partial predicates of the type <D → p Bool; ∨, ¬>. The obtained logics may be 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: Pr V,А ; 2. quasiary predicate-function logics based on algebras with two sorts: Pr V,А and Fn V,А ; 3. quasiary program logics based on algebras with three sorts: Pr V,А , Fn V,А , and Prg V,А . 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), which is a total mapping R x (P)(d). For simplicity's sake we will also use the simplified notation R v
x for renomination composition. The basic composition operations of renominative logics are ∨, ¬, and R v x . 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 v
x , 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 v x , ∃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 x S (see [6,10]), which formalizes substitution of functions into predicate. 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. Introduction of such functions allows one to model renomination compositions with the help of superposition. The basic compositions of logics of the function level are ∨, ¬, x S , ∃x, and 'x.
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 ∨, ¬, x S , ∃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:
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 [10,12].
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 [13]. We choose a reduction method that reduces the satisfiability problem of composition-nominative logic to the satisfiability 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.
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
Bool is a class of partial predicates over V A); − 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)
and interpretation for atomic formulas I: AFr(V,Ps) → t Pr V,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(Σ).
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:
For the sake of simplicity we will write
Given an algebra AQE(V, A)=<Pr V,A , ¬ ∨, , v x R , ∃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 Propositional compositions are defined by the following formulas (p, q∈ Pr V,A , d∈ V A):
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 v x R 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∈Pr
The ∇ operation is defined as follows: if d 1 and d 2 are two nominative sets, then Unary parametric composition of existential quantification ∃x with the parameter x∈V is defined by the following formula (p∈Pr V,A , d∈ V A):
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 L QE (Σ Σ Σ Σ QE ) of Quantifier-Equational Level
Note, that predicate symbols and symbols of null-ary compositions are atomic formulas.
x R , ∃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. In simplified form interpretations will be denoted J. For interpretation J and a formula Φ the meaning of Φ is denoted Φ J .
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 L QE (Σ QE ) with restriction on interpretations of predicate symbols specified by the set U. Fr QECL (V, Ps, arity). − If x∈V, Φ∈ Fr QECL (V, Ps, arity) then ∃xΦ∈ Fr QECL (V, Ps, arity).
x R , ∃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 , …, 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 Φ∈ Fr QECL (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 the satisfiability problem due to monotonicity of considered compositions under predicate extensions [13].
To simplify notation we will often omit parameters of logic signatures and write simply L QE , L QEU , and L QECL ; for classes of formulas we use notations Fr QE , Fr QEU , and Fr QECL ; formulas of these classes will be called QE-, QEU-, and CL-formulas, πinterpretations in L QE , L QEU , L QECL will also be called QE-, QEU-, CL-interpretations respectively.
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 ∈ V A 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.
Satisfiability of a formula is related to its validity. A formula Φ is called valid in a π-interpretation J if there is no d ∈ V A such that Φ J (d)↓= F. We shall denote this as
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 L QE (Σ Σ Σ Σ QE )
The problem discussed in this paper is to check whether Φ ≈ QE | holds given an arbitrary formula Φ∈Fr QE (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 L QEU with the signature
, where V=W∪U. Within L QEU 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.
From
From
From
.
Consider the transformation rules (T1-T9) of the form
R Φ , u∈U, u does not occur in the formula on the left hand side of the rule. T8) R u q P a R u q , z , z P (in case when vectors v u, are empty this rule is represented as
q q q q u u u u q q q q ,..., ,..., ,..., ,..., ,..., ..., ,..., ,..., ,..., ,..., ,..., ,..., , for the rule T4 α i = s i (v 1 ,...,v n , w 1 ,...,w m / x 1 ,...,x n , y 1 ,...,y m ), β j = z j (v 1 ,...,v n , w 1 ,...,w m / x 1 ,...,x n , y 1 ,...,y m ), where r(b 1 ,...,b q / c 1 ,...,c q ) = r if r∉{b 1 ,...,b q }, r(b 1 ,...,b q / c 1 ,...,c q ) = c i if r = b i 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. 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 v
x Ψ we have that Ψ∈Ps; − for every pair of its renominative atoms R u q P and R w y 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 v
x P and every quantifier ∃y that occurs in the initial formula Φ we have that v y ∈ .
When formula is in URNF we call its atomic subformula P R v x a renominative atom (P∈Ps). Note that if a formula is in URNF then every its subformula is in URNF as well.
, U e ∈ , 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
Note that we use derived transformation rules that handle compositions & and ∀ .
))
Indeed, let J = (W, A, I) be such an interpretation that W={x,y,z}, A={1,2}. Let
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 Φ
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 [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 principle 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 particular, 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 similarities with the logic defined in this paper. Nominal logic addresses such special questions of nominativity as name bindings, swapping, and freshness. The predicates investigated 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 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.
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 [24]. At last, prototypes of software systems for satisfiability checking in CNL should be developed.