References

  1. Raymond Aubin (1979): Mechanizing Structural Induction Part II: Strategies. Theor. Comput. Sci. 9, pp. 347–362, doi:10.1016/0304-3975(79)90035-5.
  2. Siani Baker, Andrew Ireland & Alan Smaill (1992): On the Use of the Constructive Omega-Rule within Automated Deduction. In: LPAR'92, Lecture Notes in Computer Science 624. Springer, pp. 214–225, doi:10.1007/BFb0013063.
  3. Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes & Uwe Waldmann (2018): Superposition for Lambda-Free Higher-Order Logic. In: IJCAR, Lecture Notes in Computer Science 10900. Springer, pp. 28–46, doi:10.1007/978-3-319-94205-6_3.
  4. Ahmed Bhayat & Giles Reger (2020): A Combinator-Based Superposition Calculus for Higher-Order Logic. In: IJCAR, Lecture Notes in Computer Science 12166. Springer, pp. 278–296, doi:10.1007/978-3-030-51074-9_16.
  5. Ahmed Bhayat & Giles Reger (2020): A Polymorphic Vampire - (Short Paper). In: IJCAR, Lecture Notes in Computer Science 12167. Springer, pp. 361–368, doi:10.1007/978-3-030-51054-1_21.
  6. Koen Claessen, Moa Johansson, Dan Rosén & Nicholas Smallbone (2012): HipSpec: Automating Inductive Proofs of Program Properties. In: ATx'12/WInG'12, EPiC Series in Computing 17. EasyChair, pp. 16–25. Available at https://easychair.org/publications/paper/Kb7.
  7. Véronique Cortier, Niklas Grimm, Joseph Lallemand & Matteo Maffei (2018): Equivalence Properties by Typing in Cryptographic Branching Protocols. In: POST, Lecture Notes in Computer Science 10804. Springer, pp. 160–187, doi:10.1007/978-3-319-89722-6_7.
  8. Simon Cruanes (2017): Superposition with Structural Induction. In: FroCoS, Lecture Notes in Computer Science 10483. Springer, pp. 172–188, doi:10.1007/978-3-319-66167-4_10.
  9. Mnacho Echenim & Nicolas Peltier (2020): Combining Induction and Saturation-Based Theorem Proving. J. Autom. Reason. 64(2), pp. 253–294, doi:10.1007/s10817-019-09519-x.
  10. Yotam M. Y. Feldman, James R. Wilcox, Sharon Shoham & Mooly Sagiv (2019): Inferring Inductive Invariants from Phase Structures. In: CAV, Lecture Notes in Computer Science 11562. Springer, pp. 405–425, doi:10.1007/978-3-030-25543-5_23.
  11. Pamina Georgiou, Bernhard Gleiss & Laura Kovács (2020): Trace Logic for Inductive Loop Reasoning. CoRR abs/2008.01387, doi:10.34727/2020/isbn.978-3-85448-042-6_33.
  12. Márton Hajdú, Petra Hozzová, Laura Kovács, Johannes Schoisswohl & Andrei Voronkov (2020): Induction with Generalization in Superposition Reasoning. In: CICM, Lecture Notes in Computer Science 12236. Springer, pp. 123–137, doi:10.1007/978-3-030-53518-6_8.
  13. Krystof Hoder, Nikolaj Bjørner & Leonardo Mendonça de Moura (2011): μZ- An Efficient Engine for Fixed Points with Constraints. In: CAV, Lecture Notes in Computer Science 6806. Springer, pp. 457–462, doi:10.1007/978-3-642-22110-1_36.
  14. Gabriel Hondet & Frédéric Blanqui (2020): The New Rewriting Engine of Dedukti (System Description). In: Zena M. Ariola: FSCD, LIPIcs 167. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 35:1–35:16, doi:10.4230/LIPIcs.FSCD.2020.35.
  15. Leon Horsten (2011): The Tarskian Turn: Deflationism and Axiomatic Truth. Mit Press. MIT Press, doi:10.7551/mitpress/9780262015868.001.0001.
  16. Abdelkader Kersani & Nicolas Peltier (2013): Combining Superposition and Induction: A Practical Realization. In: FroCoS, Lecture Notes in Computer Science 8152. Springer, pp. 7–22, doi:10.1007/978-3-642-40885-4_2.
  17. Evgenii Kotelnikov, Laura Kovács, Giles Reger & Andrei Voronkov (2016): The vampire and the FOOL. In: CPP. ACM, pp. 37–48, doi:10.1145/2854065.2854071.
  18. Laura Kovács, Simon Robillard & Andrei Voronkov (2017): Coming to terms with quantified reasoning. In: POPL. ACM, pp. 260–270, doi:10.1145/3009837.3009887.
  19. Laura Kovács & Andrei Voronkov (2013): First-Order Theorem Proving and Vampire. In: CAV, Lecture Notes in Computer Science 8044. Springer, pp. 1–35, doi:10.1007/978-3-642-39799-8_1.
  20. K. Rustan M. Leino (2012): Automating Induction with an SMT Solver. In: VMCAI, Lecture Notes in Computer Science 7148. Springer, pp. 315–331, doi:10.1007/978-3-642-27940-9_21.
  21. J. Strother Moore (2019): Milestones from the Pure Lisp theorem prover to ACL2. Formal Aspects Comput. 31(6), pp. 699–732, doi:10.1007/s00165-019-00490-3.
  22. Lauren Pick, Grigory Fedyukovich & Aarti Gupta (2020): Automating Modular Verification of Secure Information Flow. In: FMCAD. IEEE, pp. 158–168, doi:10.34727/2020/isbn.978-3-85448-042-6_23.
  23. Giles Reger, Martin Suda & Andrei Voronkov (2018): Unification with Abstraction and Theory Instantiation in Saturation-Based Reasoning. In: TACAS, Lecture Notes in Computer Science 10805. Springer, pp. 3–22, doi:10.1007/978-3-319-89960-2_1.
  24. Giles Reger & Andrei Voronkov (2019): Induction in Saturation-Based Proof Search. In: CADE, Lecture Notes in Computer Science 11716. Springer, pp. 477–494, doi:10.1007/978-3-030-29436-6_28.
  25. Andrew Reynolds & Viktor Kuncak (2015): Induction for SMT Solvers. In: VMCAI, Lecture Notes in Computer Science 8931. Springer, pp. 80–98, doi:10.1007/978-3-662-46081-8_5.
  26. Johannes Schoisswohl & Laura Kovacs (2021): Automating Induction by Reflection. Available at https://arxiv.org/abs/2106.05066.
  27. Andrei Voronkov (2014): AVATAR: The Architecture for First-Order Theorem Provers. In: CAV, Lecture Notes in Computer Science 8559. Springer, pp. 696–710, doi:10.1007/978-3-319-08867-9_46.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org