Bottom-up Construction of Semantic Tableaux

NICOLAS PELTIER

首页> 外文期刊>Journal of logic and computation >Bottom-up Construction of Semantic Tableaux

【24h】

Bottom-up Construction of Semantic Tableaux

机译：语义表的自下而上的构造

获取原文

获取原文并翻译 | 示例

掌桥外文数据库（机构版） >>

开具论文收录证明 >>

文献代查 >>

页面导航

摘要
著录项
相似文献
相关主题

摘要

We present a new proof procedure for first-order logic. Our approach is closely related to semantic tableaux, but it uses a more compact representation of the search space. The idea is to construct the tableau from the leaves to the root, which helps to factorize common subtrees and reduces the information that must be stored in a given branch. We prove that the method is sound and refutationally complete and we provide simplification rules in order to prune the search space and delete redundant inferences. We show that our procedure runs in polynomial time for several propositional classes, including the Hom-renamable class or the Krom class. This article is an extended version of Peltier (2007, LNAI 4548).

机译：我们提出了一阶逻辑的新证明程序。我们的方法与语义表密切相关，但是它使用了搜索空间的更紧凑表示。这个想法是从叶子到根来构造画面，这有助于分解公共子树并减少必须存储在给定分支中的信息。我们证明了该方法是正确且反驳的，并且提供了简化规则以修剪搜索空间并删除多余的推论。我们证明，我们的程序针对多项命题类（包括Hom可移植类或Krom类）在多项式时间内运行。本文是Peltier的扩展版本（2007，LNAI 4548）。

著录项

来源
《Journal of logic and computation》 |2010年第1期|283-308|共26页
作者
NICOLAS PELTIER;
展开▼
作者单位

LIG, CNRS 46, avenue Felix Viallet, 38031 Grenoble Cedex, France;

展开▼
收录信息
原文格式 PDF
正文语种 eng
中图分类
关键词
automated deduction; proof procedures; semantic tableaux; polynomial classes; complexity;

机译：自动扣除;证明程序;语义表多项式类复杂;

相似文献

外文文献
中文文献
专利

1. Bivalent semantics, generalized compositionality and analytic classic-like tableaux for finite-valued logics [J] . Wolfgang Schreiner Computing reviews . 2016,第4期

机译：有限值逻辑的二价语义，广义组合性和经典类分析表
2. Free-Variable Semantic Tableaux for the Logic of Fuzzy Inequalities [J] . Gerasimov A. S. Algebra and logic . 2016,第2期

机译：模糊不等式逻辑的自由变量语义表
3. Free-Variable Semantic Tableaux for the Logic of Fuzzy Inequalities (vol 55, pg 103, 2016) [J] . Gerasimov A. S. Algebra and logic . 2016,第3期

机译：模糊不等式逻辑的自由变量语义表（2016年第55卷，第103页）
4. A Bottom-Up Approach to Clausal Tableaux [C] . Nicolas Peltier International Conference on Automated Reasoning with Analytic Tableaux and Related Methods(TABLEAUX 2007); 20070703-06; Aix en Provence(FR) . 2007

机译：自下而上的子句处理方法
5. Generalized Foulkes' conjecture and tableaux construction [D] . Vessenes, Rebecca. 2004

机译：广义Foulkes猜想和平台构造
6. On-Surface Bottom-Up Construction of COF Nanoshells towards Photocatalytic H2 Production [O] . Yao Chen, Dong Yang, Yuchen Gao, 2021

机译：COF纳米型朝向光催化H2生产的COF纳米型施工
7. Construction de machines non electriques (Ex N.I.C.E. 36). Machines et tracteurs agricoles (N.I.C.E. 36). Machines de bureau (N.I.C.E. 362). Machines textiles et accessoires (N.I.C.E. 364.1). Machines pour materiaux de construction (N.I.C.E. 366.3). Material de levage et de manutention (N.I.C.E. 366.5). Tableaux de concentration. Allemagne. France = Construction of non-electrical machinery (Ex N.I.C.E. 36). Agricultural machinery and tractors (N.I.C.E. 36). Office machines (N.I.C.E. 362). Textile machinery and accessories (N.I.C.E. 364.1). Construction machinery (N.I.C.E. 366.3). Lifting and material handling (N.I.C.E. 366.5). Concentration tables. Germany. France. Studies: Evolution of concentration and competition series [O] . 1974

机译：建筑机械非电气（Ex N.I.C.E.36）。机器和农业机构（N.I.C.E.36）。机器局（N.I.C.E.362）。机器纺织品和配件（N.I.C.E.364.1）。机器浇筑materiaux de construction（N.I.C.E.366.3）。物质剥削与制造（N.I.C.E.366.5）。 Tableaux de concentration。 aLLEmaGNE。法国=建造非电动机械（Ex N.I.C.E.36）。农业机械和拖拉机（N.I.C.E.36）。办公室机器（N.I.C.E.362）。纺织机械及配件（N.I.C.E.364.1）。建筑机械（N.I.C.E.366.3）。提升和物料搬运（N.I.C.E.366.5）。浓度表。德国。法国。研究：集中和竞争系列的演变

Bottom-up Construction of Semantic Tableaux

摘要

著录项

相似文献

相关主题

期刊订阅