Range-Restricted Interpolation through Clausal Tableaux

要約

範囲制限のバリエーションと Horn プロパティを、一次ロジックでの Craig 補間の入力から出力にどのように渡すことができるかを示します。
証明システムは、一次 ATP に由来する節的タブローです。
私たちの結果は、節のタブロー構造の制限によって引き起こされます。これは、ソース証明が解像度/パラ変調による場合でも、一般に証明変換によって達成できます。
主に扱われるアプリケーションは、クエリ合成と補間による再定式化です。
私たちの系統的なアプローチは、高度に最適化された一次証明器を組み込むことにより、証明構造に対する操作と実現可能な実装の当面の観点を組み合わせます。

要約(オリジナル)

We show how variations of range-restriction and also the Horn property can be passed from inputs to outputs of Craig interpolation in first-order logic. The proof system is clausal tableaux, which stems from first-order ATP. Our results are induced by a restriction of the clausal tableau structure, which can be achieved in general by a proof transformation, also if the source proof is by resolution/paramodulation. Primarily addressed applications are query synthesis and reformulation with interpolation. Our methodical approach combines operations on proof structures with the immediate perspective of feasible implementation through incorporating highly optimized first-order provers.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google