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 条
  • [1] Learning to Integrate Deduction and Search in Reasoning about Quantified Boolean Formulas
    Pulina, Luca
    Tacchella, Armando
    [J]. FRONTIERS OF COMBINING SYSTEMS, PROCEEDINGS, 2009, 5749 : 350 - 365
  • [2] A Structural Approach to Reasoning with Quantified Boolean Formulas
    Pulina, Luca
    Tacchella, Armando
    [J]. 21ST INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI-09), PROCEEDINGS, 2009, : 596 - 602
  • [3] Reasoning in Argumentation Frameworks Using Quantified Boolean Formulas
    Egly, Uwe
    Woltran, Stefan
    [J]. COMPUTATIONAL MODELS OF ARGUMENT, 2006, 144 : 133 - 144
  • [4] Reasoning About Inconsistent Formulas
    Marques-Silva, Joao
    Mencia, Carlos
    [J]. PROCEEDINGS OF THE TWENTY-NINTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2020, : 4899 - 4906
  • [5] Solving advanced reasoning tasks using quantified Boolean formulas
    Egly, U
    Eiter, T
    Tompits, H
    Woltran, S
    [J]. SEVENTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE (AAAI-2001) / TWELFTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE (IAAI-2000), 2000, : 417 - 422
  • [6] Reasoning in Abstract Dialectical Frameworks Using Quantified Boolean Formulas
    Diller, Martin
    Wallner, Johannes Peter
    Woltran, Stefan
    [J]. COMPUTATIONAL MODELS OF ARGUMENT, 2014, 266 : 241 - 252
  • [7] Reasoning in abstract dialectical frameworks using quantified Boolean formulas
    Diller, Martin
    Wallner, Johannes Peter
    Woltran, Stefan
    [J]. ARGUMENT & COMPUTATION, 2015, 6 (02) : 149 - 177
  • [8] Propositional PSPACE reasoning with boolean programs versus quantified Boolean formulas
    Skelley, A
    [J]. AUTOMATA , LANGUAGES AND PROGRAMMING, PROCEEDINGS, 2004, 3142 : 1163 - 1175
  • [9] STUDENTS REASONING ABOUT THE SUPERPOSITION OF ELECTRIC-FIELDS
    VIENNOT, L
    RAINSON, S
    [J]. INTERNATIONAL JOURNAL OF SCIENCE EDUCATION, 1992, 14 (04) : 475 - 487
  • [10] Paraconsistent reasoning via quantified Boolean formulas, II: Circumscribing inconsistent theories
    Besnard, P
    Schaub, T
    Tompits, H
    Woltran, S
    [J]. SYMBOLIC AND QUANTITATIVE APPROACHES TO REASONING WITH UNCERTAINTY, PROCEEDING, 2003, 2711 : 528 - 539
12345