References

  1. A. Armando, M. Rusinowitch & S. Stratulat (2002): Incorporating Decision Procedures in Implicit Induction. J. Symb. Comput. 34(4), pp. 241–258, doi:10.1006/jsco.2002.0549.
  2. G. Barthe & S. Stratulat (2003): Validation of the JavaCard Platform with Implicit Induction Techniques. In: R. Nieuwenhuis: RTA, Lecture Notes in Computer Science 2706. Springer, pp. 337–351, doi:10.1007/3-540-44881-0.08emwidth.35em height.6pt.08em24.
  3. A. Bouhoula, E. Kounalis & M. Rusinowitch (1995): Automated Mathematical Induction. Journal of Logic and Computation 5(5), pp. 631–668, doi:10.1093/logcom/5.5.631.
  4. R. Boulton & K. Slind (2000): Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions. In: J. Lloyd, V. Dahl, U. Furbach, M. Kerber, K.-K. Lau, C. Palamidessi, L. Pereira, Y. Sagiv & P. Stuckey: Computational Logic — CL 2000, Lecture Notes in Computer Science 1861. Springer Berlin / Heidelberg, pp. 629–643, doi:10.1007/3-540-44957-4.08emwidth.35em height.6pt.08em42.
  5. R. S. Boyer & J S. Moore (1988): A computational logic handbook. Academic Press Professional.
  6. R. S. Boyer & J S. Moore (1988): Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic. In: Machine Intelligence. Oxford University Press, Inc. New York, NY, USA, pp. 83–124.
  7. R. M. Burstall (1969): Proving properties of programs by structural induction. The Computer Journal 12, pp. 41–48, doi:10.1093/comjnl/12.1.41.
  8. E. Contejean, P. Courtieu, J. Forest, O. Pons & X. Urbain (2007): Certification of Automated Termination Proofs. Frontiers of Combining Systems, pp. 148–162, doi:10.1007/978-3-540-74621-8.08emwidth.35em height.6pt.08em10.
  9. J. Courant (1996): Proof reconstruction. Research Report RR96-26. LIP. Preliminary version.
  10. D. Delahaye (2000): A Tactic Language for the System Coq. In: M. Parigot & A. Voronkov: Logic for Programming and Automated Reasoning (LPAR), Lecture Notes in Computer Science (LNCS) 1955. Springer, Reunion Island (France), pp. 85–95, doi:10.1007/3-540-44404-1.08emwidth.35em height.6pt.08em7.
  11. B. Gramlich (2005): Strategic Issues, Problems and Challenges in Inductive Theorem Proving. Electronic Notes in Theoretical Computer Science 125(2), pp. 5–43, doi:10.1016/j.entcs.2005.01.006.
  12. D. Kapur & M. Subramaniam (1996): Automating induction over mutually recursive functions. In: Algebraic Methodology and Software Technology, LNCS 1101. Springer, pp. 117–131, doi:10.1007/BFb0014311.
  13. D.E. Knuth & P.B. Bendix (1970): Simple word problems in universal algebras. In: Computational Problems in Abstract Algebra, pp. 263–297.
  14. X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy & J. Vouillon: The Objective Caml system - release 3.12. Documentation and user's manual. INRIA.
  15. D. R. Musser (1980): On Proving Inductive Properties of Abstract Data Types. In: POPL, pp. 154–162, doi:10.1145/567446.567461.
  16. M. Protzen (1994): Lazy generation of induction hypotheses. Automated Deduction —CADE-12, pp. 42–56, doi:10.1007/3-540-58156-1.08emwidth.35em height.6pt.08em4.
  17. M. Rusinowitch, S. Stratulat & F. Klay (2003): Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm. J. Autom. Reasoning 30(2), pp. 53–177, doi:10.1023/A:1023251327012.
  18. N. Shankar, S. Owre, J. M. Rushby & D. W. J. Stringer-Calvert (2001): PVS prover guide - version 2.4. SRI International.
  19. S. Stratulat (2001): A General Framework to Build Contextual Cover Set Induction Provers. J. Symb. Comput. 32(4), pp. 403–445, doi:10.1006/jsco.2000.0469.
  20. S. Stratulat (2010): Integrating Implicit Induction Proofs into Certified Proof Environments. In: Integrated Formal Methods, Lecture Notes in Computer Science 6396, pp. 320–335, doi:10.1007/978-3-642-16265-7.08emwidth.35em height.6pt.08em23.
  21. S. Stratulat (2012): A Unified View of Induction Reasoning for First-Order Logic. In: A. Voronkov: Turing-100 (The Alan Turing Centenary Conference), EPiC Series 10. EasyChair, pp. 326–352.
  22. S. Stratulat & V. Demange (2011): Automated Certification of Implicit Induction Proofs. In: CPP'2011 (First International Conference on Certified Programs and Proofs), Lecture Notes Computer Science 7086. Springer-Verlag, pp. 37–53, doi:10.1007/978-3-642-25379-9.08emwidth.35em height.6pt.08em5.
  23. The Coq Development Team (2009): The Coq Reference Manual - version 8.2. Available at http://coq.inria.fr/doc.
  24. R. Voicu & M. Li (2009): Descente Infinie Proofs in Coq. In: The 1st Coq Workshop, pp. 12 pages.
  25. C.-P. Wirth (2004): Descente Infinie + Deduction. Logic Journal of the IGPL 12(1), pp. 1–96, doi:10.1093/jigpal/12.1.1.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org