SAT-Enhanced MIZAR Proof Checking

被引：0
|
作者：
Naumowicz, Adam [1 ]
机构：
[1] Univ Bialystok, Inst Informat, Sosnowa 64, PL-15887 Bialystok, Poland
来源：
INTELLIGENT COMPUTER MATHEMATICS, CICM 2014 | 2014年 / 8543卷
关键词：
Mizar; SAT; Boolean operations;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
In this paper we present an experimental extension of the MIZAR system employing an external SAT solver to strengthen the notion of obviousness of the MIZAR proof checker. The presented extension is based on a version of MiniSAT, called Logic2CNF. The SAT-enhanced MIZAR checker is programmed to automatically spawn a new Logc2CNF process whenever it needs to justify any goal that involves equalities based on Boolean operations.
引用
收藏
页码：449 / 452
页数：4
相关论文
共 50 条
  • [1] Automating Boolean Set Operations in Mizar Proof Checking with the Aid of an External SAT Solver
    Naumowicz, Adam
    JOURNAL OF AUTOMATED REASONING, 2015, 55 (03) : 285 - 294
  • [2] Automating Boolean Set Operations in Mizar Proof Checking with the Aid of an External SAT Solver
    Adam Naumowicz
    Journal of Automated Reasoning, 2015, 55 : 285 - 294
  • [3] Interfacing external CA systems for Grobner bases computation in MIZAR proof checking
    Naumowicz, Adam
    INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, 2010, 87 (01) : 1 - 11
  • [4] Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking
    Darbari, Ashish
    Fischer, Bernd
    Marques-Silva, Joao
    THEORETICAL ASPECTS OF COMPUTING, 2010, 6255 : 260 - +
  • [5] The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
    Bancerek, Grzegorz
    Bylinski, Czeslaw
    Grabowski, Adam
    Kornilowicz, Artur
    Matuszewski, Roman
    Naumowicz, Adam
    Pak, Karol
    JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) : 9 - 32
  • [6] The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
    Grzegorz Bancerek
    Czesław Byliński
    Adam Grabowski
    Artur Korniłowicz
    Roman Matuszewski
    Adam Naumowicz
    Karol Pąk
    Journal of Automated Reasoning, 2018, 61 : 9 - 32
  • [7] Automated Improving of Proof Legibility in the Mizar System
    Pak, Karol
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2014, 2014, 8543 : 373 - 387
  • [8] A universal parallel SAT checking kernel
    Blochinger, W
    Sinz, C
    Küchlin, W
    PDPTA'03: PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON PARALLEL AND DISTRIBUTED PROCESSING TECHNIQUES AND APPLICATIONS, VOLS 1-4, 2003, : 1720 - 1725
  • [9] A technique for checking the CSP sat property
    Martin, JMR
    Jassim, SA
    ARCHITECTURES, LANGUAGES AND PATTERNS FOR PARALLEL AND DISTRIBUTED APPLICATIONS, 1998, 52 : 93 - 110
  • [10] Using SAT for combinational equivalence checking
    Goldberg, EI
    Prasad, MR
    Brayton, RK
    DESIGN, AUTOMATION AND TEST IN EUROPE, CONFERENCE AND EXHIBITION 2001, PROCEEDINGS, 2001, : 114 - 121
12345