Skip to Main content Skip to Navigation
Books

Special Issue of Theoretical Computer Science (TCS) Proof-search in Type-theoretic Languages

Didier Galmiche 1 David Pym
1 TYPES - Logic, proof Theory and Programming
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Algorithmic proof-search is a fundamental enabling technology throughout artificial intelligence and computer science. There is a long history of work in proof-search in a variety of systems of logic, including classical, intuitionistic, relevant, linear and modal systems, at the propositional, first- and higher-order levels. Such work has ranged from the most abstract to the most practical and has employed the full spectrum of logical techniques, from proof theory, model theory and recursion theory. From the computational point of view, the type-theoretic component of logical languages, which may involve propositional, first-order, higher-order or polymorphic assignment regimes, introduces significant challenges for both theoreticians and implementors.
Document type :
Books
Complete list of metadata

https://hal.inria.fr/inria-00098603
Contributor : Publications Loria <>
Submitted on : Monday, September 25, 2006 - 5:03:53 PM
Last modification on : Friday, February 26, 2021 - 3:28:08 PM

Identifiers

  • HAL Id : inria-00098603, version 1

Collections

Citation

Didier Galmiche, David Pym. Special Issue of Theoretical Computer Science (TCS) Proof-search in Type-theoretic Languages. Elsevier, 350 p, 1998. ⟨inria-00098603⟩

Share

Metrics

Record views

119