01d-Predicate-Proofs
- 格式:ppt
- 大小:598.50 KB
- 文档页数:11


模糊逻辑中英文对照外文翻译文献(文档含英文原文和中文翻译)译文:模糊逻辑欢迎进入模糊逻辑的精彩世界,你可以用新科学有力地实现一些东西。
在你的技术与管理技能的领域中,增加了基于模糊逻辑分析和控制的能力,你就可以实现除此之外的其他人与物无法做到的事情。
以下就是模糊逻辑的基础知识:随着系统复杂性的增加,对系统精确的阐述变得越来越难,最终变得无法阐述。
于是,终于到达了一个只有靠人类发明的模糊逻辑才能解决的复杂程度。
模糊逻辑用于系统的分析和控制设计,因为它可以缩短工程发展的时间;有时,在一些高度复杂的系统中,这是唯一可以解决问题的方法。
虽然,我们经常认为控制是和控制一个物理系统有关系的,但是,扎德博士最初设计这个概念的时候本意并非如此。
实际上,模糊逻辑适用于生物,经济,市场营销和其他大而复杂的系统。
模糊这个词最早出现在扎德博士于1962年在一个工程学权威刊物上发表论文中。
1963年,扎德博士成为加州大学伯克利分校电气工程学院院长。
那就意味着达到了电气工程领域的顶尖。
扎德博士认为模糊控制是那时的热点,不是以后的热点,更不应该受到轻视。
目前已经有了成千上万基于模糊逻辑的产品,从聚焦照相机到可以根据衣服脏度自我控制洗涤方式的洗衣机等。
如果你在美国,你会很容易找到基于模糊的系统。
想一想,当通用汽车告诉大众,她生产的汽车其反刹车是根据模糊逻辑而造成的时候,那会对其销售造成多么大的影响。
以下的章节包括:1)介绍处于商业等各个领域的人们他们如果从模糊逻辑演变而来的利益中得到好处,以及帮助大家理解模糊逻辑是怎么工作的。
2)提供模糊逻辑是怎么工作的一种指导,只有人们知道了这一点,才能运用它用于做一些对自己有利的事情。
这本书就是一个指导,因此尽管你不是电气领域的专家,你也可以运用模糊逻辑。
需要指出的是有一些针对模糊逻辑的相反观点和批评。
一个人应该学会观察反面的各个观点,从而得出自己的观点。
我个人认为,身为被表扬以及因写关于模糊逻辑论文而受到赞赏的作者,他会认为,在这个领域中的这种批评有点过激。
第五章证据理论(Evidence Theory)方法在本章§1,我们将讨论一种被称之为登普斯特-谢弗(Dempster-Shafer)或谢弗-登普斯特(Shafer-Dempster)理论(简称D-S理论或证据理论)的不精确推理方法。
这一理论最初是以登普斯特(Dempster,1967年)的工作为基础的,登普斯特试图用一个概率区间而不是单一概率数值去建模不确定性. 1976年,谢弗(Shafer,1976年)在《证据的数学理论》一书中扩展和改进了登普斯特工作. D-S理论具有好的理论基础。
确定性因子能被证明是D-S 理论的一种特殊情形。
在§2我们将描述一种简化的证据理论模型MET1 . 在§3我们将给出支持有序命题类问题的具有凸函数性质的简化证据理论模型。
围绕证据理论的一些新的研究工作,将在第六章介绍。
§1D-S理论(Dempster-Shafer Theory)●辨别框架(Frames of Discernment)D-S理论假定有一个用大写希腊字母Θ表示的环境(environment),该环境是一个具有互斥和可穷举元素的集合:Θ = { θ1 , θ2 , ⋯, θn }术语环境在集合论中又被称之为论域(the universe of discourse)。
一些论域的例子可以是:Θ = { airliner , bomber , fighter }Θ = { red , green , blue , orange , yellow }Θ = { barn , grass , person , cow , car }注意,上述集合中的元素都是互斥的。
为了简化我们的讨论,假定Θ是一个有限集合。
其元素是诸如时间、距离、速度等连续变量的D-S 环境上的研究工作已经被做。
理解Θ的一种方式是先提出问题,然后进行回答。
假定Θ = { airliner , bomber , fighter }提问1:“这军用飞机是什么?”;答案1:是Θ的子集{ θ2 , θ3 } = { bomber , fighter }提问2:“这民用飞机是什么?”;答案2:是Θ的子集{ θ1} = { airliner },{ θ1} 是单元素集合。
Mechanical Proving for ERDÖS-SZEKERES Problem1Meijing ShanInstitute of Information science and Technology,East China University of Political Science and Law, Shanghai, China. 201620Keywords: Erdös-Szekeres problem, Automated deduction, Mechanical provingAbstract:The Erdös-Szekeres problem was an open unsolved problem in computational geometry and related fields from 1935. Many results about it have been shown. The main concern of this paper is not only show how to prove this problem with automated deduction methods and tools but also contribute to the significance of automated theorem proving in mathematics using advanced computing technology. The present case is engaged in contributing to prove or disprove this conjecture and then solve this problem. The key advantage of our method is to utilize the mechanical proving instead of the traditional proof and this method could improve the arithmetic efficiency.IntroductionThe following famous problem has attracted more and more attention of many mathematicians [3, 6, 12, 16] due to its beauty and elementary character. Finding the exact value of N(n) turns out to be a very challenging problem. The problem is very easy to explain and understand.The Erdös-Szekeres Problem 1.1 [4, 15]. For any integer n ≥ 3, determine the smallest positive integer N(n) such that any set of at least N(n) points in generalposition in the plane contains n points that are the vertices of a convex n-gon.A set of points in the plane is said to be in the general position if it contains no three points on a line. This problem was also called Happy Ending Problem by Erdös, because two investigators Esther Klein and George Szekeres who first worked on the problem became engaged and subsequently married[8, 17].The interest of Erdös and Szekeres in this problem was initiated by Esther Klein(later Mrs. Szekeres), who observed that from 5 points of the plane of which no three lie on the same straight line it is always possible to select 4 points determining convex quadrilateral. There are three distinct types of five points in the plane, as shown in Figure 1.Figure 1. Three cases for 5 points.In any case of the Figure 1, one can find at least one convex quadrilateral determined by the points. Klein [4] suggested the following more general problem: Can we find for a given n a number N(n) such that from any set containing at least N points it is possible to select n points forming a convex polygon?As observed by Erdös and Szederes [4], there are two particular questions:(1) Does the number N corresponding to n exist?(2) If so, how is the least N(n) determined as a function of n?1T his work was financially supported by Humanity and Social Science Youth foundation of Ministry of Education of China (No. 14YJCZH020).They proved the existence of the number N(n) by two different methods. The first one is a combinatorial theorem of Ramsey. The foundation of the second one isbased on some geometrical and combinatorial considerations. And then they formulated the following conjecture.Conjecture 1.1 N (n ) = 2n −2 + 1 for all n ≥ 3.Despite its elementary characters and the efforts of many researchers, the ErdösSzekeres problem is solved for the value n = 3, 4 and 5 only. The case n = 3 istrivial, and n = 4 is due to Klein. The equality N (5) = 9 was proved by E. Makaiwhile the published proof by Kalbfleisch [11] and then Bonnice [2] and Lovasz [13]independently published the much simpler proofs. The bottle neck of this problem now is when n >5, how to prove or disprove the conjecture.About this problem, the best currently known bounds are(1)Where is a binomial coefficient. The lower bound was obtained by Erdös andSzekeres [4] and the upper bound is due to Töth and Valtr [18]. The lower bound issupposed to be sharp, according to conjecture 1.1.In this paper we use the automated deduction method and tools [1, 19-21] to establish a mechanical method for proving problem instead of the manual proof. We hope the method might give a rise to substantially promote this unsolved problem.The rest content of the paper is indicated by section headings as follows: Section 2 preliminaries, Section 3 main results, Section 4 conclusion and remarks.PreliminariesIn this Section, we present some algorithms that would help us develop our method in next section.Algorithm 2.1. Modified Cylindrical Algebraic Decomposition (CAD). Due to the problem statement, the proof should consider all kinds of points’ positions on the plane.The Cylindrical Algebraic Decomposition [5, 14] of R n adapted to a set ofpolynomials which is a partition of R d is cells (simple connected subsets of R d )such that each input polynomial has a constant sign on each cell. Basically, thealgorithm computes recursively at least one point in each cell (so that one can testthe cells that verify a fixed sign condition). The sample points Pi got by originalCAD are always more than one on each cell. We modify the procedure to have asample point on each cell of the final cell decomposition, by the rule that Pi has a constant sign on each cell. We elaborate the main idea under lying our method by showing how our main algorithm evolved from the original one.Here, we describe it as follows.Algorithm. MCADInput: A set F of polynomialsOutput: A F-sign-invariant CAD of R nStep 1. Projection. Compute the projection polynomials which using exclusivelyoperations, and receive some (n − 1) -variate polynomials.Step 2. Recur. Apply the algorithm recursively to compute a CAD of R n −1which Q(F )is sign-invariant.Step 3. Lifting. Lift the Q(F )-sign-invariant CAD of R n −1 up to a F-sign-invariant CAD of using the auxiliary polynomial Π(F ) of degree no largerthan d (F ) (d is the maximum degree of any polynomial in F).Step 4. Choice. Utilize the strategy that {Pi} has constant sign on each cell tochoose one sample point on each cell.Algorithm 2.2 (Graham Scan Algorithm) [9, 10, 22]We present one of the simplest algorithms used to find the convex hull fromsome points. Some basic definitions are provided in the field of Computational Geometry. This algorithm works in three phases:Input: A set S of pointsOutput: The convex hull of S.Step 1. Find an extreme point. The algorithm starts by picking a point in S known to be a vertex of the convex hull. This point is chosen to be with smallest y coordinate and guaranteed to be on the hull. If there are some points with the same smallest y coordinate, we will choose the point with largest x coordinate in them. In other words, we select the right most lowest point as the extreme point.Step 2. Sort the points. Having selected the base point which is called P0 , then the algorithm sorts the other points P in S by the increasing counter-clockwise (ccw) angle the line segment P0P makes with the x-axis. If there is a tie and two points have the same angle, discard the one that is closest to P0 .Step 3. Construct the convex hull. Build the hull by marching around the star shaped polygon, adding edges when we make a left turn, and back-tracking when we make a right turn. We end up with a star-shaped polygon, see Figure 3 (one in whichone special point, in this case the pivot, can “see” the whole polygon). Considering efficiency in Step 2, it is important to note that the comparison of sorting between two points P2 and P3 can be made without actually computing their angles. In fact, computing angles would use slow in accurate trigonometry functions, and doing these computations would be a bad mistake. Instead, one just observes that P2 would make a greater angle than P1 if (and only if) P2 lies on theleft side of the directed line segment P0P1 , see Figure 2.We make full use of this algorithm to judge whether the polygon received in every recursive step is a convex polygon or not. It is a decision method in our algorithm.To state the algorithm clearly, we will describe it in a style of pseudo-code.Algorithm. Graham Scan AlgorithmInput: A set S of points in the planeOutput: A list containing the vertex of the convex hullSelect the right most lowest point P0 in SFigure 3. Graham ScanFigure 2. Sort the points.Sort S angularly about P0 as a center.For ties, discard the closer points.Let S be the sorted array of points.Push S [1] = P0 and P1 onto a stack Ω.Let P1 = the top point on ΩLet P2 = the second top point on Ωwhile S [k ] P doif (S [k −1] is strictly left of the line S [k ] to S [k +1]), thenPush S [k −1] onto ΩelsePop the top point S [k ] off the stack Ω.fi;od;Main ResultsIn contrast with the traditional proof, this method presented following can show the convex polygons received in every step.The main idea of our algorithm: First, give randomly four points in general position in the plane, and then we use polynomials of points’ coordinates to represent the lines. We extend the 4-element set to some5-element sets. We do this by establishing the corresponding Modified Cylindrical Algebraic Decomposition (MCAD) and design an interactive program which allow the user to choose among the candidate one sample point in each cell. We use Graham Scan algorithm to determine whether or not there is a convex 5-gon (convexpentagon) in every set received. If some of the received 5-element sets have no convex 5-gon, then extend them to the 6-element sets by the strategy mentionedabove. Simultaneously, check whether or not each of the received 6-element sets has any convex hull at least with any convex 5-gon in the polygon. We implement theprogram repeatedly until can find a convex n-gon (n ≥ 5) in any set. We trace the processing of the extension and decision, and then draw a conclusion that N (5) = 9.To prove this approach, we write the following algorithm named “conv5”. Based on this algorithm can generate short and readable mechanical proving for the Erdös-Szekeres conjecture, including the case of n = 3, 4, 5. It consists of two main algorithms—Modified Cylindrical Algebraic Decomposition algorithm and Graham Scan algorithm and some sub-algorithms such as collinear, pol, sam, ponlist, min0,isleft, ord, conhull, point5, convex, G5,G6,Pmn.Algorithm Conv5Input: four points in the general position in the plane.Output: Any polygon with at least 9 points in general position in the planecontains a convex 5-gon. Step 1 [collinear]. Write the line polynomials with the given four points (basepoints).Step 2 [pol, sam, ponlist]. Illustrate how we utilize the CAD to find somesample points in the cell which built by the lines, and then with the base n points get n +1 -element sets.Step 3 [min0, isleft, conhull, point5, convex, G5]. Decide whether or not thereis a convex hull or a convex n-gon (n ≥ 5) in every set; if it is true, then stop; elsegoto Step 4.Step 4 [G6, Pmn]. Deal with the sets which have no convex n-gon (n ≥ 5).Recursively implement Step 2 and Step 3 process, until at least there is a convex 5-gon in any set. End Conv5.The key techniques of the algorithm are listed as follows:1. To reduce the complexity of the computation and increase the efficiency,when we check whether or not there is a convex 5-gon in the given points set,we utilize the strategy as follows:if there is a convex hull at least with 5 points in the points set thenpop this points setelif there is a convex 5-gon thenpop this points setelse “there is no convex 5-gon in this points set” go to next step2. Each convex n-gon (n ≥ 5) contains a convex 5-gon3. If there is no convex 4-gon, then there should be no convex 5-gon.Conclusion and RemarksBy the Maple procedure we have implemented the mechanical method for the conjecture in certain cases. Through observing the whole computational process, we obtain a certain answer that any set with at least 9 points in general position in the plane contains a convex 5-gon. This method can be generalized in an obvious way to arbitrary base points in the plane.For the mechanical method proposed here, on one hand it provided one of the promising direction for proving or disproving the Conjecture 1.1 (when n ≥ 6), even for handling with some unsolved problems in computational geometry. On the other hand, it gave one especially useful application of computer algebraic andautomated deduction. For further investigations, now we consider about the following problems:1. Does any set of at least 17 points in general position in the plane contains 6 points which are the vertices of a convex hexagon? Can we give the proof about N (6) existence and prove or disprovethe corresponding conclusion by mechanical proving? Now the best known conclusion about this is N (6) ≥ 27, if it exists.2. Erdös posed a similar problem on empty convex polygons. Whether or not we can give the automated proof to this problem?References[1] M. de Berg, M. van Kreveld, M. Overmars and O. Schwarzkopf, omputational GeometryAlgorithm and Applications, (2nd ed.), Spring-Verlag, Berlin, Heideberg, New York, 1997.[2] W. E. Bonnice, On convex polygons determined by a finie planar set, Amer. Math. Monthly.[3] F. R. K. Chung and R. L. Graham, Forced Convex n-gons in the Plane, Discr. Comput. Geom. 19(1998), 367-371.[4] P. Erdös and G. Szekeres, A combinatiorial problem in geometry, Comositio Mathematica 2(1935), 463-470.[5] E. Collins George, Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition Lecture Notes In Computer Sciencevol. 33, Springer-Verlag, Berlin, pp. 134-183.[6] Kráolyi Gyula, An Erdös-Szekeres type problem in the plane.[7] X. R. Hou and Z. B. Zeng, An efficient Algorithm for Finding Sample Points of Algebraic Decomposition of Plane, Computer Application, 1997, (in Chinese).[8] P. Hofiman, The Man Who loved Only Numbers Hyperion, New York, 1998.[9] /ah/alganim/version0/Graham.html.[10] http://cgm.cs.mcgill.ca/ beezer/cs507/main.html.[11] J. D. Kalbfleisch, J. G. Kalbfleisch and R. G. Stanton, A combinatorial problem on convexregions, Proc. Louisiana Conf. Combinatorics, Graph Theory and Computing, Louisianna StateUniv., Baton Touge, La, Congr. Numer. 1 (1970), 180-188.[12] D. Kleitman and L. Pachter, Finding convex sets among points in the plane, Discr. Comput.Geom. 19, (1998), 405-410.[13] L. Lovasz, Combinatorial Problem and Exercises North-Holland, msterdam, 1979.[14] Bhubaneswar Mishra, Algorithmic Algebra, Springer-Verlag, 2001.[15] W. Morris and V. Soltan, The Erdös-Szekeres Problem on Points in ConvexPosition- A, Survey Bulletin of the American Mathematical Society, vol. 37.[16] L. Graham Ronald and Yao Frances, Finding the Convex Hull of a SimplePolygon Report No. STAN-CS-81-887, 1998.[17] B. Schechter, My Brain is Open Simon Schuster, New York, 1998.[18] G. Tóth and P. Valtr, Note on the Erdös-Szekeres theorem, Discr. Comput. Geom. 19 (1998), 457-459.[19] W. T. Wu, Basic Principles of Mechanical Theorem Proving in Geometries Science Press,Beijing, 1984, (Part on elementary geometries, in Chinese).[20] L. Yang and B. C. Xia, Automated Deduction in Real Geometry, Geometric Computation, WorldScientific, 2004.[21] L. Yang and Z. Z. Jing and X. R. Hou, Nonlinear Algebraic Equation System and AutomatedTheorem Proving, Shanghai Scientific and Technological Education Publishing House, Shanghai,1996, (in Chinese).[22] P. D. Zhou, Computational Geometry Design and Analysis in Chinese, TsingHua UniversityPress, 2005.。