Anzeige
Erschienen in:
2004 | OriginalPaper | Buchkapitel
Everyday Logic
verfasst von : Dr. Yves Bertot, Dr. Pierre Castéran
Erschienen in: Interactive Theorem Proving and Program Development
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
The previous chapters show that the Calculus of Constructions is powerful enough as a type system for the representation of logical formulas and theorems. Interpreting types as formulas and terms as proofs works well and makes it possible to reduce the problem of verifying formal proofs to the problem of verifying that some terms are well-typed. This chapter takes a more pragmatic point of view and shows how we can use tactics to make the logical reasoning easier.