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 described.
A software quality is one of the main tasks of software developers. Therefore, software developers are increasingly focusing on the verification which gives them possibilities 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 dynamic, specific and symbolic. The main problem of static methods for proving properties 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 arises in the modeling of specific models is that we get a big numbers of results as a result 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 important 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
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 ESETHEO), 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, Singular, 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 formulae 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 satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, 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 priority of operations. Moreover, the application of the simplification method makes the formulae more cumbersome (the existence quantifier is always replaced by a generality 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 uninterpreted functions, linear arithmetic, bit-vectors, and arrays) and functionalities (including 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 ++ projects. 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, unfortunately, 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 standard 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 different 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 parentheses (() – 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 geometry, 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 working with the mathematical logic (quantifiers are absent, inequalities for logical formulae 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, MiniZinc 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 including those by program analysis tools, theorem provers, automated bug finders, cryptographic algorithms, intelligent fuzzers and model checkers [10]. Supports the CVC, SMT-LIB1, and SMT-LIB2 data input formats. It is recommended to use the SMTLIB2 (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 simplifier 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 functions on first-order formulae [11]. The system has a good syntax, a detailed documentation 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 factorization; 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 Satallax 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 unsatisfiability [12]. It supports the high-order logic. As a data entry format it uses the THF language 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 formulae. 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 mathematical proofs and in particular formal verification, which includes proving the correctness 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 supports the work with the first and high order logic. It is a good system in terms of simplifying 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 simplifications 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 theorem 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 different proof search procedures compete for resources for solving the given problem [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 programming 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 interpolants for various theories. The current version of SMTInterpol supports interpolation for the combination of the quantifier-free fragments of the theories of uninterpreted 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 Technology. 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 programming 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 implements the calculi of the ordered binary resolution and the superposition for the handling equality. Internally, Vampire works only with a clausal normal form. Problems are classified during preprocessing. Vampire implements many useful preprocessing 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 errors. 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 MLlanguages (OCaml, SML).
In all systems, we are faced with the problem of the need for rewriting the formulae 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 formulae at the more efficient level. 3
Introduce the basic notation:
Q - is a constructive linearly ordered field, called as the coefficient field. Q n - is a vector space over Q . a (a1,...,an ) Q n - 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 ) a x ...a n xn 1 1
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
fier-free logical formula F ( X ) F (E1(a1, X , c1),...,Em (am , X , cm )) of linear inequalities E1( X ),...Em ( X ) in the signature of logical connectives &, . The linear semialgebraic set M (F ) is a set M (F )) V Qn | 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 . (
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,...,Em ) according to the rules of propositional 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 therefore 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 (elimination 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 variables Y , x Y , is a double linear inequality in the form. L(Y ) x R(Y ) .
If Y {y1,....,ym }, then the formula s [L(Y ), x, R(Y )] is interpreted on the as an elementary dihedral area space
Q m1 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 s [L(Y ), x,] .
be transformed in x -segments: s [, x, R(Y )] or
Let M Qm and s [L(Y ), x, R(Y )] . Define the restriction s M of segment s on
M df 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
The relation (
Let s j [L j ( X j1), x j , R j ( X j1)], j 1,...,n 1 ,
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 Qn .
Denote by T j the trapezoid s j s j1 ... s
n . Then T T1 , T j s j T j1, j 1,2,...,n 1 ,
And T j1 - is the projection T j on the subspace Q n j1 , that are determined by the coordinates {x j1,...,xn } .
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 (
A convex set P Q n , that is representing the solution of a system of linear inequalities 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 i j Dim( Ai Aj ) n .
A A1 A2 ... Ak , that
This means that different elements of the partition cross over a set whose dimension 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 (
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 s1(n) ,...,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(1n) ,...,si(ln) are pairwise distinct numerical segments, then the ordering will have the form s (n) ... si(n) [L1, xn , L2 ], si(1n)1 ... si(n) [L2 , xn , L3 ],..., s (n) 1 1 2 il11 ... s (n) [Ll , xn , Ll1 ] , m where L1 L2 ... Ll1 . Then the polygon P can be represented in the form P (T1 ... Ti1 ) (Ti11 ... Ti2 ) ... (Til 1 ... Tm ) or P (T1(n1) ... Ti(n1) ) si(n) (T (n1) ... Ti(n1) ) si(n) ...
1 1 i11 2 2 (Til(n11) ... Tm(n1) ) s m(n) .
Denote the partitions of trapezoids in parentheses through Pi1(n1) , Pi2(n1) ,...,Pm(n1) . Then P Pi1(n1) si(1n) Pi2(n1) si(2n) ... Pm(n1) s m(n) .
The property of polygon partitioning that are described above holds for projections 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 l
Then T,...,Tl can be ordered in such a way that the canonicity property is fulfilled: s (k ) ... si(k ) [L1, xk , L2 ], si(1k)1 ... si(k ) [L2 , xk , L3 ],..., s (k ) 1 1 2 il11 ... s (k ) [Ll , xk , Ll1 ] ,
m L1 T (k 1 L2 T (k 1 ... T (k 1 Ll1 . (2.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( j1) 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 (
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 .
is natural to define the operation of intersection T1 T2 . As shown in [29], this intersection 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) s2n . Then T1 T2 is evaluated recursively "from belowup".
Recursion basis: s1n s2n T1 T2 else T1 T2 (T1(n1) T2(n1) ) (s1n s2n ), max(L1n , L2n ) T min(R1n , R2n )] s1n s2n [max(L1n , L2n ), x1,
min(R1n , R2n )]else s1n s2n (
Since max(L1, L2 ),min(R1, R2 ) are not linear combinations, the result of the operation of intersection of segments s1nk s2nk on T j' depends on the mutual arrangement 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 (
And we list the relations in the form of rewriting rules for all variants of the
mutual arrangement of the lower and upper caps T1, T2 , writing formulae (
RR12 ( // variants 1-6 1. LR12 T1 T2 , 2. (L2 R1 T ) & LL12 T1 T2 [LR]21 LR21,
LR21 [LR]11LL21 4. LR21 &LL12 T1 T2 [LR]21T , 5. LL21 &(L1 L2 T ) T1 T2 [LR]21 LL12 [LR]11 LL21, [LR]22 RR21
LR21 [LR]11 RR12 &LL21 [LR]12 RR21 (L2 R1 T )&(L2 T L1 ) T1 T2 [LR]21 LL12 &, 3. LR21 &LL12 T1 T2 [LR]21 RR21 [LR]22 RR12 , 4.
LR21 &(L1 T L2) ) T1 T2 [LR]21 LL12 [LR]11 LL21 & RR125. 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]21RR12 & LL12, [LR]22 RR12 &LL21 [LR]12 RR21 &LL21, LR21 &(L1 L2 T ) T1 T2 [LR]21RR12 &L12 [LR]11
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 ... T2k2 .
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 (
RP(Base(g)) RP(Base(h)) (g G)(h H ) gh hG HG
else(g G)(h H) gh gH HG (
Derivatives rules are derived from (
else (g G)h gh (
The rewriting system (
polysergment over
T j , and ST (k) is the sum of polythracoids, representing (S1nk ...S1n ) (S2nk ...S2n ) , i.е.
ST (k ) (S1nk ...S1n ) (S2nk ...S2n ) ,
PT1 PT2 ((S11 ... S1nk ) (S21 ... S2nk )) ST (k)
Then we rewrite (
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) S2n .
Let S12n S1n S2n , S1'n S1n S12n , S 2'n S2n S12n
Then S1n S1'n S12n , S2n S 2'n S12n and
PT1 PT2 Ord (PT1(n1) S1'n PT2(n1) S21n (PT1(n1) PT2(n1) ) S12n (
S1'n S1n S12n , S 2'n S2n S12n is
similar to algorithm (
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
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 predicates. 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 Examine 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.
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 trapezoid. Stand for min a1, max am . Then, by convention of an enumerated type, for x X a priori we have the representation s(0) [min, x, max], x (*) and for inequalities x y, x y = accordingly sxy [min, x, y], sxy [ 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
trapezoid T ( j) s1 j ... snj , x j - the segment of which has the form (**), and the other
i
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 (
Algorithms for computing of the canonical forms of trapezoid intersections, polygons, 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
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 . Consider the unquantified formulae of applied predicate logic off the type Set(U) of variables 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 x2 A2 ,
xi2 y2
0
. .
xn An xik yk
x j1 z1
x j2 z2
,
.
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 (
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).
After this transformation 0 & &
,
xn ynk
set X 0 will be considered as independent, and the variables X as correlate relations
of equalities of the part of the formula (
To simplify 0 & the formula (
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,...,zl } X 0 . If in this system is an
equation in the form x x then the formula (
Theorem 3. Formula (
On the analogy of the terminology used above, the canonical form (
Label the trapezoid 1 ... k k1 ... n1,1 &...& l by (n1) . Then we can write (n1) n .
Let 1, 2 be the trapezoids off the multiple type. Then the canonical form as the algorithm described above, applied to
The calculation algorithm of 1 2 is the modification of the algorithm of polytrapezoids union. Supposing that 1 0,1 & ,1 & ,1, 2 0,2 & ,2 & ,2 . The projection of the trapezoid xn An is an elementary conjunct 0 , or A j , if (x j A j ) 0 , (xn x j ) .
on the coordinate set Oxn of variable xn is equal or An , if equality
Let us assume that the 1,n , 2,n are the projections 1, 2 on Oxn . Then
1 2 1 2 3 ,
where
1,n 1,n 2,n , 3,n 2,n 1,n , 2,n 1,n 2,n ,
(0n,11) (0n,11) , ,1 .1, ,1 ,1,
(0n,31) (0n,21) , ,3 ,2 , ,1 ,3 ,
(
The formulae (
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 algorithms by the method of insertion modeling and results of their using in tasks of programs verification. 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).