HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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 :
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Monday, September 25, 2006 - 5:03:53 PM
Last modification on : Wednesday, May 12, 2021 - 4:56:04 PM


  • HAL Id : inria-00098603, version 1



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



Record views