Raymond Aubin (1979):
Mechanizing Structural Induction Part II: Strategies.
Theor. Comput. Sci. 9,
pp. 347–362,
doi:10.1016/0304-3975(79)90035-5.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.