Superposition Reasoning about Quantified Bitvector Formulas

被引：0
|
作者：
Damestani, David [1 ]
Kovacs, Laura [1 ,2 ]
Suda, Martin [3 ]
机构：
[1] TU Wien, Vienna, Austria
[2] Chalmers, Gothenburg, Sweden
[3] Czech Tech Univ, Prague, Czech Republic
来源：
2019 21ST INTERNATIONAL SYMPOSIUM ON SYMBOLIC AND NUMERIC ALGORITHMS FOR SCIENTIFIC COMPUTING (SYNASC 2019) | 2020年
关键词：
D O I：
10.1109/SYNASC49474.2019.00022
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We describe recent extensions to the first-order theorem prover Vampire for proving theorems in the theory of fixed-sized bitvectors, possibly with quantifiers. Details are given on extending both the parser of Vampire as well as the theory reasoning framework of Vampire. We present our experimental results by evaluating and comparing our approach to SMT solvers. Our experiments report also on a few examples that can be solved only by our work.
引用
收藏
页码：95 / 99
页数：5
相关论文
共 50 条
  • [21] Modular Reasoning about Heap Paths via Effectively Propositional Formulas
    Itzhaky, Shachar
    Banerjee, Anindya
    Immerman, Neil
    Lahav, Ori
    Nanevski, Aleksandar
    Sagiv, Mooly
    [J]. ACM SIGPLAN NOTICES, 2014, 49 (01) : 385 - 396
  • [22] Coming to Terms with Quantified Reasoning
    Kovacs, Laura
    Robillard, Simon
    Voronkov, Andrei
    [J]. ACM SIGPLAN NOTICES, 2017, 52 (01) : 260 - 270
  • [23] A Survey on Applications of Quantified Boolean Formulas
    Shukla, Ankit
    Biere, Armin
    Seidl, Martina
    Pulina, Luca
    [J]. 2019 IEEE 31ST INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2019), 2019, : 78 - 84
  • [24] Minimal false quantified Boolean formulas
    Buening, Hans Kleine
    Zhao, Xishun
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS, 2006, 4121 : 339 - 352
  • [25] Backdoor Sets of Quantified Boolean Formulas
    Samer, Marko
    Szeider, Stefan
    [J]. JOURNAL OF AUTOMATED REASONING, 2009, 42 (01) : 77 - 97
  • [26] RESOLUTION FOR QUANTIFIED BOOLEAN-FORMULAS
    BUNING, HK
    KARPINSKI, M
    FLOGEL, A
    [J]. INFORMATION AND COMPUTATION, 1995, 117 (01) : 12 - 18
  • [27] DECOMPOSING QUANTIFIED CONJUNCTIVE (OR DISJUNCTIVE) FORMULAS
    Chen, Hubie
    Dalmau, Victor
    [J]. SIAM JOURNAL ON COMPUTING, 2016, 45 (06) : 2066 - 2086
  • [28] Learnability of relatively quantified generalized formulas
    Bulatov, A
    Chen, HB
    Dalmau, V
    [J]. ALGORITHMIC LEARNING THEORY, PROCEEDINGS, 2004, 3244 : 365 - 379
  • [29] Backdoor sets of quantified Boolean formulas
    Samer, Marko
    Szeider, Stefan
    [J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2007, PROCEEDINGS, 2007, 4501 : 230 - +
  • [30] Decomposing Quantified Conjunctive (or Disjunctive) Formulas
    Chen, Hubie
    Dalmau, Victor
    [J]. 2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 205 - 214
12345