=Paper=
{{Paper
|id=Vol-1844/10000536
|storemode=property
|title=The Canonical Forms of Logical Formulae over the Data Types and
Their Using in Programs Verification
|pdfUrl=https://ceur-ws.org/Vol-1844/10000536.pdf
|volume=Vol-1844
|authors=Michael Lvov,Vladimir Peschanenko,Oleksandr Letychevskyi,Yuliia Tarasich
|dblpUrl=https://dblp.org/rec/conf/icteri/LvovPLT17
}}
==The Canonical Forms of Logical Formulae over the Data Types and
Their Using in Programs Verification==
https://ceur-ws.org/Vol-1844/10000536.pdf
The Canonical Forms of Logical Formulae over the Data
Types and Their Using in Programs Verification
Michael Lvov1, Vladimir Peschanenko1, Oleksandr Letychevskyi2,
Yuliia Tarasich1
1Kherson State University, Universitetskaja St. 27, 73000, Kherson, Ukraine
2Glushkov Institute of Cybernetics of NASU, Glushkov ave., St., 03187, Kyiv, Ukraine
Lvov@ksu.ks.ua, vpeschanenko@gmail.com, lit@iss.org.ua,
YuTarasich@gmail.com
Abstract. A brief review and the results of working with tools for the formulae
simplifying are presented. The algorithm for constructing the canonical forms
of linear semi-algebraic formulae over the enumerated and multiple types is de-
scribed.
Keywords: System of linear inequalities, canonical forms, logical formulae,
linear semi-algebraic formulae, trapezoids.
1 Introduction
A software quality is one of the main tasks of software developers. Therefore, soft-
ware developers are increasingly focusing on the verification which gives them possi-
bilities to search errors before writing a source code of the system and also to prove
various properties of models that were built on the already written code.
In general, methods of the formal models proof can be divided into static and dy-
namic, specific and symbolic. The main problem of static methods for proving prop-
erties of a model is the work with the fairly complex formulae, the complexity of
which can be increased step by step (the construction of invariants, etc.). The main
problem of dynamic methods is a well-known problem in specific modeling - the
exponential explosion of the number of passed states in the model.
On the other hand, there is a lot of number of the well-researched algorithms for
proving properties of models (static and dynamic methods). The problem, which aris-
es in the modeling of specific models is that we get a big numbers of results as a re-
sult of proving their properties. The symbolic modeling is deprived of such problems.
Each state in it is the certain formula that covers a set of specific states. But despite
the fact that the number of states of the symbol model which is given by a formula is
less than in the specific model, in the symbolic modeling the difficult questions of
determining the reachability of passed states in the process of using dynamic methods
and the fairly complex formulae are raised. The complexity of these formulae can
grow step by step if the canonical or normal form is lacking. This implies that the
problem of construction of the canonical and normal forms is one of the most im-
portant problems in the symbol modeling.
In the first part of the article we give a brief review and the analysis of results of
working with the tools for simplifying formulae. In the second part we describe the
algorithm for constructing the canonical forms of linear semi-algebraic formulae off
the enumerated and multiple types.
2 Tools for the Formulae Simplification
There are a lot of tools for prove. All of them can be divided into several types:
- The tools that are based on the extensions of the propositional logic or of the
first-order logics. In this category, the very known tools are: ACL2, E (and E-
SETHEO), KeY, Vampire, Waldmeister, Darwin.
- The tools that are based on the high order logic. The most famous and widely
used of them are: PVS, HOL, Isabelle, Coq.
In this paper, we consider such systems as CVC4, MathSAT5, QEPCAD, Singu-
lar, COCOA, MiniZinc, STP, RedLog, Satallax, Isabelle, E-SETHEO, Minisat,
SMTInterpol, TPS / ETPS, Paradox, Gandalf, Z3, Vampire. The main attention in the
analysis of the considered systems was paid to the availability of tools for the formu-
lae simplifying. The brief characteristics of these systems and the results of their tests
are given below.
CVC4 1.4. CVC4 is an efficient open-source automatic theorem prover for satisfi-
ability modulo theories (SMT) problems. It can be used to prove the validity (or, dual-
ly, the satisfiability) of the first-order formulae in a large number of built-in logical
theories and their combinations [1]. To simplify the formulae in the prover the
TRANSFORM method is used. To obtain normal results, it is necessary to put the
formulae in brackets which determine a problem with the implementation of the prior-
ity of operations. Moreover, the application of the simplification method makes the
formulae more cumbersome (the existence quantifier is always replaced by a generali-
ty quantifier; many symbols of negation appear; can't to remove the quantifiers in an
unclosed formula). Positive characteristics of the prover – it’s the ability to use it in
projects that are developed under C ++, the availability of its documentation and the
user-friendly syntax.
MathSAT5 5.3.10 - is an efficient SMT solver. MathSAT 5 is the successor of
MathSAT 4, supporting a wide range of theories (including e.g. equality and uninter-
preted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (includ-
ing e.g. the computation of Craig interpolants, the extraction of unsatisfiable cores,
the generation of models and proofs, and the ability of working incrementally) [2, 3].
As an input formats it supports SMT-LIB 2, SMT-LIBv1.2, DIMACS. Works with
GMP (Gnu Multiprecision library) and GNU C Library. Can be used in C / C ++ pro-
jects. There is a verification of SAT. The input format is limited to the libraries that it
uses as the input format. It is easy to install and has good documentation, but, unfor-
tunately, the prover doesn't have the tools for the formulae simplifying, which means
that it isn't suitable for solving our problem.
QEPCAD Version B 1.69 - is an interactive command-line program written in
C/C++, which is based on the SACLIB library [4]. One of the most important features
of QEPCAD is its ability to produce the simple quantifier-free equivalent formulae
[22], which points out the possibility of its using to simplify formulae.
This is a very good system for the formulae simplifying. In addition to the stand-
ard quantifiers it includes the existence quantifier "E" and the generality quantifier
"A". Also it supports the additional quantifiers: "F" - for infinitely many; "G" - for all
but certainly many; "C" - for the connected set, "xk" – for the exact number of k dif-
ferent values. Its shortcomings, in our opinion, is the following: 1) The QEPCAD
does not understand the priority of the usage of logical operators; 2) It doesn’t support
the functional symbols (You need to use the algorithms for replace of functionals on
the variables, that makes the formula more cumbersome); 3) It uses the different pa-
rentheses (() – for numeric operations, [] – for logical operations); 4) The negative
numbers must be enclosed in the parentheses and there is no sign of multiplication (5
* x => 5x), which isn't always convenient.
Singular 4.0.3 is the computer algebra system for polynomial computations with
the special emphasis on commutative and non-commutative algebra, algebraic geome-
try, and singularity theory. It is free and open-source under the GNU General Public
Licence [5,6]. The system is easy to install, well documented and has a good syntax.
There is a calculation of invariants. Can be used as the computer algebra system, but
it isn't suitable for solving our problem, since it isn't developed as a system for work-
ing with the mathematical logic (quantifiers are absent, inequalities for logical formu-
lae can't be used, there are no checks for SAT proofs).
COCOA 5.1.3. CoCoA (Computations in Commutative Algebra) [7] is the free
computer algebra system to compute with numbers and polynomials. The CoCoA
(CoCoALib [8]) is available under GNU General Public License. Like as Singular,
the CoCoA system doesn't have the functionality for working with the mathematical
logic (it does not support the quantifiers, it does not simplify the formulae), and
therefore it can not be used to solve our problems.
MiniZinc (WIndows) – is the medium-level constraint modelling language. It is
designed for an easy interaction with the various server solvers. In particular, MiniZ-
inc allows the specification of global constraints by decomposition [9].
MiniZinc is written in C ++. The system works only with integer and rational
numbers. It is a very good tool for modeling and programming. It is easy to install and
has a good documentation. It also has an IDE which makes it easier to work with it.
Unfortunately, it is not suitable for solving our problem. In the model with the help of
such functions as solve satisfy, solve maximize, solve minimize, we set the constraints
on variables (constraint programming) and then we find the solution that satisfies
these constraints.
STP 2.1.2. - is the constraint solver that can solve many kinds of problems includ-
ing those by program analysis tools, theorem provers, automated bug finders, crypto-
graphic algorithms, intelligent fuzzers and model checkers [10]. Supports the CVC,
SMT-LIB1, and SMT-LIB2 data input formats. It is recommended to use the SMT-
LIB2 (although not all features are used in STP). Works with bit vectors and arrays.
Can't work with quantifiers. There is a SAT. As stated in the description, it has a sim-
plifier that includes containing simplification algorithms, but in the sense in which we
need simplifications (we gave a formula → at the output we got a simplified one) it
does not work.
RedLog (Reduce _2015_10_20 Windows) – is an integral part of the interactive
computer algebra system Reduce. It supplements Reduce's comprehensive collection
of powerful methods from symbolic computation by supplying more than 100 func-
tions on first-order formulae [11]. The system has a good syntax, a detailed documen-
tation and it is simple in installation. It supports the functions, quantifiers and priority
of operations. But, it simplified only two formulae. The remaining formulae were
rewritten in a different form. The minuses of the system are: the absence of factoriza-
tion; the absence of SAT and the proof of formulae. The system is written in LISP, so
its integration with C ++ systems is complicated.
Satallax 2.8 - Satallax is the automated theorem prover for higher-order logic Sa-
tallax progressively generates higher-order formulae and corresponding propositional
clauses. These formulae and propositional clauses correspond to a complete tableau
calculus for higher-order logic with a choice operator. Satallax uses the SAT solver
MiniSat as an engine to test the current set of propositional clauses for unsatisfiabil-
ity [12]. It supports the high-order logic. As a data entry format it uses the THF lan-
guage in the TPTP library. There is no documentation of the system; there is only a
brief description. The program isn't oriented on the simplifying of the predicate for-
mulae. It performs its SMT-prover tasks, proves the satisfactories or unsatisfactories
of the problem, but does not simplify the formulae.
Isabelle2016 (Windows) is the generic proof assistant. It allows mathematical
formulae to be expressed in a formal language and provides tools for proving those
formulae in a logical calculus. The main application is the formalization of mathemat-
ical proofs and in particular formal verification, which includes proving the correct-
ness of computer hardware or software and proving properties of computer languages
and protocols. The most widespread instance of Isabelle nowadays is Isabelle/HOL,
which provides a higher-order logic theorem proving environment that is ready to use
for big applications [13]. It is easy to install and has a good documentation. It sup-
ports the work with the first and high order logic. It is a good system in terms of sim-
plifying the formulae. The rules for formulae simplifying are defined by users. In this
regard, it works as a system of rewriting rules. Therefore, the responsibility of simpli-
fications rests with the user. Written in SML, so the integration of this system with C
++ is very difficult.
E-SETHEO. E-SETHEO is the strategy-parallel compositional theorem prover
for the first-order logic with equality. It combines a variety of high-performance theo-
rem provers and specialized decision procedures into one of the most powerful ATP
systems currently available. The core idea of the E-SETHEO framework is to let dif-
ferent proof search procedures compete for resources for solving the given prob-
lem [14].
Unfortunately, we can't install this system. The main problem is that the project
was abandoned for many years, and besides this the system is written on many pro-
gramming languages such as C, Eclipse Prolog, Perl, Bigloo Scheme.
Minisat 2.2.0 – is the minimalistic, open-source SAT solver [15]. The solver is
written in C ++. It has MIT license. It accepts the input data in DIMACS format
(CNF - data input format). There is no simplification of the formulae; therefore the
data input format should be in the conjunctive normal form. Therefore, it can’t be
used to solve our problem.
SMTInterpol 2.1. SMTInterpol is the SMT Solver that can compute Craig inter-
polants for various theories. The current version of SMTInterpol supports interpola-
tion for the combination of the quantifier-free fragments of the theories of uninter-
preted functions, linear real arithmetic, linear integer arithmetic, and arrays [16]. It
uses a SMT-LIB as the input data format. It is written in Java and can be adapted for
C ++. It has an experimental tool for the formulae simplifying. It does not work with
quantifiers. As a result it could not simplify any of the proposed formulae.
TPS/ETPS. TPS and ETPS are, respectively, the Theorem Proving System and
the Educational Theorem Proving System [17]. Unfortunately, there is no access to
download the system, and the available sources do not work. The system is written in
Common Lisp, so their integration into the C ++ system is complicated.
Paradox 3.0. – Paradox is the automated theorem proving system developed by
Koen Lindström Claessen and Niklas Sörensson at the Chalmers University of Tech-
nology. The software is written in the Haskell programming language and is released
under the terms of the GNU General Public License and is free [18]. It is only in the
public folder of the provers of previous CASC tests. It doesn’t work like the previous
systems.
Gandalf c-2.6.r1 - is the first-order automated theorem prover applied to several
domain-specific tasks such as Semantic web. It is programmed in the Scheme pro-
gramming language which is then compiled to the C programming language using
Hobbit from SCM [19]. The access to the prover and its documentation is closed to
those who do not have an access to the account of the University of Tallinn. The last
design date of the work over this prover was the 2003. Since the Gandalf did not take
part in the competitions recent years and we did not get any answers to the letters to
the authors, we can assume that its development stopped.
Vampire 2.6 (Vampire 4.0) is the automatic theorem prover for the first-order
logic. It was used in a number of academic and industrial projects [20]. Vampire im-
plements the calculi of the ordered binary resolution and the superposition for the
handling equality. Internally, Vampire works only with a clausal normal form. Prob-
lems are classified during preprocessing. Vampire implements many useful prepro-
cessing transformations including the Sine axiom selection algorithm [21]. It is said in
the official website that it will be possible to download the prover, after the release of
the 3rd version (although the 4.0 version is already participating in the CASC). The
previous versions cannot be downloaded also. Source codes with CASC contain er-
rors. So, the prover could not be tested.
Z3 is a state-of-the art theorem prover from Microsoft Research. It can be used to
check the satisfiability of logical formulae over one or more theories. Z3 offers a
compelling match for software analysis and verification tools, since several common
software constructs map directly into supported theories [26]. Z3 is a low level tool. It
is best used as a component in the context of other tools that require solving logical
formulae. Consequently, Z3 exposes a number of API facilities to make it convenient
for tools to map into Z3, but there are no stand-alone editors or user-centric facilities
for interacting with Z3. The language syntax used in the front ends favor simplicity in
contrast to linguistic convenience [41, 42].
As it can be seen from the material described above, not all considered systems
were launched and analyzed. The Isabelle2016 is only one system that can completely
done our task. But, in turn, as was mentioned above, it doesn't contain a set of rules
for simplification (the rule process is set by the user himself).
As for QEPCAD ver. B 1.69 then from the point of view of simplifying of the
formulae – the system works well, but it has a fairly complex and cumbersome syntax
and does not have a good documentation.
The most used languages for creating such systems are C / C ++ and ML-
languages (OCaml, SML).
In all systems, we are faced with the problem of the need for rewriting the formu-
lae in a certain format. It is very difficult to rewrite formulae and bring them to the
required format, especially if parentheses are to be placed everywhere, such as in
SMT-LIB. Accordingly, the development of systems for the formulae simplifying,
which would allow the posed tasks is an open problem. In addition, no less important
is the need to implement appropriate algorithms that make it possible to simplify for-
mulae at the more efficient level.
3 The Canonical Forms of Linear Semialgebraic Formulae
Introduce the basic notation:
X {x1 ,...,xn } - is a n - dimensional vector of variables.
Q - is a constructive linearly ordered field, called as the coefficient field.
Q n - is a vector space over Q .
n
a ( a1 ,...,a n ) Q - is a vector of numerical coefficients,
b Q - is a numerical coefficient.
df
LF ( a , X ) -is a linear form from X , a : LF (a, X ) a1x1 ... a n xn
The linear inequality (LI) E(a , X , c) has a form LF ( a , X ) c b and is denoted
by E(a , X , c) . To shorten the record, the linear inequalities will be written in the
form E (X ) , indicating only the variables on which it depends.
Definition 1. A linear semialgebraic formula (LSF) over Q from X is a quanti-
fier-free logical formula F ( X ) F ( E1 ( a1 , X , c1 ),...,E m ( a m , X , cm )) of linear
inequalities E1 ( X ),...E m ( X ) in the signature of logical connectives &, . The linear
n
semialgebraic set M (F ) is a set M ( F )) V Q | F (V ) .
Definition 2. Let x - be a variable that is on the left-hand side of LI with nonzero
coefficient and Y X {x} . Then the LI can be transformed to the form
x LF (b , Y ) c or x LF (b , Y ) c . (1)
Such form of LI will be called resolved with respect to or -resolved. If each LI of a
linear semi-algebraic formula is depending on x , is represented in the allowed form,
then the LSF will be called represented in the x-allowed form. Is represented in the
allowed form, then the LSF will be called represented in the x -allowed form.
By transforming the formula F ( E1 ,...,E m ) according to the rules of proposition-
al algebra of a disjunctive normal form, one can obtain its representation in the form
of a set of LI systems. However, such representation is not the only one and is there-
fore poorly suitable for computer algebra algorithms. The main result of this work is
the definition of the canonical form of a LSF that is possessing by the property of
uniqueness and by the other useful properties, and the description of its construction
algorithm. The proposed canonical form of a LSF is the direct generalization of the
canonical form of the LI system representation and the algorithm for its construction,
those where presented in [29, 30]. The algebraic programming methodology used in
[29] lies in a constructive definition of a multisorted algebraic system [31] whose
objects are represented in the form of expressions, and algorithms compute values of
these expressions, i.e., construct their canonical forms [32–37]. The basic canonical
form of an SLI is the polyhedron of solutions to the SLI in the form of the union of a
finite number of trapezoids. This canonical form uses the idea of projection (elimina-
tion of a quantifier) from the Fourier-Motzkin [38,39] and Tchernikov [40] methods.
Definition3. The formula of a x -segment s [ L(Y ), x, R(Y )] over a set of varia-
bles Y , x Y , is a double linear inequality in the form. L(Y ) x R(Y ) .
If Y { y1 ,...., y m } , then the formula s [ L(Y ), x, R(Y )] is interpreted on the
m1
space Q as an elementary dihedral area
M ( s ) ( q0 , q ) Q
m1
| L( q ) q0 R ( q )] - x - segment.
Inequalities that are represented in the x -resolved form of the form x R (Y ) or
x L(Y ) , can be transformed in x -segments: s [ , x, R(Y )] or
s [ L(Y ), x,] .
m
Let M Q and s [ L(Y ), x, R(Y )] . Define the restriction s M of segment s
df
on M as follows:: s M [ L(Y ), x, R(Y )] M ( L(Y ) x R(Y )) & (Y M ) .
s M if and only if the condition is satisfied q (q M ) (L(q ) R(q )) . This
condition will be written in the form L( x) M R( x) . It is obvious that there is a property
M [ L, x, R] M ' M [ L, x, H ] M ' M [ H , x, R] M ' . (2).
The relation (2) defined on the set of segments the operation of reduction and the
inverse operation of partitioning the set on the part. The exact definition of the parti-
tion is given below.
2.1. Systems of Linear Inequalities and Trapezoids
On the vector variables X {x1,...,xn } defined the order x1 ... xn and denoted
df
X j {x j ,...,xn }
Let s j [ L j ( X j 1 ), x j , R j ( X j 1 )], j 1,...,n 1 ,
sn [Ln , xn , Rn ], Ln , Rn Q .
Definition 4. The set T , defined by the formula T s1 s2 ... sn (the parentheses
are grouped by default to the right), is called a trapezoid in space Q n .
Denote by T j the trapezoid
s j s j 1 ... s n . Then
T T1 , T j s j T j 1 , j 1,2,...,n 1 ,
And T j 1 - is the projection T j on the subspace Q n j 1 , that are determined by
the coordinates {x j 1 ,...,x n } .
Thus, the trapezoid T is defined by a sequence of projections onto a decreasing
sequence of subspaces Q n Q n1 ... Q1 , and each projection is also a trapezoid.
The representation of a trapezoid T in the form of a sequence of its projections
will be denoted by the formula
T T (n) T (n1) ... T (1) .
A convex set P Q n , that is representing the solution of a system of linear ine-
qualities is called a polygon.
Definition 5. By a partition of a set A Q n we mean its representation in the
form of a union of subsets A A1 A2 ... Ak , that
i j Dim( Ai A j ) n .
This means that different elements of the partition cross over a set whose dimen-
sion is less than the dimension of the space ( only a common boundary can exist).
The polygon P can be represented in the form of a partition P T1 ... Tm
into trapezoids T,...,Tm . The algorithm for this representation is described in [29].
Definition 6. The partition P T1 ... Tm will be called irreducible if for any
pair of trapezoids Ti , T j can’t be applied the operation (2).
Arrangement of elements of polygon partitioning on trapezoid. The irreducible
partition of the polygon into trapezoids is unique up to permutations of the trapezoids
of the partition.
The sequence can be ordered in accordance with the following properties. If
( n)
s1 ,...,s m( n) then the sequence of projections of an irreducible partition of a polygon
P T1 ... Tm onto the axis Oxn , then or si( n) s (jn) , or Dim(si( n) s (jn) ) 0 ,
i.e. si( n) , s (jn) either coincide, or don't intersect, or are adjacent. Therefore, s1( n) ,...,s m( n)
can be represented so that they are located on the axis Oxn in ascending order. If
si( n ) ,...,si( n ) are pairwise distinct numerical segments, then the ordering will have the
1 l
form
s1( n ) ... si( n ) [ L1 , xn , L2 ], si( n)1 ... si( n ) [ L2 , xn , L3 ],..., si( n )1 ...
1 1 2 l 1
s m( n ) [ Ll , x n , Ll 1 ] ,
where L1 L2 ... Ll 1 . Then the polygon P can be represented in the form
P (T1 ... Ti1 ) (Ti1 1 ... Ti2 ) ... (Til 1 ... Tm )
or
P (T1( n1) ... Ti( n1) ) si( n) (Ti(n11) ... Ti( n1) ) si( n) ...
1 1 1 2 2
(Ti(n11) ... Tm( n1) ) s m( n) .
l
Denote the partitions of trapezoids in parentheses through Pi1( n 1) , Pi2( n 1) , ..., Pm( n1) .
Then P Pi1( n1) si(1n ) Pi2( n1) si(2n ) ... Pm( n 1) s m( n ) .
The property of polygon partitioning that are described above holds for projec-
tions of any dimension. Namely, let P T1 ... Tl - is a irreducible partition of a
polygon with common k 1 - th projection T ( k 1) :
T1 T1(1) ... T1(k ) T (k 1) ,...,Tl Tl(1) ... Tl(k ) T (k 1) .
Then T,...,Tl can be ordered in such a way that the canonicity property is ful-
filled:
s1( k ) ... si( k ) [ L1 , xk , L2 ], si( k)1 ... si( k ) [ L2 , xk , L3 ],..., si( k )1 ...
1 1 2 l 1
s m( k ) [ Ll , x k , Ll 1 ] , (2.1)
L1 T ( k 1 L2 T ( k 1 ... T ( k 1 Ll 1 . (2.2)
An irreducible partition of the polygon into trapezoids ordered in accordance with
the canonical property will be called the canonical decomposition or the canonical
sum.
Since Ti( j ) = projection Ti( j 1) onto a subspace Q j , the Definition 5 means that
in the canonical sum any projections of trapezoid summands can intersect only along
their boundary. Relation (2) can be called an operation of bringing of similar.
Theorem 1. Let be a system of linear inequalities and P Q n ia a polygon (a
convex set in Q n ), defined by this system. Then P can be represented in the form of
the canonical sum of trapezoids P T1 ... Tk .
Algorithm 1 (intersection of trapezoids). On the set of trapezoids in space Q n it
is natural to define the operation of intersection T1 T2 . As shown in [29], this inter-
section can be represented as the canonical sum of trapezoids. Consider the algorithm
for computing the intersection T1 T2 T1' ... Tk' . Let T1 , T2 in the form
T1 T1( n1) s1n , T2 T2( n1) s 2 n . Then T1 T2 is evaluated recursively "from below-
up".
Recursion basis:
s1n s 2n T1 T2 else T1 T2 (T1( n1) T2( n1) ) ( s1n s 2n ),
max(L1n , L2n ) T min( R1n , R2n )] s1n s2n [max(L1n , L2n ), x1,
min( R1n , R2n )]else s1n s2n (3)
Recursion step:
Suppose that T1 T1( nk ) T1( k ) , T2 T2( nk ) T2( k ) and T1( k ) T2( k ) has already
been calculated, and T1( k ) T2( k ) T1' ... Tl' . Then, due to the distributive mark
«++»with respect to a mark «», the computation reduces to the calculation
(T1( nk ) T2( nk ) ) T j' , and this calculation, in turn, reduces to calculation
(s1nk s 2nk ) T j' , j 1,...,l. The result of the operation must satisfy the conditions
in (3).
Since max(L1 , L2 ), min( R1 , R2 ) are not linear combinations, the result of the op-
eration of intersection of segments s1nk s2nk on T j' depends on the mutual ar-
rangement of these segments on the trapezoid T j' .
The relation L(Y ) T R(Y ) is defined as follows: L(Y ) T R(Y ) , if for any vector
Y0 T the inequality L(Y0 ) Rk (Y0 ) holds. In the canonical form of a representation
of a trapezoid T , these relations must be satisfied for any value k n, n 1,...,1 on
subspaces Q k .
Let us first consider the problem of calculating the intersection s1 s2 on T in
general terms.
Let s1 [L1 , x, R1 ], s2 [L2 , x, R2 ] , T1 s1 T , T2 s2 T , and
L1 T R1 , L2 T R2 .
df
Let LLij T ( Li T L j ) , RRij T ( Ri T R j ) , LRij Li T R j ,
df
[ LR]ij [ Li , x, R j ], i, j 1,2 (4)
And we list the relations in the form of rewriting rules for all variants of the mutu-
al arrangement of the lower and upper caps T1 , T2 , writing formulae (3) in terms of
(4):
RR12 ( // variants 1-6
1. LR12 T1 T2 ,
2. (L2 R1 T ) & LL12 T1 T2 [LR]21 LR21 ,
( L2 R1 T ) & ( L2 L1 T ) T1 T2 [ LR]21 LL21 &
3.
LR21 [ LR]11 LL21
4. LR21 & LL12 T1 T2 [LR]21 T ,
5. LL21 & (L1 L2 T ) T1 T2 [LR]21 LL12 [LR]11 LL21 ,
6. LL12 T1 T2 T2
);
(R2 R1 T ) & LR12 ( // variants 7-11
( L2 R1 T ) & LL12 T1 T2 [ LR]21 LR21 & RR12
1.
[ LR]22 RR21
( L2 R1 T ) & ( L2 T L1 ) T1 T2 [ LR]21 LL12 &
2. ,
LR21 [ LR]11 RR12 & LL21 [ LR]12 RR21
3. LR21 & LL12 T1 T2 [LR]21 RR21 [LR]22 RR12 ,
LR21 & ( L1 T L2 ) ) T1 T2 [ LR]21 LL12 [ LR]11 LL21 & RR12
4. 5.
[ LR]12 RR21 & LL21
LL21 T1 T2 [LR]11 RR12 [LR]12 RR21
);
(R2 R1 T ) & (R2 L1 T ) ( // variants 12-14
( R1 L2 T ) & ( L1 L2 T ) T1 T2 [ LR]21 RR12 &
1.
LL12 , [ LR]22 RR12 & LL21 [ LR]12 RR21 & LL21,
LR21 & ( L1 L2 T ) T1 T2 [ LR]21 RR12 & L12 [ LR]11
2.
RR12 & LL21 [ LR]12 RR21 & LL21,
3. LL21 T1 T2 [LR]12 RR21
);
RR21 & LR12 ( // variants 15-17
1. LL12 T1 T2 T2 ,
2. L1 L2 T T1 T2 [LR]22 LL12 [LR]12 LL21 ,
3. LL21 T1 T2 [LR]12 T
);
RR21 & (L1 R2 ) ( // variants 18-19
1. L1 L2 T T1 T2 [LR]22 LL12 [LR]12 LL21 ,
2. LL21 T1 T2 [LR]12 LR21
);
1. RR21 T1 T2 . // variant 20
Algorithm 2 (Variant recognition) is described in [30].
Algorithm 3 (Intersection of polygons). The operation of polygons intersection
P1 P2 is described by a system of ratio - rewriting rules. Let
P1 T11 T12 ... T1k1 , P2 T21 T22 ... T2 k2 .
Represented P1 , P2 as P1 g G, P2 h H , where
g T11, h T21 , G T12 ... T1k1 , H T22 ... T2k2 .
The basic rule is:
( g G)(h H ) gh ( gH hG) HG (5)
Let g T '[l g , rg ], h T ' '[l h , rh ] . Then, if rg rh gH , and if
rh rg hG . This makes it possible to simplify rule (5). We introduce the follow-
df
ing access functions: for T T 's , Base(T ) s , for s [ L, x, R]
LP( s) L, RP( s) R . Then (4) simplify:
RP( Base( g )) RP( Base(h)) ( g G)(h H ) gh hG HG
else ( g G)(h H ) gh gH HG (6)
Derivatives rules are derived from (5) for special cases G or H :
RP(Base( g)) RP(Base( g)) g(h H ) gh else g(h H ) gh gH (7)
RP( Base( g )) RP( Base(h)) ( g G)h gh hG
else ( g G)h gh (8)
The rewriting system (6) - (8) represents an algorithm for polygons intersecting.
2.2. Linear Semi-Algebraic Formulae and Polytrapezoids
Definition6. Let Y ( y1 ,..., y m ), x Y , T Q m . The algebra of x - poly-
segments (polysegments) over the base T is a constructive extension of the algebra
of x - segments which elements of carrier have a
form: S T ([L1, x, R1 ] [L2 , x, R2 ] ... [Lk , x, Rk ]) T , Li ,
Li (Y ), Ri Ri (Y ) (9)
with the following conditions:
1. L1 T R1 T L2 M R2 T ... T Lk T Rk , Ri Li1 ; (10)
2. if for some i Ri Li1 , the record (3) is reduced in accordance with (2):
[Li , x, Ri ] [Li1 , x, Ri1 ] [Li , x, Ri1 ] .
On the algebra of polysegments defined set-theoretic operations of intersection
and union. It's obvious that
([L1, x, R1 ] ... [Lk , x, Rk ]) T [L1 , x, R1 ] T ...[Lk , x, Rk ] T .
Definition7. Let X j ( x1 ,...,x j ) , j 1, 2,...,n . Define the sequence S j recur-
sively:
1. s1i [ai , x1 , bi ], a j , b j Q, i 1,...,k1 . S1 s11 ... s1k1 - Basic, x1 - poly-
df
sergment, T1 S1 .
2. For any j 1,...,n 1 S j 1 - x j 1 is a polysergment over T j , and
df
T j 1 S j 1 T j .
A set Tn (or simply T ) is called a polytrapecoid in space Q n . Obviously,
T Sn Sn1 ... S1 , and T j - projection T j 1 onto the subspace Q j , defined by the
coordinates x1 ,...,x j .
The polytrapecoid T is defined by a sequence of projections onto a decreasing se-
quence of subspaces Q n Q n1 ... Q1 , with each projection also a polytrapezoid.
Algorithm 4 (intersection of polytrapecoids). Let PT1 , PT2 be a polytrapecoid
and P PT1 PT2 . Obviously, P can be represented as a canonical sum of poly-
trapecoids. The algorithm for intersecting polythracoids computes P recursively
"bottom-up".
Basis of recursion.
Let PT1 S11 ... S1n , PT2 S21 ... S2n . Then
PT1 PT2 ( PT1( n1) PT2( n1) ) ( S1n S 2n ) (11)
The relation (11), in accordance with Definition 6, 1 defines a recursion basis -the
calculation algorithm of S1n S2n , which is defined by the rewriting rules (6) - (8)
and represents the sum of the segments of the numerical axis Oxx , satisfying (10).
Step of recursion.
Let for some k PT1 S11 ... S1nk ST ( k ) , PT2 S 21 ... S 2nk ST ( k ) , , where
ST (k ) is the sum of polythracoids, representing (S1nk ...S1n ) (S 2nk ...S 2n ) , i.е.
ST ( k ) ( S1nk ...S1n ) ( S 2nk ...S 2n ) ,
PT1 PT2 ((S11 ... S1nk ) ( S 21 ... S 2nk )) ST ( k ) (12)
Then we rewrite (12) in the form
PT1 PT2 ((S11 ... S1nk 1 ) ( S 21 ... S 2nk 1 ))(S1nk S 2 nk ) ST ( k ) ,
reducing the problem to the step of recursion - computing ( S1nk S 2 nk ) ST ( k ) .
Since ST (k ) is the sum of polytrapecoids, ST (k ) PT1(k ) ... PTl(k )
(S1nk S 2nk ) ST (k ) (S1nk S 2nk ) PT1(k ) ... (S1nk S 2nk ) PTl(k ) For
the calculation, (S1nk S 2nk ) PT j(k ) algorithms 1-3 described above are applied.
Algorithm 5 (unification of polythracoids). Let PT1 , PT2 are the polythrape-
zoids and P PT1 PT2 . P can be represented in the form of a canonical sum of
polytrapecoids. Let
PT1 PT1( n1) S1n , PT2 PT2( n1) S 2n .
Let S12n S1n S 2n , S1' n S1n S12n , S 2' n S 2n S12n
Then S1n S1' n S12n , S 2n S 2' n S12n and
PT1 PT2 Ord ( PT1( n1) S1' n PT2( n1) S 21n ( PT1( n1) PT2( n1) ) S12n (13)
where the function Ord () orders the summands. The calculation algorithm
S1' n , S 2' n , S12n in (13) computes S12n , using algorithms 1-3 and recursively computes
PT1( n1) PT2( n1) . The calculation algorithm S1' n S1n S12n , S 2' n S 2n S12n is
similar to algorithm (3).
In conclusion, we note that the algebra of linear semialgebraic sets is constructed
as a chain of extensions of the algebras of trapezoids, polygons and polytrapezoids by
an overload of set-theoretic operations &,
Theorem 2. Every linear semialgebraic set M (see Definition1) can be uniquely
represented as a sum of polytrapecoids: M GT1 GT2 ... GTk
4 The Canonical Forms of Logical Formulae off the
Enumerated Type
An enumerated data type we have defined as a finite ordered set
A {a1 , a2 ,...,am } with logical operations that are order predicates and equality pred-
icates. We restrict the consideration with the predicate of non-strict order, because the
strict order obviously is expressed by non-strict order, order is denoted as " , " and
equality is denoted as "" .
Consider unquantified formulae of applied logic of predicate over the type Exam-
ine unquantified formulae of applied logic of predicate off the type A in the signature
of logical connectives &, to determine their canonical forms that are analogous
to the canonical forms of linear semi-algebraic formulae which were mentioned
above.
The algorithm for the canonical form calculation of the logical formulae off
the enumeration type
Suppose that X {x1 ,...,xn } , x1 ... xn - is an ordered set of object variables
and F (P1 ,...,Pk ; X ) is a formula of the applied predicate logic off A by the atomic
predicates P1 ,...Pk and by the object variables from the set X . The atomic predicates
P1 ,...Pk have the form x y, x y, x y , where x, y are/or the object variables with
the aim of defining A , or the elements A .
The preliminary simplification F (P1 ,...,Pk ; X ) is the elimination of the equalities
and the bringing of atomic equalities to the form x y or x y , where x X ,
y X A , and if y X , then x y.
Submit the x - segments [ L, x, R] as double inequalities L x R , and trapezoids
in a form T s1 ... sn , si [Li , xi , Ri ] . Each inequality can be represented as a trap-
ezoid. Stand for min a1 , max am . Then, by convention of an enumerated type, for
x X a priori we have the representation
s x(0) [min, x, max] , (*)
and for inequalities x y, x y = accordingly
s x y [min, x, y ], s x y [ y, x, max] . (**)
In accordance with this, each atomic inequality Pj x ji y or Pj x ji y of
the formula F (P1 ,...,Pk ; X ) can be presented in the form of an atomic trape-
zoid T ( j ) s1 j ... s nj , x ji - the segment of which has the form (**), and the other
segments have the form (*). We replace the logic ligaments &, by operations , .
As a result, the calculation of the canonical form F (P1 ,...,Pk ; X ) is reduced to the
calculation of values F (T (1) ,...,T ( k ) ; X ) .
Algorithms for computing of the canonical forms of trapezoid intersections, poly-
gons, polytrapezoids and of linear semialgebraic formulae off an enumerated type are
essentially represented by the foregoing algorithms. Point out, that due to the simple
of right part of inequalities the algorithm 2 of the option recognition has simpler form
than in the general case.
5 The Canonical Forms of Logical Formulae off the Multiple
Type
Multiple data type Set(U ) is defined as the algebra of subsets off a finite set –
universum U {u1 , u2 ,...,um } , signature set-theoretic operations ,, and
affiliations operations a A , equality a b and negation of equality a b . Consid-
er the unquantified formulae of applied predicate logic off the type Set(U ) of varia-
bles X ( x1 ,...,xn ) of type Var in the signature of the logical connectives
&,, to determine their canonical forms, which are analogous to canonical
forms of linear semi-algebraic formulae, which were mentioned above.
First of all, give consideration the logical product of the form
0 & & , where
x1 A1 xi1 y1 x j1 z1
x 2 A2 xi 2 y 2 x j 2 z 2
0 , , (1)
. . .
x n An xik y k x z
jl l
elementary conjunctions of which have the appropriate form x A, x y, x z ,
where A U , x, y, z X . It can be assumed that the conditions are met in (1):
1. In the part 0 all conjuncts are included in the form x j A j , j 1,..,n . (In
particular, the conjunct can be in the form x j U or x a , i.e. x{a} .
2. If in is a conjunct in the form x y , then the conjunct of the form x y
will be absent in (otherwise, a conjunction is false).
The following relation can be used for the simplification of (1):
( x A) & ( y B) & ( x y) ( x A B) & ( x y) (2)
After this transformation we obtain the conjunction of the form
0 & &
x1 A1 xk 1 y1 x j1 z1
x 2 A2 xk 2 y 2 x j 2 z2
0 , , , (3)
. . .
x k Ak xn y nk x z
jl l
where {y1 ,...,ynk } {x1 ,...xk } . Analyze the X 0 ( x1 ,...,xk ), X ( xk 1 ,...,xn ) .
So, if we consider only the parts 0 , of the (3) conjunction, variables of the sub-
set X 0 will be considered as independent, and the variables X as correlate relations
of equalities of the part of the formula (3). Thus, we have received the canonical
form 0 & of formula (1) with up to the order of elementary conjuncts. The
uniqueness is ensured by the ordering of variables in the left part of the elementary
conjuncts: x1 x2 ... xk ; xk 1 xk 2 ... xn .
To simplify 0 & the formula (3) define a mapping : X X base :
x, if х X base
( x)
y, if ( x y) Fequ
Apply the relation to the of formula (3)
( x y) (( x) ( y)) (4)
as a rewriting rule. As a result, in we obtain the equalities canonized system
of negations, in which {x j1 ,...,x jl } X 0 , {z1 ,...,z l } X 0 . If in this system is an
equation in the form x x then the formula (3) is false.
Theorem 3. Formula (3) which is obtained as a result of above transformations, to
the formula (1) is the canonical form of (1).
On the analogy of the terminology used above, the canonical form (3) of the for-
mula (1) is designated as a trapezoid off the multiple type. On the analogy of the
presentation of the trapezoid off the type Rat , formula of trapezoid off the multi-
ple type will be written in the form
1 ... k k 1 ... n , 1 & ...& l ,
0 1 ... k , k 1 ... n , 1 & ...& l .
Label the trapezoid 1 ... k k 1 ... n1, 1 & ...& l by ( n1) . Then
we can write ( n1) n .
Operations of union and intersection by trapezoid off the multiple type
Let 1 , 2 be the trapezoids off the multiple type. Then the canonical form
1 2 is calculated as the algorithm described above, applied to
( 0,1 ,1 ) & ( 0,2 ,2 ) .
The calculation algorithm of 1 2 is the modification of the algorithm of pol-
ytrapezoids union. Supposing that
1 0,1 & ,1 & ,1 , 2 0,2 & ,2 & ,2 . The projection of the trap-
ezoid on the coordinate set Oxn of variable x n is equal or An
, if equality
xn An is an elementary conjunct 0 , or A j , if ( x j A j ) 0 , ( x n x j ) .
Let us assume that the 1,n , 2,n are the projections 1 , 2 on Oxn . Then
1 2 1 2 3 , (5)
where
1,n 1,n 2,n , 3 ,n 2,n 1,n , 2 ,n 1,n 2,n , (6)
(0n,11) (0n,11) , ,1 .1 , ,1 ,1 ,
(0n,31) (0n,21) , ,3 ,2 , ,1 ,3 , (7)
(2n1 1( n1) (2n1) . (8)
The formulae (5) - (8) represent a recursive algorithm for the computing
1 2 .
6 Conclusions
The development of systems for the formulae simplifying, which would allow the
posed tasks remains an open problem. In addition, no less important is the need to
implement appropriate algorithms that makes it possible to simplify formulae at the
more efficient level.
The main result of this work is the definition of the canonical form of a linear
semi-algebraic formulae that is possessing by the property of uniqueness and by the
other useful properties, and the description of its construction algorithm.
In the next article authors plan to describe the implementation of the proposed al-
gorithms by the method of insertion modeling and results of their using in tasks of
programs verification.
References
1. CVC4, http://cvc4.cs.nyu.edu/web/
2. Mathsat, http://mathsat.fbk.eu/
3. Cimatti A. et al. The mathSAT5 SMT solver //International Conference on Tools and Al-
gorithms for the Construction and Analysis of Systems. – Springer Berlin Heidelberg,
2013. – С. 93-107.
4. QEPCAD, https://www.usna.edu/CS/qepcadweb/B/WhatisQEPCAD.html
5. Greuel G. M., Pfister G., Schönemann H. Singular 2.0: A Computer Algebra System for
Polynomial Computations. University of Kaiserslautern (2001).
6. Singular, https://www.singular.uni-kl.de/
7. COCOA, http://cocoa.dima.unige.it/
8. COCOA, http://cocoa.dima.unige.it/cocoalib/
9. MINIZINC, http://www.minizinc.org/
10. STP constraint solver, http://stp.github.io/
11. Redlog, http://www.redlog.eu/
12. Satallax, http://www.ps.uni-saarland.de/~cebrown/satallax/
13. Isabelle, https://isabelle.in.tum.de/
14. E-SETHEO, http://www4.informatik.tu-muenchen.de/~schulz/WORK/e-setheo.html
15. MiniSat, http://minisat.se/
16. SMTInterpol, http://ultimate.informatik.uni-freiburg.de/smtinterpol/
17. About SMTInterpol, http://gtps.math.cmu.edu/tps-about.html
18. Theorem-proving system, http://dic.academic.ru/dic.nsf/eng_rus/793528/theorem
19. Gandalf, http://deepthought.ttu.ee/it/gandalf/
20. Vampire, http://www.vprover.org/download.cgi
21. Vampire 4.1-SMT System Description, http://smtcomp.sourceforge. net/
2016/systemDescriptions/ Vampire.pdf
22. QEPCAD - The Solution Formula Construction Phase,
https://www.usna.edu/CS/qepcadweb/B/user/Solution.html
23. The E Theorem Prover, http://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html
24. iProver, http://www.cs.man.ac.uk/~korovink/iprover/
25. LEO-II, http://page.mi.fu-berlin.de/cbenzmueller/leo/
26. Z3Prover, https://github.com/Z3Prover/z3
27. ABOUT WALDMEISTER, http://www.waldmeister.org/
28. SPASS, http://www.mpi-inf.mpg.de/departments/automation-of-logic/software/spass-
workbench/
29. M. S. Lvov, “Algebraic approach to the problem of solving systems of linear inequalities,”
Cybernetics and Systems Analysis, 46, No. 2, 326–338 (2010).
30. Lvov, M. S., and V. S. Peschanenko. "Trapezoid method for solving systems of linear ine-
qualities and its implementation in insertion modeling." Cybernetics and Systems Analy-
sis 48, No. 6, 931-942. (2012)
31. J. Goguen and J. Meseguer, “Ordered-sorted algebra I: Partial and Overloaded Operations,
Errors and Inheritance,” Computer Science, 105, No. 2, 217–273 (1992).
32. J. A. Goguen, J. W. Thatcher, and E. Wagner, “An initial algebra approach to the specifi-
cation, correctness and implementation of abstract data types,” in: R. Yeh (ed.), Current
Trends in Programming Methodology, Prentice Hall, NJ (1978), pp. 80–149.
33. M. S. Lvov, “Synthesis of interpreters of algebraic operations in extensions of multisorted
algebras,” Visn. Khark. Nats. Un-tu, No. 847, 221–238 (2009).
34. M. S. Lvov, “Verification of interpreters of algebraic operations in extensions of multisort-
ed algebras,” KhUPS, No. 3(21), 127–137 (2009).
35. M. S. Lvov, “Method of inheritance in implementing algebraic computations in mathemat-
ical systems of educational destination,” Syst. Upravl., Navigats. 3 Zv’yazku, TsNDINiU,
No. 3 (11), 120–130, (2009).
36. M. S. Lvov, “Method of morphisms in implementing algebraic computations in mathemat-
ical systems of educational destination,” Systemy Obrobky Informatsii, No. 6 (80), 183–
190 (2009)
37. M. S. Lvov, “An approach to the implementation of algebraic computations: Computations
in propositional algebra,” Visn. Khark. Nats. Un-tu, Information Technologies:
Mathematical Modeling, No. 863, 157–168 (2009).
38. T. S. Motzkin, H. Raiffa, G. L. Thompson, and R. M. Thrall “The double description
method” in: Matrix Games, Fizmatgiz, Moscow (1961), pp. 81–109.
39. G. L. Zeidler, Lectures on Convex Polytopes, Springer, Berlin–New York (1994).
40. S. N. Tchernikov, Linear Inequalities [in Russian], Nauka, Moscow (1968).
41. Z3, http://rise4fun.com/z3/tutorial/guide
42. De Moura, Leonardo, and Nikolaj Bjørner. "Z3: An efficient SMT solver." International
conference on Tools and Algorithms for the Construction and Analysis of Systems.
Springer Berlin Heidelberg (2008).