Regular derivations in basic superposition-based calculi

被引：0
|
作者：
Aleksic, V [1 ]
Degtyarev, A [1 ]
机构：
[1] Kings Coll London, Dept Comp Sci, London WC2R 2LS, England
来源：
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS | 2005年 / 3835卷
关键词：
D O I：
10.1007/11591191_21
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We prove the completeness of the regular strategy of derivations for superposition-based calculi. The regular strategy was pioneered by Kanger in [Kan63], who proposed that all equality inferences take place before all other steps in the proof. We show that the strategy is complete with the elimination of tautologies. The implication of our result is the completeness of non-standard selection functions by which in non-relational clauses only equality literals (and all of them) are selected.
引用
收藏
页码：292 / 306
页数：15
相关论文
共 50 条
  • [1] 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
  • [2] 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,
  • [3] Superposition-based equality handling for analytic tableaux
    Giese, Martin
    JOURNAL OF AUTOMATED REASONING, 2007, 38 (1-3) : 127 - 153
  • [4] Superposition-based equality handling for analytic tableaux
    Giese, Martin
    Journal of Automated Reasoning, 2007, 38 (1-3): : 127 - 153
  • [5] 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
  • [6] Superposition-based Equality Handling for Analytic Tableaux
    Martin Giese
    Journal of Automated Reasoning, 2007, 38 : 127 - 153
  • [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