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 条
  • [41] A TRUNCATION TECHNIQUE FOR CLAUSAL ANALYTIC TABLEAUX
    WRIGHTSON, G
    COLDWELL, J
    INFORMATION PROCESSING LETTERS, 1992, 42 (05) : 273 - 281
  • [42] Multiscale modeling for fire induced spalling in concrete tunnel linings based on the superposition-based phase field fracture model
    Cheng, Panpan
    Zhu, Hehua
    Yan, Zhiguo
    Shen, Yi
    Fish, Jacob
    COMPUTERS AND GEOTECHNICS, 2022, 148
  • [43] Analytic Tableaux for all of SIXTEEN 3
    Muskens, Reinhard
    Wintein, Stefan
    JOURNAL OF PHILOSOPHICAL LOGIC, 2015, 44 (05) : 473 - 487
  • [44] Utility of superposition-based finite element approach for part-scale thermal simulation in additive manufacturing
    Moran, T. P.
    Li, P.
    Warner, D. H.
    Phan, N.
    ADDITIVE MANUFACTURING, 2018, 21 : 215 - 219
  • [45] The proof complexity of analytic and clausal tableaux
    Massacci, F
    THEORETICAL COMPUTER SCIENCE, 2000, 243 (1-2) : 477 - 487
  • [46] An efficient seven-parameter double superposition-based theory for free vibration analysis of laminated composite shells
    Fan, Guangli
    Lezgy-Nazargah, M.
    EUROPEAN JOURNAL OF MECHANICS A-SOLIDS, 2024, 106
  • [47] A Superposition-Based Variable-Weight Over-Modulation Method for Drive PMSM Controller in Electric Vehicles
    Lin C.
    Jiang X.
    Zhuang X.
    Liu H.
    Xing J.
    Gao S.
    Qiche Gongcheng/Automotive Engineering, 2022, 44 (11): : 1725 - 1734+1754
  • [48] Block-wise superposition-based frequency-domain synthetic aperture focusing imaging of leaky Rayleigh waves
    Hu, Hongwei
    Yang, Decao
    Lyu, Duo
    Luo, Xiaofei
    Chen, Xiaomin
    APPLIED ACOUSTICS, 2025, 233
  • [49] Analytic Tableaux for Non-deterministic Semantics
    Graetz, Lukas
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2021, 2021, 12842 : 38 - 55
  • [50] Analytic tableaux for KLM preferential and cumulative logics
    Giordano, L
    Gliozzi, V
    Olivetti, N
    Pozzato, GL
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 666 - 681
12345