Superposition-based equality handling for analytic tableaux

被引：0
|
作者：
Giese, Martin [1 ]
机构：
[1] Austrian Acad Sci, Johann Radon Inst Computat & Appl Math, A-4040 Linz, Austria
来源：
JOURNAL OF AUTOMATED REASONING | 2007年 / 38卷 / 1-3期
关键词：
superposition rules; equality handling; analytic tableaux;
D O I：
10.1007/s10817-006-9050-1
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present a variant of the basic ordered superposition rules to handle equality in an analytic free-variable tableau calculus. We prove completeness of this calculus by an adaptation of the model generation technique commonly used for completeness proofs of superposition in the context of resolution calculi. The calculi and the completeness proof are compared to earlier results of Degtyarev and Voronkov. Some variations and refinements are discussed.
引用
收藏
页码：127 / 153
页数：27
相关论文
共 50 条
  • [1] Superposition-based equality handling for analytic tableaux
    Giese, Martin
    Journal of Automated Reasoning, 2007, 38 (1-3): : 127 - 153
  • [2] Superposition-based Equality Handling for Analytic Tableaux
    Martin Giese
    Journal of Automated Reasoning, 2007, 38 : 127 - 153
  • [3] On superposition-based satisfiability procedures and their combination
    Kirchner, H
    Ranise, S
    Ringeissen, C
    Tran, DK
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2005, 2005, 3722 : 594 - 608
  • [4] A Superposition-Based Calculus for Diagrammatic Reasoning
    Echahed, Rachid
    Echenim, Mnacho
    Mhalla, Mehdi
    Peltier, Nicolas
    PROCEEDINGS OF THE 23RD INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, PPDP 2021, 2021,
  • [5] Regular derivations in basic superposition-based calculi
    Aleksic, V
    Degtyarev, A
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 292 - 306
  • [6] Superposition-based concurrent multiscale approaches for poromechanics
    Sun, Wei
    Fish, Jacob
    Ni, Pengpeng
    INTERNATIONAL JOURNAL FOR NUMERICAL METHODS IN ENGINEERING, 2021, 122 (24) : 7328 - 7353
  • [7] Superposition-based concurrent multiscale approaches for porodynamics
    Sun, Wei
    Zhang, Jian-Min
    Fish, Jacob
    Wang, Rui
    INTERNATIONAL JOURNAL FOR NUMERICAL AND ANALYTICAL METHODS IN GEOMECHANICS, 2024, 48 (16) : 3909 - 3932
  • [8] Superposition-based coupling of peridynamics and finite element method
    Sun, Wei
    Fish, Jacob
    COMPUTATIONAL MECHANICS, 2019, 64 (01) : 231 - 248
  • [9] Superposition-based coupling of peridynamics and finite element method
    Wei Sun
    Jacob Fish
    Computational Mechanics, 2019, 64 : 231 - 248
  • [10] Towards a Unified Ordering for Superposition-Based Automated Reasoning
    Jakubuv, Jan
    Kaliszyk, Cezary
    MATHEMATICAL SOFTWARE - ICMS 2018, 2018, 10931 : 245 - 254
12345