Skip to Main content Skip to Navigation
New interface
Book sections

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.
Document type :
Book sections
Complete list of metadata
Contributor : Helene Kirchner Connect in order to contact the contributor
Submitted on : Friday, November 20, 2009 - 9:40:39 AM
Last modification on : Wednesday, February 2, 2022 - 3:51:46 PM
Long-term archiving on: : Tuesday, October 16, 2012 - 2:30:25 PM


Files produced by the author(s)


  • HAL Id : inria-00433745, version 1



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⟩



Record views


Files downloads