本科毕业设计（论文）
外文翻译
使用符号与数字的结合推理解决几何问题
作者：沙查尔·伊扎基[1]、苏米特·古尔瓦尼[2]、尼尔·伊梅尔马[3]和穆利·萨吉夫[1]
国籍：[1]以色列特拉维夫大学
[2]美国华盛顿州雷蒙德微软研究院
[3]美国马萨诸塞州阿默斯特大学
出处：爱学术网站，由温桂荣上传https://www.ixueshu.com/document/3b78b474e3bf1ca4318947a18e7f9386.html#correlation
摘要：我们描述了一个框架，它结合了演绎推理、数值推理和归纳推理来解决几何问题。应用程序包括生成几何模型和动画，以及在智能辅导系统环境中解决问题。
我们的新方法使用（i）演绎推理从逻辑约束生成一个部分程序，（ii）数值方法来评估部分程序，从而创建几何模型来解决原始问题，（iii）归纳合成，读取新的约束，然后应用到一轮演绎中。导致期望的确定性程序的推理。通过各种方法的结合，我们能够解决每一种方法本身无法解决的问题。
部分计划中非确定性选择的数量提供了一个衡量问题解决的程度的指标，因此可以在教育环境中用于评分和提供提示。
我们已经成功地评估了我们的方法论，包括18个学术能力倾向测试几何问题和11个基于标尺/罗盘的几何结构问题。我们的工具用平均几秒钟的时间解决了这些问题。
关键词：几何；推理；综合
1 引言
我们描述了一个解决几何问题的框架，它被指定为输入、输出和它们之间的约束的元组。几何问题的完美解决方案包括一个构造性的模型生成过程，并证明其正确性。当输入点移动时，合成过程允许在交互环境中实时构建模型-这在动态几何环境[WCY05]和动画中都有应用程序。
这类问题是CLP（R）[JMSY92]的一个子集——带有实数变量的约束逻辑编程。目前prolog中CLP（R）的实现对非线性约束的支持有限[swi]。Gr–Obner Base提出了一种解决直尺和罗盘构造问题的技术，但这种技术依赖于使用多项式表示约束[buc98]。对于我们的目标域来说，这是不够的，因为问题通常包含角度和长度形式的数字数据，需要使用三角法。
我们的求解器首先使用符号和数字推理的组合构造满足约束的输入和输出模型。为了弥合这两种技术之间的差距，我们使用了部分程序的概念。部分程序是包含“choice”语句的程序，这意味着某些输出对象需要从某些loci中以非确定性方式选择。为了在实际应用中对这些程序进行评估，我们使用数值方法来最小化非负函数，当满足相关约束条件时，该非负函数的值为0。这些方法通常在维度数量较低（最多2个）时表现良好，因此在减少搜索维度方面投入了相当大的精力。更具体地说，解算器有一个内置的几何定理知识库，作为一组数据记录规则编写。在给定输入问题规范的情况下，该算法尝试识别较小的搜索空间，并将问题分解为单个低维搜索调用。一旦找到所有输出对象，我们就可以解决给定的问题。构造实例足以解决SAT考试等几何问题（这通常需要计算一些数量的值，如长度、角度、面积等，这些值可以从模型中读取）。
也许更有趣的是，解算器从以下两个方面超越了模型的构造。首先，如果构建模型需要数值推理，那么求解器会尝试消除这种需求，以减少运行时间。该过程的工作原理如下：它为另一个问题的实例构造了第二个模型，在这个问题中输入的位置受到了扰动。解算器接下来搜索两个构造模型中出现的距离和角度之间的相等性，但在输入规范中没有提到。根据[hon86，gkt11]所示的定理，这些等式是偶然的概率接近于零。解算器将这些新的等式添加到输入约束中，并解决新的问题。这种数字搜索的消除产生了一个更有效的程序，使得对同一问题的实例的未来评估更快。对于给定问题的一个实例，我们指的是具有不同输入值的相同约束（例如，不同长度的段或点的位置）。此外，生成的程序提供了一个完整的、构造性的解决方案，而不是数值近似。第二，一旦合成了一个确定性程序，我们的求解器就会生成一个证明程序总是构造一个满足约束的模型。从而自动证明了该结构的正确性。我们认为一个整体程序是一个给定几何问题的完美解决方案，而一个局部程序则寻找答案。搜索空间的维度提供了对搜索运行时成本的估计。
将来，我们计划使用几何解算器作为几何学生的助手和导师。上述部分课程的指标将有助于衡量学生与解决方案之间的距离，以及衡量学生帮助他们解决给定问题所需的“提示大小”。
本文的主要贡献如下：
1. 我们的几何程序解算器展示了我们如何结合符号、数字和归纳推理的互补优势。
2. 我们介绍了一种非确定性的部分程序语言，用于获取有关几何结构的部分见解。这类程序的基本成本与必须用数字搜索的位置的大小和数量相对应。这种语言对于解决方案的中间数据结构和用户交流见解都很有用。
3. 我们提供了一个实质性的实验评估，证明了我们的解决方案的有效性。在网上免费提供的SAT实践测试中的21个问题中，我们能够自动解决18个问题。我们唯一无法解决的问题是，当问题的大小是输入或输出的一部分时（例如，当要求用户确定给定多边形的边数时）。在我们测试的6个问题中，解算器能够消除所有的数字搜索步骤，从而合成一个非常有效的程序来解决给定问题的一般版本。
在下文中,我们定义我们考虑的几何问题的格式。我们详细介绍了解算器。最后,我们报告我们的实验结果。
2 几何构造问题
我们首先描述如何指定几何构造问题。我们还定义了该问题解决方案的三个组成部分，即模型、绘图程序和程序正确性的证明。
同样的形式也适用于问题的另一个子类，我们称之为测量问题，学生需要计算一些值，例如角度或面积。
问题说明；几何构造问题是一个约束满足问题，由一组变量v和一组约束c组成。每个变量visin;v表示实数、点、线或圆。对于纯构造问题，变量分为输入变量i（与问题一起考虑）和输出变量o（待构造）。
对于测量问题，输入和输出之间的区别并不显著；相反，给出了一组查询表达式Q，并且输出是每个此类术语的一个数值。
解决方案；解决方案由模型、绘图程序和正确性证明组成。模型是对满足所有约束条件C的变量的赋值。绘图程序是一个计算序列。证明该程序对满足其约束条件的所有输入都是正确的。
3 部分程序
我们现在描述部分程序的语言，它结合了命令式和声明式构造。解算器的第一个主要步骤是构建用于构建所需模型的部分程序。
部分程序是一系列指令。有些构造步骤需要进行数字搜索以查找相关对象。部分程序的语言由图1所示的BNF语法定义。该方案是通用的，从某种意义上说，它允许域特定的谓词和函数符号，在语法中分别用P和F表示。
|
程序 |
S |
::= |
A1;...;An; |
||
|
陈述 |
A |
::= |
v := F(v1,...,vn) | p :isin; R |
定义 ϕ |
|
|
范围 |
R |
::= |
G(v1,...,vn) | R1 cap; R2 |
||
|
约束 |
ϕ |
::= |
gamma;1 and; .. and; gamma;n |
||
|
元组 |
gamma; |
::= |
P(v1,...,vn) |
表1用于部分程序的一种语言。
对于几何图形，我们使用表1中所示的一组符号。这些谓词和函数对于二维欧几里德几何来说是非常自然的。函数行（`）、ray（p，）、segment（a，b）、circle（p，r）和disc（p，r）是原始函数，从系统内部识别的意义上讲，它们只是逻辑推理规则中使用的名称（见下文4.1）。为了将框架重新定位到另一个领域，例如三维空间，设计师可以引入其他符号，但对这一点的讨论超出了本文的范围。
直观地讲，读者可能会发现，将部分程序看作是对问题的部分洞察的表示，这是一种解决问题的算法，但有一些“漏洞”。
例1:一个简单的部分程序。
1: a := h0,0i // a是原点
2: b :isin; circle(a,10) // b位于给定中心、半径的圆上
3: c := Middle(a,b) // c为AB段中点
4: Assert c.y = 4 // c的y值为4
此程序查找距离原点10的点B，这样，从原点到B的直线段的中点在X轴上方的高度为4。
前三个语句为要查找的对象指定一个可能的值范围（在本例中，这三个点是A、B和C），定义指定一个约束。定义不同于赋值，因为它约束已赋值对象的属性。
为了评估这个程序，我们应该在原点周围半径为10的圆上搜索B点，这样C.Y=4就可以了。
程序变量和函数是类型化的，并且分配必须是正确类型化的。因此，在语句v：=f（v1，..，vn）中，如果v的类型是t，那么f应该是返回t类型对象的函数，在语句v：isin;g（v1，..，vn）中，g应该返回一个集合s t。例如，如果v是一个点（t=r2），我们要求g（v1，..，vn）r2。
assert语句对上述范围内提供但尚未修复的变量启动数值搜索。成功完成搜索后，将为其中一些变量指定固定值。每一个约束都被转换成数字要求，一些必然的非负值被最小化。例如，约束c.y=4转换为“最小化（c.y-4）2”。
表1。几何用函数符号和谓词符号
|
圆(O,r)是以O为中心半径r的圆,线(A,B)穿过A和B，射线(A,B)线,其原点为A射线,通过B，射线(A,u)其原点为A且带有u方向的射线, (A,B) 线段是连接A和B的直线段。 Dist(A,B) 点A和点B之间的距离 ang;(A,B,C) (较小)角度 ang;ABC ang;ccw(A,B,C) 角 ang;ABC, 逆时针测量 Middle(A,B) 段 AB 圆周 (R) 的中点_ ArcDist(O,A,B) 以 O 为中心的圆弧 AB 的长度 Diameter(R,AB) 真正的 iff AB 是圆 R 中的直径 IntersectSegments(A,B,C,D) 真iff AB相交CD Colinear(A,B,C) 真iff A、B和C在同一条线上 |
运行示例，第一部分部分程序生成规则六边形。
下面的部分程序生成一个规则的六边形abcdef给定边ab。它首先选择ab的垂直平分线上的点o。然后它绘制c，使cob与aob形成相同的角度，oc=ob。接下来绘制D，
剩余内容已隐藏，支付完成后下载完整资料
Solving Geometry Problems using a
Combination of Symbolic and Numerical
Reasoning
Shachar Itzhaky1, Sumit Gulwani2, Neil Immerman3, and Mooly Sagiv1
1 Tel Aviv University, Israel
2
Microsoft Research, Redmond, WA, USA
3
University of Massachusetts, Amherst, MA, USA
Abstract. We describe a framework that combines deductive, numeric, and inductive reasoning to solve geometric problems. Applications include the generation of geometric models and animations, as well as problem solving in the context of intelligent tutoring systems.
Our novel methodology uses (i) deductive reasoning to generate a partial program from logical constraints, (ii) numerical methods to evaluate the partial program, thus creating geometric models which are solutions to the original problem, and (iii) inductive synthesis to read off new constraints that are then applied to one more round of deductive reasoning leading to the desired deterministic program. By the combination of methods we were able to solve problems that each of the methods was not able to solve by itself.
The number of nondeterministic choices in a partial program provides a measure of how close a problem is to being solved and can thus be used in the educational context for grading and providing hints.
We have successfully evaluated our methodology on 18 Scholastic Aptitude Test geometry problems, and 11 ruler/compass-based geometry construction problems. Our tool solved these problems using an average of a few seconds per problem.
Keywords: geometry, reasoning, synthesis
1 Introduction
We describe a framework for solving geometry problems, which are specified as a
tuple of inputs, outputs, and constraints between them. The perfect solution to a geometry problem consists of a constructive model generation procedure along with a proof of its correctness. The synthesized procedure can allow models to be constructed in real time, within an interactive environment, as the input points are moved — this has applications in both dynamic geometry environments [WCY05] and animations.
This class of problems is a subset of CLP(R) [JMSY92] — Constraint Logic Programming with Real variables. Current implementation of CLP(R) in Prolog has limited support for non-linear constraints [swi]. Gruml;obner bases suggest a technique for solving ruler-and-compass construction problems, but this technique relies on expressing the constraints using polynomials [Buc98]. This is insufficient for our target domain, since problems typically contain numerical data in the form of both angles and length, requiring some use of trigonometry.
Our solver starts out by constructing a model of inputs and outputs that satisfy the constraints using a combination of symbolic and numeric reasoning. To bridge the gap between the two techniques, we use the notion of partial programs. A partial program is one that contains “choice” statements, meaning that certain output objects need to be chosen nondeterministically from certain loci. To evaluate these programs in practice, we use numerical methods for minimizing a non-negative function that has the value 0 iff the relevant constraints are met. These methods typically perform well when the number of dimensions is low (up to 2), so a considerable effort is invested in decreasing the search dimension. More specifically, the solver has a built-in knowledge base of geometric theorems, written as a set of Datalog rules. Given an input problem specification, the algorithm tries to identify small search spaces and splits the problem into individual search invocations of low dimension. Once all the output objects are found we have a solution to the given problem. Constructing the instance suffices to solve geometry problems from SAT exams, etc. (This typically requires computing the value of some quantity such as length, angle, area, etc, which can be read off from the model).
Perhaps more interestingly, the solver goes beyond the construction of the model in the following two ways. First, if numeric reasoning was required to constructing the model, then the solver attempts to eliminate this need in an attempt to decrease running time. The procedure works as follows: it constructs a second model for another instance of the problem in which the positions of the inputs have been perturbed. The solver next searches for equalities between distances and angles that occur in both of the constructed models, but were not mentioned in the input specification. According to theorems shown in [Hon86,GKT11], the probability that such equalities are incidental approaches zero. The solver adds these new equalities to the input constraints and solves the new problem. This elimination of numeric search produces a more efficient program, making future evaluations of instance of the same problem much faster. By an instance of a given problem we mean the same constraints with different values for the inputs (e.g. different lengths of segments or positions of points). Furthermore, the resulting program provides a complete, constructive solution rather than a numeric approximation. Second, once a deterministic program has been synthesized, our solver generates a proof that the program always constructs a model satisfying the constraints. Thus the correctness of the construction is automatically proved. We view a total program as a perfect solution for a given geometric problem, whereas a partial program searches for the answer. The dimension of the search spaces provides an estimation for the run-time cost of the search.
In the future we plan to use our geometric solver as a helper and tutor for geometry students. The above metric for partial programs will be useful for measuring how far a student is from a
剩余内容已隐藏，支付完成后下载完整资料
资料编号：[272288]，资料为PDF文档或Word文档，PDF文档可免费转换为Word
以上是毕业论文外文翻译，课题毕业论文、任务书、文献综述、开题报告、程序设计、图纸设计等资料可联系客服协助查找。
