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.
Type de document :
Ouvrage (y compris édition critique et traduction)
Elsevier, 350 p, 1998
Liste complète des métadonnées

Contributeur : Publications Loria <>
Soumis le : lundi 25 septembre 2006 - 17:03:53
Dernière modification le : mardi 24 avril 2018 - 13:34:56


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



Consultations de la notice