Skip to Main content Skip to Navigation
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 metadatas

https://hal.inria.fr/inria-00433745
Contributor : Helene Kirchner <>
Submitted on : Friday, November 20, 2009 - 9:40:39 AM
Last modification on : Thursday, March 5, 2020 - 6:22:02 PM
Long-term archiving on: : Tuesday, October 16, 2012 - 2:30:25 PM

File

strategic-3K.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

463

Files downloads

186