REWRITE METHODS FOR CLAUSAL AND NON-CLAUSAL THEOREM-PROVING

被引:0
|
作者
HSIANG, J [1 ]
DERSHOWITZ, N [1 ]
机构
[1] UNIV ILLINOIS,DEPT COMP SCI,URBANA,IL 61801
关键词
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
引用
收藏
页码:331 / 346
页数:16
相关论文
共 50 条
  • [1] COMPLETELY NON-CLAUSAL THEOREM-PROVING
    MURRAY, NV
    [J]. ARTIFICIAL INTELLIGENCE, 1982, 18 (01) : 67 - 85
  • [2] Reductions for non-clausal theorem proving
    Aguilera, G
    de Guzmán, IP
    Ojeda-Aciego, M
    Valverde, A
    [J]. THEORETICAL COMPUTER SCIENCE, 2001, 266 (1-2) : 81 - 112
  • [3] nanoCoP: Natural Non-clausal Theorem Proving
    Otten, Jens
    [J]. PROCEEDINGS OF THE TWENTY-SIXTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2017, : 4924 - 4928
  • [4] From Non-Clausal to Clausal MinSAT
    Li, Chu-Min
    Manya, Felip
    Soler, Joan Ramon
    Vidal, Amanda
    [J]. ARTIFICIAL INTELLIGENCE RESEARCH AND DEVELOPMENT, 2021, 339 : 27 - 36
  • [5] A Non-clausal Connection Calculus
    Otten, Jens
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 2011, 6793 : 226 - 241
  • [6] Non-clausal Redundancy Properties
    Barnett, Lee A.
    Biere, Armin
    [J]. AUTOMATED DEDUCTION, CADE 28, 2021, 12699 : 252 - 272
  • [7] Combining SAT Methods with Non-Clausal Decision Heuristics
    Barrett, Clark
    Donham, Jacob
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 125 (03) : 3 - 12
  • [8] An application of non-clausal deduction in diagnosis
    Ramesh, A
    Murray, NV
    [J]. EXPERT SYSTEMS WITH APPLICATIONS, 1997, 12 (01) : 119 - 126
  • [9] Prime Compilation of Non-Clausal Formulae
    Previti, A.
    Ignatiev, A.
    Morgado, A.
    Marques-Silva, J.
    [J]. PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI), 2015, : 1980 - 1987
  • [10] Applying GSAT to Non-Clausal Formulas
    Sebastiani, Roberto
    [J]. JOURNAL OF ARTIFICIAL INTELLIGENCE RESEARCH, 1993, 1 : 309 - 314