→∈理论计算机科学电子笔记36（2000）网址：http://www.elsevier.nl/locate/entcs/volume36.html共210页规则系统ELAN克里斯托夫·林盖森洛里亚-因里亚615rueduJardinBotanique，BP101，F-54602Villers-l`es-NancyCedex，France电子邮件：Christophe. loria.fr摘要我们提出了一种在基于规则的编程语言ELAN中有效处理小有限域上关系的方法。通常，关系被指定为在给定代数结构中解释的一阶公式（约束）。重写的概念允许我们以一种非常优雅的方式实现一个代数结构，通过使用定义运算符和谓词的规则。因此，我们可以直接获得一个基于规则的可执行规范来计算一个关系的所有元组，但在大多数情况下，相关的计算是完全无效的。事实上，关系的指定涉及条件规则，并且许多重写步骤在尝试后失败。在本文中，我们使用有限代数中的约束求解器将关系的朴素的基于规则的ELAN规范转换为仅具有无条件规则的高效的基于规则的ELAN因此，约束求解器使我们能够提高基于规则的计算的关系。1介绍在基于规则的编程语言[16 ，4，12，14]中，程序是术语重写系统（TRS），涉及由规则定义的函数给定一个由连续和终止TRS定义的函数，基于规则的系统允许我们计算任何元素（查询）的唯一图像（结果）。在这项工作中，我们也有兴趣在基于规则的编程关系。显然，函数和关系之间没有真正的区别。因此，m元函数f：D mD是D 上 的（m +1）元关系（即，Dm+1），使得连续t和终止TRS计算结果f（d→）foranyqueryd→Dm，还计算该关系的一个元素nt（d→，f（d→））。相反，域D上的任意m元关系R可以被视为：一个函数fR：Dm→bool，使得d→∈Dm在Rif中且仅ifR（d→）是真的然后，一个连续的和终止的TRS计算fR允许决定Dm的一个元组是否在关系R中。2000年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。林盖森2在本文中，我们对计算一个关系的一个元组不感兴趣，或者决定一个元组是否在一个关系中。相反，我们感兴趣的是（有效地）计算一个关系的所有元组。对于这个问题，仅仅有连续的TRS是不够的，能够处理非连续的TRS是非常有趣的，因为它面对的是一个关系的所有元组的生成所导致的非确定性。在这种情况下，我们的想法是使用基于规则的语言集成确定性和非确定性的计算，使用re-concurrence和non-concurrence的TRS。一个可能的例子是ELAN，在这种情况下，只要定义了控制规则应用的策略，就可以对非连续TRS进行编程。使用这种策略获得的范式（在我们的例子中，是关系的元组）是通过类似Prolog系统的回溯机制收集的。我们在本文中报告了如何使用基于规则的系统（如ELAN[17，4]）处理函数和关系（也称为约束），当域D被假设为有限时。特别是，我们感兴趣的是在一个给定的关系中使用的所有元组的生成策略。我们的主要贡献是展示了有限代数中现有约束求解器的兴趣[7，21]。事实上，这个求解器对于简化我们要计算的关系非常有用这种简化是通过使用求解器计算的最一般的解来实现的，这实际上是关系的参数化。参数化由一个函数元组给出，该函数元组由直接从约束求解器中实现的内部数据结构[5]中提取的重写规则定义。因此，约束求解器可以在编译时使用，作为一种方法，以获得一个高效的基于规则的计算的关系，最初指定的代数方式。这种关系的基于规则的描述包括一组确定性的计算规则的参数化的功能，加上一个单一的非确定性规则的参数化本身。然后，这段代码在任何基于规则的程序建模中都是有用的，其中涉及关系。有限域上的约束和关系对于多值逻辑中指定的复杂系统（如电子元件）的原型设计和检查最感兴趣[6，8]。本文的组织结构如下。在第二节中，我们简要介绍了基于规则的系统ELAN。第3节介绍了几种方法来编码关系在ELAN中，无论是通过扩展，或通过内涵使用代数结构中表示的约束。 最后，我们用一个例子来激励我们基于关系参数化的方法。在第4节中，我们展示了如何使用有限代数中的约束求解器获得的项来构造关系的参数化。这些条款进行评估后，instantiation的变量，根据规则指定一个功能完备代数。在第5节中，我们展示了另一种更好的参数化，它使用函数而不是项。这些函数的基于规则的描述直接从约束求解器中实现的内部数据结构中提取。第6节讨论了这种方法的不同可能应用。最后，我们在第7节中总结了未来的工作。林盖森3→×···×›→\2基于规则的系统ELAN我们假设读者熟悉基于规则的编程语言，例如ELAN。在本文的其余部分，一个类似ELAN的语法被用来呈现基于规则的程序的例子。这些基于规则的程序中的每一个都由一个多排序的签名和一组规则组成，这些规则涉及在该签名上构建的术语。在此语法中，多排序运算符声明f：s1s ns如下给出：f（@，...，@）：（s1. s n）s，其中s1，.， sn，s是排序符号，@表示占位符。 对于算子符号f，我们可以关联多个运算符声明，这意味着ELAN允许运算符重载。给定一组操作符声明，现在可以定义重写规则。相同排序s的两个项l和r之间的（全局）重写规则l r写为如下：s的规则V ar（r）V ar（l）全球[R]l=>r end end让我们详细说明这一规则的不同组成部分。局部变量在规则体中声明在关键字global（或local）之前，用于设置规则/声明的可见性。标识符R随附by []括号是（可选）规则标签。右边的r包含一个可能包含局部变量的项，加上一个条件列表（if@）和赋值（其中@：=@），将按照给定的顺序进行计算。if的参数是内置sortbool的一个项。如果该项不能还原为真，则规则应用失败。where构造有两个参数：• 第一个参数是一个项，假设p，包含将通过匹配分配的局部变量。• 第二个参数对应于应用于术语的策略，它将返回一个（有限）术语集。项p将通过回溯机制连续地匹配这些项中的每一项。如果术语集为空，则无法为规则构建右侧，并且规则应用程序失败。最后，局部变量被映射到基项，因此它们可以在r项中被替换，以便获得规则应用的结果我们用表示策略表达式处理项的排序的sorts。sort的策略表达式可以由规则us定义-内置的策略语言。我们在论文中使用的独特的内置构造是dk（R），它计算由R标记的规则的应用（在最顶部位置）产生的所有项。为了执行确定性计算，我们还使用了内置的空策略（），它通过使用最左-最内策略来应用未标记的规则按照命令，林盖森4∈如果给定了哪些未标记的规则，ELAN会尝试这些未标记的规则中的每一个，并应用第一个适用的规则。通常，未标记的规则集被假设为一个连续的和终止的TRS，因此应用顺序并不重要。3基于规则的关系编码3.1成员关系让我们首先考虑最基本的关系，即一元关系XD。对于这个关系，我们定义一个常数算子，假设D是dom类的，以及一个策略inD，使得（inD）应用于项D的标准形式都是D的dom类元素。这可以很容易地在ELAN中编码如下：operatorsglobalD：dom;d1：dom;...dn：dom;enddomglobal[genD]D =>d1 end的规则...[genD] D =>dn endendglobal[]inD=> dk（genD）endend然后，这个关系可以用来定义像这样的非确定性函数：实施例3.1domY：dom;global的规则[addRule]add（X）=>X+Y其中Y：=（inD）Dend端使用此定义，（dk（addRule））add（x）计算集合{x + d|d ∈D}。林盖森5∈--{1}|}3.2关系的外延定义对于任意m元关系R，我们可以类似于前面的情况使用常数算子R和策略算子inR，使得（inR）R枚举所有项R（d→），其中d→R. 现在，我们可以选择将Rin的元组封装到m元运算符R（. . ）.例3.2例如考虑域D= 0， 1， 2和D 2上的二元关系GT（0：dom;1：dom;2：dom;GT：rel;GT（@，@）：（domdom）rel;endrelglobal[genGT]GT=> GT（1，0）end [genGT]GT=> GT（2，0）end[genGT]GT=> GT（2，1）end的规则端rel> global[] inGT => dk（genGT）end end的规则然后，可以使用常数算子R和策略算子inR 在if/where部分规则中。例3.3GT关系允许我们定义以下非确定性规则：domY：dom;global的规则[gtRule] gt（X）=>Y其中GT（Y，X）：=（inGT）GT end端（dk（gtRule））gt（x）的正规形式是y GT（y，x）的元素。使用关系作为where部分的模式（“左手边”）是非常方便的因此，非确定性函数gt可以以非常自然的方式定义。到目前为止，我们只看到了广义上的关系。使用这种方法，缺点是关系的每个元组都需要一个带标签的规则。对于一个显著大小的关系，这会导致一个程序有太多的标记规则，这很难被基于规则的系统处理3.3关系的内涵定义通常，将关系定义为用约束语言表示的约束要方便得多，在约束语言中，变量映射为值，林盖森6--运算符和谓词以一阶代数结构解释。运算符和谓词的解释可以通过计算规则来实现，而变量的分配可以通过成员关系来执行例3.4考虑域D= 0， 1， 2和D 2上的二元关系GEQ （“大于或等于”），它可以在ELAN中具体实现如下：0：dom;1：dom;2：dom;@>@：（dom dom）bool;GEQ：rel;GEQ（@，@）：（domdom）rel;end//解释>bool的规则X，Y：dom;全局[]1>0 => trueend[]2>0 => trueend[]2>1 => trueend[]X>Y =>false end//否则endrelX，Y：dom;global的规则[genGEQ] GEQ => GEQ（X，Y）其中X：=（inD）D其中Y：=（inD） D，如果 X>Y或X==Y结束端rel> global的规则[]inGEQ => dk（genGEQ）end end内涵定义的一般形式如下：相关规则X1，...，Xm：dom;全球林盖森7∗F=XYK=！我∃[genR]R=>R（X1，.， X m）其中X1：=（inD）D...其中，如果 R（X1，...， X m）端端规则rel>global[] inR =>dk（genR）end end现在，主要的优点是我们只有一个标签规则。相反，这个规则是有条件的。因此，将尝试为Dm中的任何元组构造右手边。如果这个条件的计算涉及到很多局部（辅助）变量，那么它就会变得非常有问题。3.4我们的方法：从规范到计算为了说明我们的方法，让我们考虑一个内涵定义的关系通过使用二元布尔代数中的约束，其中与、或、非运算符分别表示为+和！。这种关系对应于一个“电子”门[15]，它被定义为和/或非元素门的组合：E、F、G、H、I、J、K、L、M、N、O、P：快！X=G快！Y=EI=G+FH=E+FGate（X，Y，A，B）门 （X，Y，A，B）HM=K+FJ=J+F*O=L+MP=！KN=！JA.A.=POB=N基本门的输出由辅助变量表示，林盖森8这是存在性量化的。 这种关系可以简单地具体化为：ELAN如下：相关规则X，Y，A，B，E，F，G，H，I，J，K，L，M，N，O，P：dom;全球[genGate] Gate => Gate（X，Y，A，B）如果！X == G还有！Y == E和F == X*YI= G+F哪里X ：=（单位D）D和H == E+F哪里Y ：=（单位D）D和K == ！我哪里一 ：=（单位D）D和J == ！H哪里B ：=（单位D）D和M == K+F哪里E ：=（单位D）D和L == J+F哪里F ：=（单位D）D和O == L+M哪里G ：=（单位D）D和P == ！K哪里H ：=（单位D）D和N == ！J哪里 我：=（单位D）D和一 == P*O哪里 J ：=（单位D）D和B == N*O其中K：=（inD）D ， 其 中L ： =（ inD ） D， 其 中M：=（inD） D端端其中N：=（inD）D ， 其 中 O ： =（ inD ） D ， 其 中P：=（inD）Drel> global的规则[]inGate => dk（genGate）endend这个定义直接对应于门的具体化。然而，这种基于规则的编码太天真了，而且完全不明智。有太多的变量（16），ELAN系统将试图计算216右侧，当然有很多冗余。但是读者可以注意到，在这种特殊情况下，指定Gate的等式系统可以通过替换存在性量化变量来转换为求解形式。此外，除了X和Y，所林盖森9有其他变量都是唯一定义的。因此，Gate可以计算如下：RelX，Y，A，B，E，F，G，H，I，J，K，L，M，N，O，P的规则：dom;全球[genGate] Gate => Gate（X，Y，A，B）其中X：=（inD）D其中Y：=（inD）D其中G：=（）！X其中E：=（）！Y其中F：=（）X*Y其中I：=（）G+F其中H：=（）E+F其中K：=（）！我其中J：=（）！H其中M：=（）K+F其中L：=（）J+F其中O：=（）L+M其中P：=（）！K其中N =（）！J林盖森10端其中A：=（）P*O，其中B：=（）N*O端我们的方法导致以下等效程序，这是更从计算的角度来看是有吸引力的RelY1，Y2的规则：dom;global[genGate] Gate => Gate（Y1，Y2，Y2，Y1）其中Y1：=（inD）D ， 其 中Y2 ： =（inD） D结束端上述规则中Gate的参数化直接从有限代数中约束求解器返回的最一般解中获得。 它允许我们避免使用条件。因此，右边的建设永远不会失败.此外，辅助变量的数量可以最小化。读者可以检查新规则生成的关系是否与指定的关系相同，这要归功于等式约束。现在可以清楚地看到，Gate是一个非常简单的如果不解决指定门的约束，这是不容易检测到的。4按术语给定约束R（X1，...，X m）（非空关系），有限代数中的约束求解器计算唯一的方程组X1=t1···Xm=tm使得R（X1，.，X m）X1= t1· · ·X m= t m术语t1，…，t m用于建立R的以下参数定义，它等价于3.3节中给出的内涵定义。相关规则X1，...，Xm：dom;Y1， . ，Yr：dom;全球[genR]R=>R（X1，.， X m）其中Y1：=（inD）D...林盖森11其中Y r：=（inD）D其中X1：=（）t1（Y1，.，Y（r）...其中X m：=（）t m（Y1，.，Y（r）端端规则rel>global[] inR =>dk（genR）end end术语t1，…，t m包含一些新的（局部）变量Y1，...，Y r与关系中最初出现的变量集不同。新变量Y1，...，Y r是最小的整数，使得n r≥|R|.为了简单起见，我们还考虑变量X1，...，X m，其值通过计算项t1，.，在实例化变量Y1，...，Y r由D中的值。但是，我们也可以得到变量X1，...，通过考虑R（ t1，...，t m）作为右手边。现在让我们详细说明用于构建项t1，...， t m。它是[7，19]中定义的函数完备有限代数的签名，具有两个二元算子+和，以及一元算子1Cd，对于每个d∈D：operatorsglobalBot：domaliasd1：;...// DTop的元素：dom别名dn：; @+@：（dom dom）dom; @*@：（dom dom）dom; C_@（@）：（dom dom）dom;dom X，Y的规则：dom;global[]X+Y=> X如果 X>Y结束[]X+Y=> Yend//否则（X =Y）[]X*Y=> Xif X Yend[]X*Y=> Y端//否则（X>=Y）[]C_X（X）=>顶端[]C_Y（X）=> Bot endend end上面定义的函数完备代数使我们能够用一个包含（至多）r个变量的项tk来表示任何函数Fk：Dr→D1一元运算符Cd论点林盖森120112110∃2例4.1让我们考虑下面的电子门[7]：S.K.，S：B=A A组B组S =B B组Xor（A，B，X）异或S=！KB+KSX=！SK=！一约束求解器计算以下最一般的解：A=Y1B=Y2X=C（Y）然后，我们使用这个最一般的解决方案来构建生成关系的ELAN程序关系A，B，X的规则：dom;Y1，Y2：dom;global[genXor] Xor => Xor（A，B，X）其中Y1：=（inD）D其中Y2：=（inD）D其中A：=（）Y1其中B：=（）Y2式中X=C_0（Y1）*C_1（Y2）+C_1（Y1）*C_0（Y2）端端rel> global的规则[]inXor => dk（genXor）end end使用这种方法，当局部变量由值实例化时，术语通常是巨大的，并且仍然需要解释。 这可能导致 一个右边很大的带标签的规则。此外，术语是从内部数据结构实现函数自动导出的。这种数据结构，也称为DAG，是二进制决策图[5]（BDD）的直接扩展DAG的主要优点上述两个缺点在下面的方法中消失了。S =！BK+BS林盖森135函数参数化术语t1，…，在第4节中使用的t m是函数F1，.，F m由DAG的d 1在内部实现，...，dm。这些函数可以通过使用DAG的计算规则直接定义。加上F1的计算规则， F m，我们将考虑以下生成规则：相关规则X1，...，Xm：dom;Y1， . ，Yr：dom;全球[genR]R=>R（X1，.， X m）其中Y1：=（inD）D...其中Y r：=（inD）D其中X1：=（）F1（Y1，.，Y（r）...其中，X m：= （）F m（Y1，.，Y（r）端端为了解释F1的计算规则的构造，...，首先，让我们考虑一些关于DAG的符号。定义5.1 DAG d由两种节点组成，即顶点和叶子。DAG d的根由Root（d）表示。的集合（分别为叶）由V er（d）（resp. Lea（d））。一个顶点v由一个整数id（v）标识，即id：V er（d）→N是单射的。一个顶点v有一个元数n，这意味着它有n个儿子，记为v1，...，v;一个叶子的arity为0，这意味着它没有后代。叶或顶点v的元数记为ar（v）。 叶v由D的值标记，表示为lab（v）。 顶点v由一个变量标记，表示为lab（v）。以v为根的DAG的顶点的标签出现的变量的有序列表由args（v）表示。如果v是叶子，这个列表是空的表示变量的顶点是由顶点（Y）表示的顶点V，使得其标签是Y，并且对于每个i = 1，.，第i个子是标记为di的叶子。与DAG d相关联的重写规则为：GenRules（d）：=v∈Ver（d）GenRules V er（v）其中GenRules V er（v）是与d的顶点v相关联的规则nGenRules V er（v）：=i=1{[]fid（v）（di，tail（args（v）=>Rhs（vi）end}林盖森1410其中tail（l）是列表l的尾部，Rhs（v）是与顶点v相关联的右侧：• Rhs（v）：=lab（v），如果ar（v）= 0;• Rhs（v）：=Y，如果v=顶点（Y）;• Rhs（v）：=fi d（v）（a rgs（v）），否则。注5.2需要注意的是，函数fid（v）是通过第一个参数的模式匹配定义的。对于每个k = 1，...，m，函数F k对应于fid（Root（dk））。命题5.3给定DAG d，集合GenRules（d）是计算由d表示的函数的连续和终止TRS。 GenRules（d）的计算在d的大小上是线性的（其中d的大小是|Ver（d）|）.实施例5.4（续实施例4.1）。Xor的最一般解决方案的DAGd（A）=Y10R01tzd（B）=Y20rtz0 1d（X）=Y1Y21 10J，stzY20zJ0 1给定这些DAG运算符全局F3（@，@）：（dom dom）dom;F3-2（@）：（dom）dom;域Y1，Y2的规则：dom;全局[]F3（0，Y2）=>Y2end[]F3（1，Y2）=> F3-2（Y2）end[]F3-2（0）=> 1end[]F3-2（1）=> 0结束端相关规则A，B，X：dom;11林盖森15Y 1，Y 2：d o m;全局[genXor] Xor => Xor（A，B，X）其中Y1：=（inD）D其中Y2：=（inD）D其中A：=（）Y1其中B：=（）Y2其中X：=（）F3（Y1，Y2）端端rel> global的规则[]inXor => dk（genXor）end end使用这种方法，我们只有一个标记规则和许多未标记规则。这对于效率问题来说非常有趣，因为ELAN编译器[23，20]对未标记的规则比标记的规则更有效。用这种方法生成的程序可能是ELAN编译器的良好基准。6应用6.1关系的预处理在约束求解器的顶部，我们实现了GenRules，它生成了内部表示为DAG的函数的基于规则的定义现在，约束求解器不仅计算约束的最一般解，而且还自动计算用于生成关系的ELAN模块。 目前，这个新功能被用作一个预处理工具，用于从我们想要集成到ELAN中的关系R的代数规范自动生成一个高效的基于规则的程序（一个模块）。然后，相关的常数R和R中的策略在我们想要使用R的更一般的ELAN程序中是有用的，特别是在wherewith模式中，如例3.3。6.2程序的转换另一种可能性是使用参数化（通过函数），以便将（朴素的）基于规则的ELAN规范转换为改进的基于规则的ELAN程序。具体化定义了兴趣的有限代数和关系。此信息将用于初始化，然后运行约束求解器。约束求解器的输出为我们提供了相关的基于规则的ELAN计算。约束求解器能够处理基于规则的ELAN规范林盖森16我我以下形式。输入规格到目前为止，我们只看到了通过成员关系由值实例化变量的例子。有趣的是，变量受到更复杂关系的约束。为此，我们要变换的关系根据q个独立关系R1，...， R q，对于其中的每一个Rii nv是变量的元组X-i=X1， . ，Xar（Ri），使得我变量X→i的离散元组i，i，J= 1， . ，q，ii=iJ。对于relX→1， . . . ，X→q：dom;全局[genR]R=>R（X→1， . ，X→q）其中R1（X→1）：=（inR1）R1...其中，如果R（X-1， . ，X→q）端我X→iX→iJ =0，用于端关系Ri的对于一个只有一个变量作为左边的where，它的右边是（inD）D。输出计算将条件规则genR转化为无条件规则genR。每个分量Xj由函数Fj生成计算出ELAN无标签规则。约束求解器生成以下带标签的规则genR：相关规则X→1， . ，X→q：dom;Y1， . ，Yr：dom;全球[genR]R=>R（X→1， . ，X→q）其中Y1：=（inD）D→...其中Yr：=（inD）D→其中X1：=（）F1（Y1，...，Y（r）1 1...其中Xar（R1）：=（）Far（R1）（Y1， . ，Yr）1 1...其中X1：=（）F1（Y1，...，Y（r）Q Q...林盖森17其中Xar（R q）：=（）Far（Rq）（Y， . ， Y）的端Q端q1r6.3反射积分法前面的转换的主要缺点是它是一个编译时过程.最好的解决方案是在运行时生成用于参数化关系的规则（同样，通过使用有限代数中的约束求解器）。然后，这些规则可以直接通过基于规则的语言中的反射[11，12]执行。这仅在基于规则的语言中是可能的，该语言具有调用外部求解器和执行由该外部求解器生成的规则的能力。在ELAN中还没有可用的反射机制，甚至已经通过使用当前ELAN交换格式实现了一些实验[3]。然而，在ELAN中已经可以将约束求解器作为外部过程调用[18]。求解器计算的（唯一）结果是一个基于规则的程序，必须通过对ELAN的新调用来执行。7结论在本文中，我们讨论了几种在基于规则的编程语言（如ELAN）中处理有限域上的关系和约束的方法，其中确定性和非确定性计算都是可能的。一方面，我们有确定性的计算免费使用一个concilient和终止TRS由未标记的规则。另一方面，由于策略的作用，非确定性得到了控制，例如收集非连续终止TRS的所有范式的策略。在这种情况下，最合适的方法包括将关系实现为与参数化相关联的非确定性（标记）规则，以及参数化中涉及的函数的一组确定性（未标记）规则。这种基于规则的描述可以使用有限代数中的约束求解器来获得。该求解器的输出已被修改，以生成生成关系的基于规则的程序。然后，这个程序可以在ELAN中以一种更有效的方式执行，而不是通过指定ELAN规则、代数和关系而得到的目前，求解器被用作一个单独的工具。一个跨学科的角度来看，将研究ELAN程序中这个工具的运行时集成。我们相信这将是一个相当好的应用反射机制（尚未提供在ELAN），因为求解器生成一个可执行的ELAN程序。这项工作可以被认为是在同一编程环境中集成约束和规则[13，18，1，10，9]的进一步步骤。在这里，我们感兴趣的是通过使用林盖森18从有限代数中的约束求解器获得的基于规则的程序。该求解器还有助于生成传播规则[22]，这对于执行约束求解和约束传播[2]是最重要的引用[1] Apt ， K. R. ， A Proof Theoretic View of Constraint Programming ，Fundamenta Informaticae34（1998），pp. 295-321[2] Apt，K. R.和E. Monfroy，小有限域约束传播算法的自动生成，在：第五届约束编程原理与实践国际会议（CP58比72[3] Bor ovans ky'，P.， S. Jamoussi，P. E. Moreau和C. 韩·林·埃兰·林盖森通过交换格式重写程序，在：Proc. [16]1998年。[4] Bor ovans ky'， P.， C.Kir c hner ， H.Kir c hner ， P. E.Moreau 和 C.Ringeissen，ELAN概述，载于：Proc. of [16]，1998。[5] 布 赖 恩 特 河E 、 基 于 图 的 布 尔 函 数 操 作 算 法 ， IEEE 计 算 机 学 报 C-35（1986），pp. 677-691[6] Büttner，W. ，在一个扩展的prolog系统中实现复杂的应用域，国际通用系统杂志15（1989），第15页. 129比139[7] B üttner，W.，K. 埃 斯 滕费尔德河S. C.Hmid，H. A. S chneider和E.Tiden，Sym Bolicconstraint handling through unification in finite algebras，Applied Algebra in Engineering ， Communication and Computation 1（1990），pp. 97比118[8] Büttner，W.和H.Simonis，Embededdingbooleanexpressionintologicprogramming，JournalofSymbolicComputation 4（1987），pp. 191-205.[9] Caseau，Y.和F. 结合物件与规则解决问题，载于：JICSLP'96多范例逻辑程式设计研讨会论文集，柏林工业大学，德国，1996年[10] 卡斯特罗角，使用重写规则和策略构建约束满足问题求解器，FundamentaInformaticae34（1998），pp。263-293。[11] Clavel，M.，“一般逻辑中的重写，重写逻辑和Maude，”博士。 西班牙纳瓦拉大学论文（1998年）。[12] Cl avel，M.，F. 你好，S。 Eker，P. Lincoln，N. Mart's-Oliet，J. 梅塞格尔和F. Quesada，Maude as a Metalanguage，in：Proc. [16]1998年。[13] Comon，H.，M. Dincbas，J. P. Jouannaud和C. Kirchner，A methodologicalview of constraint solving，约束4（1999），pp.337-361[14] Deursen，A.， J. Heering和P. Klint，林盖森19[15] Dincbas，M.，H. Simonis和P. Van Hentenryck，逻辑程序设计中的扩展方程求解和约束处理，H。Ait-Kaci和M. Nivat，编者，《代数结构中的方程求解》，学术出版社，圣地亚哥，美国，1989年，第100页。87比115[16] 基什内尔角和H.《明史》（卷112）：“第二次。重写逻辑及其应用研讨会，”爱思唯尔，Pont-a ` -Mousson（法国），1998年。[17] Kirchner ， C. ， H. Kirchner 和 M. Vittek ， Designing Constraint LogicProgramming Languages using Computational Systems，P. Van Hentenryck和V. Saraswat，编辑，Principles and Practice of Constraint Programming。纽波特论文，麻省理工学院出版社，1995年，页。131-158。[18] 基 什 内 尔 角 和 C. Ringeissen ， 基 于 规 则 的 约 束 编 程 ， FundamentaInformaticae34（1998），pp. 225-262[19] Kirchner，H.和C. Ringeissen，A constraint solver in finite algebras and itscombination with unification algorithms ， in： K. Apt ， editor ， Proc. JointInternational Conference and Symposium on Logic Programming（1992），pp. 225-239.[20] Moreau，P. and H.陈晓，一个基于关联交换理论的编译器，北京：清华大学出版社. Palamidessi，H. Glaser和K. Meinke，编辑，声明式编程原理，计算机科学讲义（1998年）第1490号，pp. 230-249。[21] Ringeissen，C.，“Etude et implantation d'un algorithme d'unification dans lesal g ` ebres finies，”Rap p ort de DEA，Uni v ersi t'e Henri Poinca r'e-Nancy 1（1990）.[22] 林盖森角和E. Monfroy，Generating Propagation Rules for Finite Domains：aMixed Approach ， in ： New Trends in Constraints.论 文 从 联 合ERCIM/Computlog-Net研讨会（1999年），讲义在人工智能（2000年），出现。[23] 维特克， M.， 一种用于非确定性项重写系统的编译器，在：H. Ganzinger，编辑，Proceedings 7th Conference on Rewriting Techniquesand Applications，新不伦瑞克（新泽西州，美国），计算机科学讲义1103（1996），pp. 154-168。
我的内容管理
展开
