Page 61 - 《软件学报》2026年第2期

540 软件学报 2026 年第 37 卷第 2 期

[7] Shah A, Mora F, Seshia SA. An eager satisfiability modulo theories solver for algebraic datatypes. In: Proc. of the 38th AAAI Conf. on
Artificial Intelligence. Vancouver: AAAI Press, 2024. 8099–8107. [doi: 10.1609/aaai.v38i8.28649]
[8] Cruanes S. Superposition with structural induction. In: Proc. of the 11th Int’l Symp. on Frontiers of Combining Systems. Brasília:
Springer, 2017. 172–188. [doi: 10.1007/978-3-319-66167-4_10]
[9] Kovács L, Robillard S, Voronkov A. Coming to terms with quantified reasoning. In: Proc. of the 44th ACM SIGPLAN Symp. on
Principles of Programming Languages. Paris: ACM, 2017. 260–270. [doi: 10.1145/3009837.3009887]
[10] Cruanes S. Extending superposition with integer arithmetic, structural induction, and beyond [Ph.D. Thesis]. Palaiseau: École
Polytechnique, 2015.
[11] Kovács L, Voronkov A. First-order theorem proving and Vampire. In: Proc. of the 25th Int’l Conf. on Computer Aided Verification. Saint
Petersburg: Springer, 2013. 1–35. [doi: 10.1007/978-3-642-39799-8_1]
[12] De Angelis E, Fioravanti F, Pettorossi A, Proietti M. Removing algebraic data types from constrained Horn clauses using difference
predicates. In: Proc. of the 10th Int’l Joint Conf. on Automated Reasoning. Paris: Springer, 2020. 83–102. [doi: 10.1007/978-3-030-51074-
9_6]
[13] De Angelis E, Fioravanti F, Pettorossi A, Proietti M. Satisfiability of constrained Horn clauses on algebraic data types: A transformation-
based approach. Journal of Logic and Computation, 2022, 32(2): 402–442. [doi: 10.1093/logcom/exab090]
[14] Kostyukov Y, Mordvinov D, Fedyukovich G. Beyond the elementary representations of program invariants over algebraic data types. In:
Proc. of the 42nd ACM SIGPLAN Int’l Conf. on Programming Language Design and Implementation. ACM, 2021. 451–465. [doi: 10.
1145/3453483.3454055]
[15] Govind VKH, Shoham S, Gurfinkel A. Solving constrained Horn clauses modulo algebraic data types and recursive functions. Proc. of
the ACM on Programming Languages, 2022, 6(POPL): 60. [doi: 10.1145/3498722]
[16] Cook SA. The complexity of theorem-proving procedures. In: Proc. of the 3rd Annual ACM Symp. on Theory of Computing. Shaker
Heights: ACM, 1971. 151–158. [doi: 10.1145/800157.805047]
[17] Armando A, Giunchiglia E. Embedding complex decision procedures inside an interactive theorem prover. Annals of Mathematics and
Artificial Intelligence, 1993, 8(3-4): 475–502. [doi: 10.1007/BF01530803]
[18] Armando A, Castellini C, Giunchiglia E. SAT-based procedures for temporal reasoning. In: Proc. of the 5th European Conf. on Planning
Recent Advances in AI Planning. Durham: Springer, 2000. 97–108. [doi: 10.1007/10720246_8]
[19] Bryant RE, German S, Velev MN. Exploiting positive equality in a logic of equality with uninterpreted functions. In: Proc. of the 11th Int’l
Conf. on Computer Aided Verification. Trento: Springer, 1999. 470–482. [doi: 10.1007/3-540-48683-6_40]
[20] Giunchiglia F, Sebastiani R. Building decision procedures for modal logics from propositional decision procedures: The case study of
modal K(m). Information and Computation, 2000, 162(1–2): 158–178. [doi: 10.1006/inco.1999.2850]
[21] Ganzinger H, Hagen G, Nieuwenhuis R, Oliveras A, Tinelli C. DPLL(T): Fast decision procedures. In: Proc. of the 16th Int’l Conf. on
Computer Aided Verification. Boston: Springer, 2004. 175–188. [doi: 10.1007/978-3-540-27813-9_14]
[22] Dutertre B, de Moura L. A fast linear-arithmetic solver for DPLL(T). In: Proc. of the 18th Int’l Conf. on Computer Aided Verification.
Seattle: Springer, 2006. 81–94. [doi: 10.1007/11817963_11]
[23] de Moura L, Bjørner N. Z3: An efficient SMT solver. In: Proc. of the 14th Int’l Conf. on Held as Part of the Joint European Conf. on
Theory and Practice of Software Tools and Algorithms for the Construction and Analysis of Systems. Budapest: Springer, 2008. 337–340.
[doi: 10.1007/978-3-540-78800-3_24]
[24] Barbosa H, Barrett C, Brain M, Kremer G, Lachnitt H, Mann M, Mohamed A, Mohamed M, Niemetz A, Nötzli A, Ozdemir A, Preiner M,
Reynolds A, Sheng Y, Tinelli C, Zohar Y. cvc5: A versatile and industrial-strength SMT solver. In: Proc. of the 28th Int’l Conf. on Tools
and Algorithms for the Construction and Analysis of Systems. Munich: Springer, 2022. 415–442. [doi: 10.1007/978-3-030-99524-9_24]
[25] Brummayer R, Biere A. Boolector: An efficient SMT solver for bit-vectors and arrays. In: Proc. of the 15th Int’l Conf. on Tools and
Algorithms for the Construction and Analysis of Systems. York: Springer, 2009. 174–177. [doi: 10.1007/978-3-642-00768-2_16]
[26] Niemetz A, Preiner M, Wolf C, Biere A. BTOR2, BtorMC and boolector 3.0. In: Proc. of the 30th Int’l Conf. Computer Aided
Verification. Oxford: Springer, 2018. 587–595. [doi: 10.1007/978-3-319-96145-3_32]
[27] Nieuwenhuis R, Rubio A. Paramodulation-based theorem proving. Handbook of Automated Reasoning, 2001, 1: 371–443. [doi: 10.1016/
B978-044450813-3/50009-6]
[28] Reger G, Suda M, Voronkov A. Instantiation and pretending to be an SMT solver with Vampire. In: Proc. of the 15th Int’l Workshop on
Satisfiability Modulo Theories. Heidelberg: CEUR-WS.org, 2017. 63–75.
[29] Nelson G, Oppen DC. Fast decision procedures based on congruence closure. Journal of the ACM (JACM), 1980, 27(2): 356–364. [doi:
10.1145/322186.322198]