Tactics and Automation

  • Yves Bertot
  • Pierre Castéran
Part of the Texts in Theoretical Computer Science An EATCS Series book series (TTCS)


There are two parts to this chapter. The first part presents several collections of tactics specialized in various domains of logic and mathematics: tactics specialized in reasoning about inductive types, the main automatic tactics, which rely on a Prolog-like proof search mechanism, the tactics for equality and rewriting, the tactics for numerical proofs, and the automatic decision procedures for restricted fragments of logic.


Pattern Match Finished Transaction Choice Point Inductive Type Proof Search 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Yves Bertot
    • 1
  • Pierre Castéran
    • 2
  1. 1.Inria Sophia AntipolisSophia Antipolis CedexFrance
  2. 2.LaBRI and Inria Futurs LabRIUniversité Bordeaux ITalence CedexFrance

Personalised recommendations