Strategic Computation and Deduction

Abstract : We introduce the notion of abstract strategies for abstract reduction systems. Adequate properties of termination, confluence and normalization under strategy can then be defined. Thanks to this abstract concept, we draw a parallel between strategies for computation and strategies for deduction. We define deduction rules as rewrite rules, a deduction step as a rewriting step and a proof construction step as a narrowing step in an adequate abstract reduction system. Computation, deduction and proof search are thus captured in the uniform foundational concept of abstract reduction system in which abstract strategies have a clear formalisation.
Type de document :
Chapitre d'ouvrage
Christoph Benzmüller and Chad E. Brown and Jörg Siekmann and Richard Statman. Reasoning in Simple Type Theory. Festchrift in Honour of Peter B. Andrews on His 70th Birthday, 17, College Publications, pp.339-364, 2008, Studies in Logic and the Foundations of Mathematics, 978-1-904987-70-3
Liste complète des métadonnées

https://hal.inria.fr/inria-00433745
Contributeur : Helene Kirchner <>
Soumis le : vendredi 20 novembre 2009 - 09:40:39
Dernière modification le : jeudi 11 janvier 2018 - 06:22:10
Document(s) archivé(s) le : mardi 16 octobre 2012 - 14:30:25

Fichier

strategic-3K.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00433745, version 1

Collections

Citation

Claude Kirchner, Florent Kirchner, Helene Kirchner. Strategic Computation and Deduction. Christoph Benzmüller and Chad E. Brown and Jörg Siekmann and Richard Statman. Reasoning in Simple Type Theory. Festchrift in Honour of Peter B. Andrews on His 70th Birthday, 17, College Publications, pp.339-364, 2008, Studies in Logic and the Foundations of Mathematics, 978-1-904987-70-3. 〈inria-00433745〉

Partager

Métriques

Consultations de la notice

330

Téléchargements de fichiers

119