A RESOLUTION PROVER FOR S4

被引：0
|
作者：
BAZYLEV, VY
机构：
来源：
SOVIET JOURNAL OF COMPUTER AND SYSTEMS SCIENCES | 1991年 / 29卷 / 03期
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The implementation is described of a system of automatic and interactive search of deduction in resolution calculus for the modal proportional logic S4 [1]. Certain modifications of classical resolution strategies applicable to S4 are considered. A version of a reduction algorithm of an arbitrary formula to a list of disjuncts based on introduction of new variables and on equivalent transformations is proposed. Results are given of an experiment conducted with a program which shows that it seems to be substantially superior, so far as its possibilities are concerned, to all other programs for S4 known to the author.
引用
收藏
页码：97 / 101
页数：5
相关论文
共 50 条
  • [1] Transfer of sequent calculus strategies to resolution for S4
    Mints, G
    Orevkov, V
    Tammet, T
    [J]. PROOF THEORY OF MODAL LOGIC, 1996, 2 : 17 - 31
  • [2] S4正式到来:详解S4季前赛补丁
    皮杰飞飞
    [J]. 电子竞技, 2013, (23) : 72 - 79
  • [3] Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
    Schlichtkrull, Anders
    Blanchette, Jasmin
    Traytel, Dmitriy
    Waldmann, Uwe
    [J]. JOURNAL OF AUTOMATED REASONING, 2020, 64 (07) : 1169 - 1195
  • [4] Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
    Anders Schlichtkrull
    Jasmin Blanchette
    Dmitriy Traytel
    Uwe Waldmann
    [J]. Journal of Automated Reasoning, 2020, 64 : 1169 - 1195
  • [5] Formalizing Bachmair and Ganzinger's Ordered Resolution Prover
    Schlichtkrull, Anders
    Blanchette, Jasmin Christian
    Traytel, Dmitriy
    Waldmann, Uwe
    [J]. AUTOMATED REASONING, IJCAR 2018, 2018, 10900 : 89 - 107
  • [6] Splittings of S4
    Lickorish, WBR
    [J]. BOLETIN DE LA SOCIEDAD MATEMATICA MEXICANA, 2004, 10 : 305 - 312
  • [7] The Incompleteness of S4 ⊕ S4 for the Product Space R x R
    Kremer, Philip
    [J]. STUDIA LOGICA, 2015, 103 (01) : 219 - 226
  • [8] THE ILLINOIS PROVER - A GENERAL-PURPOSE RESOLUTION THEOREM PROVER
    GREENBAUM, S
    PLAISTED, DA
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1986, 230 : 685 - 686
  • [9] A Resolution Prover for Coalition Logic
    Nalon, Claudia
    Zhang, Lan
    Dixon, Clare
    Hustadt, Ullrich
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (146): : 65 - 73
  • [10] Intuitionistic S4 is decidable
    Girlando, Marianna
    Kuznets, Roman
    Marin, Sonia
    Morales, Marianela
    Strassburger, Lutz
    [J]. 2023 38TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, LICS, 2023,
12345