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 : Wednesday, March 27, 2019 - 4:41:26 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

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

416

Files downloads

145