Efficient Implementation of the Plan Graph in STAN
STANにおけるプラングラフの効率的な実装
STAN is a Graphplan-based planner, so-called because it uses a variety of STate ANalysis techniques to enhance its performance. STAN competed in the AIPS-98 planning competition where it compared well with the other competitors in terms of speed, finding solutions fastest to many of the problems posed. Although the domain analysis techniques STAN exploits are an important factor in its overall performance, we believe that the speed at which STAN solved the competition problems is largely due to the implementation of its plan graph. The implementation is based on two insights: that many of the graph construction operations can be implemented as bit-level logical operations on bit vectors, and that the graph should not be explicitly constructed beyond the fix point. This paper describes the implementation of STAN’s plan graph and provides experimental results which demonstrate the circumstances under which advantages can be obtained from using this implementation.
STANはGraphplanベースのプランナーです。これは、パフォーマンスを向上させるために様々な状態分析手法を使用していることから、このように呼ばれています。STANはAIPS-98プランニングコンペティションに出場し、速度の点で他の競合相手に引けを取らず、提示された多くの問題に対して最速で解を見つけ出しました。STANが利用するドメイン分析手法は全体的なパフォーマンスの重要な要素ですが、STANがコンペティションの問題を解く速度は、主にプラングラフの実装によるものだと考えています。この実装は、グラフ構築演算の多くはビットベクトルに対するビットレベルの論理演算として実装できること、そしてグラフは固定点を超えて明示的に構築されるべきではないという2つの知見に基づいています。本稿では、STANのプラングラフの実装について説明し、この実装を使用することでどのような状況でメリットが得られるかを示す実験結果を示します。
A Counter Example to Theorems of Cox and Fine
コックスとファイン定理の反例
Cox’s well-known theorem justifying the use of probability is shown not to hold in finite domains. The counterexample also suggests that Cox’s assumptions are insufficient to prove the result even in infinite domains. The same counterexample is used to disprove a result of Fine on comparative conditional probability.
確率の使用を正当化するCoxのよく知られた定理は、有限領域では成り立たないことが示されています。反例はまた、Coxの仮定は無限領域であっても結果を証明するのに不十分であることを示唆しています。同じ反例は、比較条件付き確率に関するFineの結果を反証するために使用されています。
The Good Old Davis-Putnam Procedure Helps Counting Models
古き良きデイビス・パトナム法は計数モデルに役立つ
As was shown recently, many important AI problems require counting the number of models of propositional formulas. The problem of counting models of such formulas is, according to present knowledge, computationally intractable in a worst case. Based on the Davis-Putnam procedure, we present an algorithm, CDP, that computes the exact number of models of a propositional CNF or DNF formula F. Let m and n be the number of clauses and variables of F, respectively, and let p denote the probability that a literal l of F occurs in a clause C of F, then the average running time of CDP is shown to be O(nm^d), where d=-1/log(1-p). The practical performance of CDP has been estimated in a series of experiments on a wide variety of CNF formulas.
最近示されたように、多くの重要なAI問題では、命題論理式のモデルの数を数える必要があります。現在の知見によれば、このような式のモデルの数を数える問題は、最悪の場合、計算的に扱いにくい問題です。Davis-Putnam手順に基づいて、命題CNFまたはDNF論理式Fのモデルの正確な数を計算するアルゴリズムCDPを紹介します。mとnをそれぞれFの節と変数の数とし、pをFのリテラルlがFの節Cに出現する確率とすると、CDPの平均実行時間はO(nm^d)であることが示されます(d=-1/log(1-p))。CDPの実際的なパフォーマンスは、さまざまなCNF論理式に対する一連の実験で推定されています。
Variational Cumulant Expansions for Intractable Distributions
扱いにくい分布に対する変分キュムラント展開
Intractable distributions present a common difficulty in inference within the probabilistic knowledge representation framework and variational methods have recently been popular in providing an approximate solution. In this article, we describe a perturbational approach in the form of a cumulant expansion which, to lowest order, recovers the standard Kullback-Leibler variational bound. Higher-order terms describe corrections on the variational approach without incurring much further computational cost. The relationship to other perturbational approaches such as TAP is also elucidated. We demonstrate the method on a particular class of undirected graphical models, Boltzmann machines, for which our simulation results confirm improved accuracy and enhanced stability during learning.
確率的知識表現フレームワークにおける推論では、扱いにくい分布が共通の難題となっており、近似解を得るための変分法が近年人気を集めています。本稿では、キュムラント展開という形で摂動論的アプローチについて述べ、最低次で標準的なカルバック・ライブラー変分境界を回復します。高次の項は、変分法の補正を記述しますが、計算コストはそれほど増加しません。TAPなどの他の摂動論的アプローチとの関係も明らかにします。本稿では、この手法を特定のクラスの無向グラフィカルモデルであるボルツマンマシンに適用し、シミュレーション結果から学習精度の向上と安定性の向上を確認しました。
Extensible Knowledge Representation: the Case of Description Reasoners
拡張可能な知識表現：記述推論器の場合
This paper offers an approach to extensible knowledge representation and reasoning for a family of formalisms known as Description Logics. The approach is based on the notion of adding new concept constructors, and includes a heuristic methodology for specifying the desired extensions, as well as a modularized software architecture that supports implementing extensions. The architecture detailed here falls in the normalize-compared paradigm, and supports both intentional reasoning (subsumption) involving concepts, and extensional reasoning involving individuals after incremental updates to the knowledge base. The resulting approach can be used to extend the reasoner with specialized notions that are motivated by specific problems or application areas, such as reasoning about dates, plans, etc. In addition, it provides an opportunity to implement constructors that are not currently yet sufficiently well understood theoretically, but are needed in practice. Also, for constructors that are provably hard to reason with (e.g., ones whose presence would lead to undecidability), it allows the implementation of incomplete reasoners where the incompleteness is tailored to be acceptable for the application at hand.
本論文では、記述論理として知られる形式主義ファミリーのための、拡張可能な知識表現と推論へのアプローチを提示します。このアプローチは、新しい概念構成子を追加するという概念に基づいており、望ましい拡張を指定するためのヒューリスティックな方法論と、拡張の実装をサポートするモジュール化されたソフトウェアアーキテクチャを含む。ここで詳述するアーキテクチャは、正規化比較パラダイムに属し、概念を含む意図的推論（包摂）と、知識ベースの増分更新後の個体を含む外延的推論の両方をサポートします。このアプローチは、日付や計画などに関する推論など、特定の問題や応用分野を動機とする特殊な概念を用いて推論システムを拡張するために使用することができます。さらに、理論的には現時点では十分に理解されていないものの、実際には必要とされる構成子を実装する機会も提供します。また、推論が証明困難な構成子（例えば、その存在が決定不能性につながる構成子）については、不完全性が現在のアプリケーションで許容される程度に調整された不完全な推論システムの実装を可能にします。
Solving Highly Constrained Search Problems with Quantum Computers
量子コンピュータを用いた高度に制約された探索問題の解法
A previously developed quantum search algorithm for solving 1-SAT problems in a single step is generalized to apply to a range of highly constrained k-SAT problems. We identify a bound on the number of clauses in satisfiability problems for which the generalized algorithm can find a solution in a constant number of steps as the number of variables increases. This performance contrasts with the linear growth in the number of steps required by the best classical algorithms, and the exponential number required by classical and quantum methods that ignore the problem structure. In some cases, the algorithm can also guarantee that insoluble problems in fact have no solutions, unlike previously proposed quantum search algorithms.
1-SAT問題を1ステップで解くために以前に開発された量子探索アルゴリズムを一般化し、様々な制約条件を持つk-SAT問題に適用できるようにしました。変数の数が増えても、この一般化アルゴリズムが定数ステップ数で解を見つけられる、充足可能性問題における節の数に上限があることを明らかにしました。この性能は、最良の古典的アルゴリズムで必要なステップ数が線形に増加することや、問題の構造を無視する古典的手法および量子的手法で必要なステップ数が指数関数的に増加することとは対照的です。また、このアルゴリズムは、これまで提案された量子探索アルゴリズムとは異なり、場合によっては、解けない問題には実際には解が存在しないことを保証できます。
Efficient Heuristic Hypothesis Ranking
効率的なヒューリスティック仮説ランキング
This paper considers the problem of learning the ranking of a set of stochastic alternatives based upon incomplete information (i.e., a limited number of samples). We describe a system that, at each decision cycle, outputs either a complete ordering on the hypotheses or decides to gather additional information (i.e., observations) at some cost. The ranking problem is a generalization of the previously studied hypothesis selection problem – in selection, an algorithm must select the single best hypothesis, while in ranking, an algorithm must order all the hypotheses. The central problem we address is achieving the desired ranking quality while minimizing the cost of acquiring additional samples. We describe two algorithms for hypothesis ranking and their application for the probably approximately correct (PAC) and expected loss (EL) learning criteria. Empirical results are provided to demonstrate the effectiveness of these ranking procedures on both synthetic and real-world datasets.
本論文では、不完全な情報（すなわち、限られた数のサンプル）に基づいて、確率的選択肢の集合の順位付けを学習する問題を考察します。各決定サイクルにおいて、仮説の完全な順序付けを出力するか、何らかのコストをかけて追加情報（すなわち、観測値）を収集することを決定するシステムについて説明します。順位付け問題は、これまで研究されてきた仮説選択問題の一般化です。選択においては、アルゴリズムは最良の仮説を1つ選択する必要があり、順位付けにおいては、アルゴリズムはすべての仮説を順序付けする必要があります。我々が取り組む中心的な問題は、追加サンプルの取得コストを最小限に抑えながら、望ましい順位付け品質を達成することです。本論文では、仮説順位付けのための2つのアルゴリズムと、それらの学習基準（おそらく近似正解（PAC）および期待損失（EL））への適用について説明します。これらの順位付け手順の有効性を、合成データセットと実世界のデータセットの両方で実証的に示します。
Squeaky Wheel Optimization
軋む車輪の最適化
We describe a general approach to optimization which we term `Squeaky Wheel’ Optimization (SWO). In SWO, a greedy algorithm is used to construct a solution which is then analyzed to find the trouble spots, i.e., those elements, that, if improved, are likely to improve the objective function score. The results of the analysis are used to generate new priorities that determine the order in which the greedy algorithm constructs the next solution. This Construct/Analyze/Prioritize cycle continues until some limit is reached, or an acceptable solution is found. SWO can be viewed as operating on two search spaces: solutions and prioritizations. Successive solutions are only indirectly related, via the re-prioritization that results from analyzing the prior solution. Similarly, successive prioritizations are generated by constructing and analyzing solutions. This `coupled search’ has some interesting properties, which we discuss. We report encouraging experimental results on two domains, scheduling problems that arise in fiber-optic cable manufacturing, and graph coloring problems. The fact that these domains are very different supports our claim that SWO is a general technique for optimization.
本稿では、「きしむ車輪」最適化（SWO）と呼ぶ一般的な最適化手法について説明します。SWOでは、貪欲アルゴリズムを用いて解を構築し、その解を分析して問題点、すなわち改善すれば目的関数のスコアが向上する可能性が高い要素を特定します。分析結果を用いて新たな優先順位を生成し、貪欲アルゴリズムが次の解を構築する順序を決定します。この構築／分析／優先順位付けのサイクルは、ある限界に達するか、許容可能な解が見つかるまで継続されます。SWOは、解と優先順位付けという2つの探索空間で動作していると見ることができます。次々に生成される解は、前の解の分析から生じる再優先順位付けを介してのみ間接的に関連しています。同様に、次々に生成される優先順位付けは、解の構築と分析によって生成されます。この「結合探索」には興味深い特性があり、それらについて考察します。光ファイバーケーブル製造におけるスケジューリング問題とグラフ彩色問題という2つの領域において、有望な実験結果を報告します。これらの領域が大きく異なるという事実は、SWOが最適化のための汎用的な手法であるという我々の主張を裏付けています。
Constructing Conditional Plans by a Theorem-Prover
定理証明器による条件付きプランの構築
The research on conditional planning rejects the assumptions that there is no uncertainty or incompleteness of knowledge with respect to the state and changes of the system the plans operate on. Without these assumptions the sequences of operations that achieve the goals depend on the initial state and the outcomes of nondeterministic changes in the system. This setting raises the questions of how to represent the plans and how to perform plan search. The answers are quite different from those in the simpler classical framework. In this paper, we approach conditional planning from a new viewpoint that is motivated by the use of satisfiability algorithms in classical planning. Translating conditional planning to formulae in the propositional logic is not feasible because of inherent computational limitations. Instead, we translate conditional planning to quantified Boolean formulae. We discuss three formalizations of conditional planning as quantified Boolean formulae, and present experimental results obtained with a theorem-prover.
条件付きプランニングの研究では、プランが適用されるシステムの状態と変化に関して、知識の不確実性や不完全性が存在しないという仮定を否定しています。これらの仮定がなければ、目標を達成する操作のシーケンスは、初期状態とシステムにおける非決定論的な変化の結果に依存します。この設定では、プランをどのように表現し、プラン探索をどのように実行するかという問題が生じます。その答えは、より単純な従来のフレームワークの場合とはまったく異なります。本稿では、古典的なプランニングにおける充足可能性アルゴリズムの適用に着目し、新たな観点から条件付きプランニングにアプローチします。条件付きプランニングを命題論理の論理式に置き換えることは、計算上の制約から現実的ではない。そこで本稿では、条件付きプランニングを量化ブール論理式に変換します。量化ブール論理式として条件付きプランニングを形式化する3つの方法について考察し、定理証明器を用いて得られた実験結果を示す。
Variational Probabilistic Inference and the QMR-DT Network
変分確率推論とQMR-DTネットワーク
We describe a variational approximation method for efficient inference in large-scale probabilistic models. Variational methods are deterministic procedures that provide approximations to marginal and conditional probabilities of interest. They provide alternatives to approximate inference methods based on stochastic sampling or search. We describe a variational approach to the problem of diagnostic inference in the `Quick Medical Reference’ (QMR) network. The QMR network is a large-scale probabilistic graphical model built on statistical and expert knowledge. Exact probabilistic inference is infeasible in this model for all but a small set of cases. We evaluate our variational inference algorithm on a large set of diagnostic test cases, comparing the algorithm to a state-of-the-art stochastic sampling method.
大規模確率モデルにおける効率的な推論のための変分近似法について説明します。変分法は、対象となる周辺確率と条件付き確率の近似値を提供する決定論的な手順です。これらは、確率的サンプリングや探索に基づく近似推論法の代替手段となります。本稿では、「Quick Medical Reference」（QMR）ネットワークにおける診断推論の問題に対する変分アプローチについて説明します。QMRネットワークは、統計的知識と専門知識に基づいて構築された大規模な確率的グラフィカルモデルです。このモデルでは、少数のケースを除いて正確な確率的推論は実行不可能です。本稿では、変分推論アルゴリズムを多数の診断テストケースで評価し、最先端の確率的サンプリング法と比較します。
Issues in Stacked Generalization
スタック一般化における問題
Stacked generalization is a general method of using a high-level model to combine lower-level models to achieve greater predictive accuracy. In this paper we address two crucial issues which have been considered to be a `black art’ in classification tasks ever since the introduction of stacked generalization in 1992 by Wolpert: the type of generalizer that is suitable to derive the higher-level model, and the kind of attributes that should be used as its input. We find that best results are obtained when the higher-level model combines the confidence (and not just the predictions) of the lower-level ones. We demonstrate the effectiveness of stacked generalization for combining three different types of learning algorithms for classification tasks. We also compare the performance of stacked generalization with majority vote and published results of arcing and bagging.
スタック一般化は、高レベルモデルを用いて低レベルモデルを組み合わせることで、より高い予測精度を実現する一般的な手法です。本稿では、1992年にWolpertがスタック一般化を導入して以来、分類タスクにおいて「黒魔術」とされてきた2つの重要な問題、すなわち、高レベルモデルを導出するのに適した一般化器の種類と、その入力として使用すべき属性の種類について考察します。高レベルモデルが低レベルモデルの予測値だけでなく信頼度も組み合わせることで、最良の結果が得られることがわかりました。分類タスクにおいて、3つの異なる学習アルゴリズムを組み合わせるスタック一般化の有効性を示します。また、スタック一般化の性能を多数決法、および公開されているアーク法とバギング法と比較します。
Learning to Order Things
物事の順序付けの学習
There are many applications in which it is desirable to order rather than classify instances. Here we consider the problem of learning how to order instances given feedback in the form of preference judgments, i.e., statements to the effect that one instance should be ranked ahead of another. We outline a two-stage approach in which one first learns by conventional means a binary preference function indicating whether it is advisable to rank one instance before another. Here we consider an on-line algorithm for learning preference functions that is based on Freund and Schapire’s ‘Hedge’ algorithm. In the second stage, new instances are ordered so as to maximize agreement with the learned preference function. We show that the problem of finding the ordering that agrees best with a learned preference function is NP-complete. Nevertheless, we describe simple greedy algorithms that are guaranteed to find a good approximation. Finally, we show how metasearch can be formulated as an ordering problem, and present experimental results on learning a combination of ‘search experts’, each of which is a domain-specific query expansion strategy for a web search engine.
インスタンスを分類するのではなく、順序付けすることが望ましいアプリケーションは数多く存在します。本稿では、選好判断（あるインスタンスを他のインスタンスよりも上位にランク付けすべき旨の記述）という形でフィードバックを与えられた場合に、インスタンスの順序付け方法を学習する問題を考察します。まず、従来の方法を用いて、あるインスタンスを他のインスタンスよりも上位にランク付けすることが適切かどうかを示す2値選好関数を学習する2段階アプローチを概説します。本稿では、フロイントとシャピレの「ヘッジ」アルゴリズムに基づく、選好関数を学習するためのオンラインアルゴリズムを考察します。第2段階では、学習した選好関数との一致を最大化するように、新しいインスタンスを順序付けます。学習した選好関数と最も一致する順序付けを見つける問題はNP完全であることを示します。しかしながら、良好な近似値を見つけることが保証される単純な貪欲アルゴリズムについて説明します。最後に、メタサーチを順序付け問題として定式化する方法を示し、Web検索エンジンのためのドメイン固有のクエリ拡張戦略である「検索エキスパート」の組み合わせを学習する実験結果を示します。
Probabilistic Deduction with Conditional Constraints over Basic Events
基本事象に対する条件付き制約付き確率的演繹
We study the problem of probabilistic deduction with conditional constraints over basic events. We show that globally complete probabilistic deduction with conditional constraints over basic events is NP-hard. We then concentrate on the special case of probabilistic deduction in conditional constraint trees. We elaborate very efficient techniques for globally complete probabilistic deduction. In detail, for conditional constraint trees with point probabilities, we present a local approach to globally complete probabilistic deduction, which runs in linear time in the size of the conditional constraint trees. For conditional constraint trees with interval probabilities, we show that globally complete probabilistic deduction can be done in a global approach by solving nonlinear programs. We show how these nonlinear programs can be transformed into equivalent linear programs, which are solvable in polynomial time in the size of the conditional constraint trees.
本研究では、基本事象に対する条件付き制約付き確率演繹の問題を考察します。基本事象に対する条件付き制約付き大域的完全確率演繹はNP困難であることを示す。次に、条件付き制約木における確率演繹の特殊なケースに焦点を当てる。大域的完全確率演繹のための非常に効率的な手法を詳述します。具体的には、点確率を持つ条件付き制約木に対して、条件付き制約木のサイズに対して線形時間で実行される、大域的完全確率演繹への局所的アプローチを提示します。区間確率を持つ条件付き制約木に対しては、非線形計画問題を解くことによって、大域的アプローチで大域的完全確率演繹が実行可能であることを示す。これらの非線形計画問題を、条件付き制約木のサイズに対して多項式時間で解ける等価な線形計画問題に変換する方法を示す。
Cooperation between Top-Down and Bottom-Up Theorem Provers
トップダウン型とボトムアップ型の定理証明器の連携
Top-down and bottom-up theorem proving approaches each have specific advantages and disadvantages. Bottom-up provers profit from strong redundancy control but suffer from the lack of goal-orientation, whereas top-down provers are goal-oriented but often have weak calculi when their proof lengths are considered. In order to integrate both approaches, we try to achieve cooperation between a top-down and a bottom-up prover in two different ways: The first technique aims at supporting a bottom-up with a top-down prover. A top-down prover generates subgoal clauses, they are then processed by a bottom-up prover. The second technique deals with the use of bottom-up generated lemmas in a top-down prover. We apply our concept to the areas of model elimination and superposition. We discuss the ability of our techniques to shorten proofs as well as to reorder the search space in an appropriate manner. Furthermore, in order to identify subgoal clauses and lemmas which are actually relevant for the proof task, we develop methods for a relevancy-based filtering. Experiments with the provers SETHEO and SPASS performed in the problem library TPTP reveal the high potential of our cooperation approaches.
トップダウン型とボトムアップ型の定理証明手法には、それぞれ長所と短所があります。ボトムアップ型証明器は強力な冗長性制御の恩恵を受けますが、ゴール指向性に欠けるという欠点があります。一方、トップダウン型証明器はゴール指向性を備えていますが、証明長を考慮すると計算が弱いという問題があります。この2つの手法を統合するために、我々はトップダウン型証明器とボトムアップ型証明器の連携を2つの異なる方法で実現しようと試みます。最初の手法は、ボトムアップ型証明器をトップダウン型証明器でサポートすることを目的としています。トップダウン型証明器はサブゴール節を生成し、それをボトムアップ型証明器が処理します。2つ目の手法は、ボトムアップ型証明器で生成された補題をトップダウン型証明器で使用することを扱います。この概念をモデル消去と重ね合わせの分野に適用します。本手法が証明を短縮する能力と、探索空間を適切に並べ替える能力について議論します。さらに、証明課題に実際に関連するサブゴール節と補題を特定するために、関連性に基づくフィルタリング手法を開発します。問題ライブラリTPTPにおいて、証明器SETHEOおよびSPASSを用いた実験により、本協調アプローチの高い可能性が明らかになった。
Modeling Belief in Dynamic Systems, Part II: Revision and Update
動的システムにおける信念のモデリング、パートII：修正と更新
The study of belief change has been an active area in philosophy and AI. In recent years two special cases of belief change, belief revision and belief update, have been studied in detail. In a companion paper (Friedman & Halpern, 1997), we introduce a new framework to model belief change. This framework combines temporal and epistemic modalities with a notion of plausibility, allowing us to examine the change of beliefs over time. In this paper, we show how belief revision and belief update can be captured in our framework. This allows us to compare the assumptions made by each method, and to better understand the principles underlying them. In particular, it shows that Katsuno and Mendelzon’s notion of belief update (Katsuno & Mendelzon, 1991a) depends on several strong assumptions that may limit its applicability in artificial intelligence. Finally, our analysis allow us to identify a notion of minimal change that underlies a broad range of belief change operations including revision and update.
信念変化の研究は、哲学とAIにおいて活発な分野です。近年、信念の変化に関する2つの特殊なケース、信念の修正と信念の更新が詳細に研究されてきました。関連論文(Friedman & Halpern, 1997)では、信念の変化をモデル化する新しい枠組みを紹介します。この枠組みは、時間的および認識論的様相を妥当性の概念と組み合わせることで、時間の経過に伴う信念の変化を調べることができます。本論文では、信念の修正と信念の更新をこの枠組みでどのように取り込むことができるかを示します。これにより、各手法の仮定を比較し、その背後にある原理をより深く理解することができます。特に、KatsunoとMendelzonによる信念の更新の概念(Katsuno & Mendelzon, 1991a)は、人工知能への適用性を制限する可能性のあるいくつかの強力な仮定に依存していることを示しています。最後に、私たちの分析により、修正や更新を含む幅広い信念の変化操作の根底にある最小限の変化の概念を特定することができます。
Order of Magnitude Comparisons of Distance
距離の桁違い比較
Order of magnitude reasoning – reasoning by rough comparisons of the sizes of quantities – is often called `back of the envelope calculation’, with the implication that the calculations are quick though approximate. This paper exhibits an interesting class of constraint sets in which order of magnitude reasoning is demonstrably fast. Specifically, we present a polynomial-time algorithm that can solve a set of constraints of the form `Points a and b are much closer together than points c and d.’ We prove that this algorithm can be applied if `much closer together’ is interpreted either as referring to an infinite difference in scale or as referring to a finite difference in scale, as long as the difference in scale is greater than the number of variables in the constraint set. We also prove that the first-order theory over such constraints is decidable.
桁違い推論（量の大まかな比較による推論）はしばしば「ざっくりとした計算」と呼ばれ、計算は近似的ではあるものの高速であるという含意があります。本論文では、桁違い推論が明らかに高速である興味深い制約集合のクラスを示します。具体的には、「点aと点bは点cと点dよりもはるかに近い」という形式の制約集合を解くことができる多項式時間アルゴリズムを提示します。このアルゴリズムは、「はるかに近い」が無限大のスケール差を指すと解釈される場合も、有限のスケール差を指すと解釈される場合も、スケール差が制約集合内の変数の数よりも大きい限り適用できることを証明します。また、このような制約上の一階理論が決定可能であることも証明します。