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 条

[31] 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
[32] Message passing for quantified Boolean formulas
Zhang, Pan
Ramezanpour, Abolfazl
Zdeborova, Lenka
Zecchina, Riccardo
[J]. JOURNAL OF STATISTICAL MECHANICS-THEORY AND EXPERIMENT, 2012,
[33] Backdoor Sets of Quantified Boolean Formulas
Marko Samer
Stefan Szeider
[J]. Journal of Automated Reasoning, 2009, 42 : 77 - 97
[34] NONLINEAR EQUATIONS WITH SUPERPOSITION FORMULAS AND EXCEPTIONAL GROUP G2 .3. THE SUPERPOSITION FORMULAS
GAGNON, L
HUSSIN, V
WINTERNITZ, P
[J]. JOURNAL OF MATHEMATICAL PHYSICS, 1988, 29 (10) : 2145 - 2155
[35] On Unordered BDDs and Quantified Boolean Formulas
Janota, Mikolas
[J]. PROGRESS IN ARTIFICIAL INTELLIGENCE, PT II, 2019, 11805 : 501 - 507
[36] Equivalence models for quantified Boolean formulas
Büning, HK
Zhao, XS
[J]. THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, 2005, 3542 : 224 - 234
[37] Induction with Generalization in Superposition Reasoning
Hajdu, Marton
Hozzova, Petra
Kovacs, Laura
Schoisswohl, Johannes
Voronkov, Andrei
[J]. INTELLIGENT COMPUTER MATHEMATICS, CICM 2020, 2020, 12236 : 123 - 137
[38] A Superposition Calculus for Abductive Reasoning
Echenim, M.
Peltier, N.
[J]. JOURNAL OF AUTOMATED REASONING, 2016, 57 (02) : 97 - 134
[39] A Superposition Calculus for Abductive Reasoning
M. Echenim
N. Peltier
[J]. Journal of Automated Reasoning, 2016, 57 : 97 - 134
[40] Semantic reasoning study for rough logic about n-ary formulas
Yan, Lin
Wang, Sui-Hua
Zhang, Xue-Dong
[J]. 2006 IEEE INTERNATIONAL CONFERENCE ON GRANULAR COMPUTING, 2006, : 381 - +

← 1 2 3 4 5 →