Basic proof theory / Troelstra, A.

Public ISBD Titre : Basic proof theory Type de document : texte imprimé Auteurs : Troelstra, A. ; Schwichtenberg, H. Mention d'édition : 2nd ed. Editeur : Cambridge : Cambridge University Press Année de publication : 2000 Collection : Cambridge Tracts in Computer Sciences num. 43 Importance : xii - 417 p. ISBN/ISSN/EAN : 978-0-521-77911-1 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-01 Instructional exposition (textbooks, tutorial papers, etc.) 03-XX Mathematical logic and foundations:03-02 Research exposition (monographs, survey articles) 03-XX Mathematical logic and foundations:03BXX General logic:03B40 Combinatory logic and lambda-calculus 03-XX Mathematical logic and foundations:03BXX General logic:03B45 Modal logic 03-XX Mathematical logic and foundations:03BXX General logic:03B70 Logic in computer science 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F03 Proof theory, general 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F05 Cut-elimination and normal-form theorems 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F30 First-order arithmetic and fragments 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F35 Second- and higher-order arithmetic and fragments 03-XX Mathematical logic and foundations:03GXX Algebraic logic:03G30 Categorical logic, topoi 68-XX Computer science :68NXX Software:68N17 Logic programming Mots-clés : apartness  e-logic  multi-succedent intuitionistic sequent calculus  kleene-style sequent calculus  logic programming  connections with computer science  first-order arithmetic  modal logic  hilbert-style system  resolution  second-order heyting arithmetic  linear logic  coherence theorem  categorical logic  formulas-as-types relation  combinatory logic  type theory  interpolation  strong normalization  cut elimination  gentzen type system  sequent calculus  natural deduction system  intuitionistic logic  classical logic  minimal logic  proof theory Index. décimale : 03C Monographie Basic proof theory [texte imprimé] / Troelstra, A. ; Schwichtenberg, H.  . -  2nd ed. . - Cambridge : Cambridge University Press, 2000 . - xii - 417 p.. - (Cambridge Tracts in Computer Sciences; 43) . ISBN : 978-0-521-77911-1 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-01 Instructional exposition (textbooks, tutorial papers, etc.) 03-XX Mathematical logic and foundations:03-02 Research exposition (monographs, survey articles) 03-XX Mathematical logic and foundations:03BXX General logic:03B40 Combinatory logic and lambda-calculus 03-XX Mathematical logic and foundations:03BXX General logic:03B45 Modal logic 03-XX Mathematical logic and foundations:03BXX General logic:03B70 Logic in computer science 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F03 Proof theory, general 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F05 Cut-elimination and normal-form theorems 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F30 First-order arithmetic and fragments 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F35 Second- and higher-order arithmetic and fragments 03-XX Mathematical logic and foundations:03GXX Algebraic logic:03G30 Categorical logic, topoi 68-XX Computer science :68NXX Software:68N17 Logic programming Mots-clés : apartness  e-logic  multi-succedent intuitionistic sequent calculus  kleene-style sequent calculus  logic programming  connections with computer science  first-order arithmetic  modal logic  hilbert-style system  resolution  second-order heyting arithmetic  linear logic  coherence theorem  categorical logic  formulas-as-types relation  combinatory logic  type theory  interpolation  strong normalization  cut elimination  gentzen type system  sequent calculus  natural deduction system  intuitionistic logic  classical logic  minimal logic  proof theory Index. décimale : 03C Monographie

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
13412	03C02	imprimé / autre	CRDM	03/MATHEMATICAL LOGIC AND FOUNDATIONS	Disponible

Interactive models of computation and program behavior / Pierre-Louis Curien

Public ISBD Titre : Interactive models of computation and program behavior Type de document : texte imprimé Auteurs : Pierre-Louis Curien, Auteur ; Hugo Herbelin, Auteur ; Krivine, Jean-Louis, Auteur Editeur : Paris : Société mathématique de France Année de publication : 2009 Collection : Panoramas et synthèses, ISSN 1272-3835 num. 27 Importance : xvi, 275 p. Présentation : fig. Format : 24 cm ISBN/ISSN/EAN : 978-2-85629-273-0 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F05 Cut-elimination and normal-form theorems 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F52 Linear logic and other substructural logics 68-XX Computer science :68QXX Theory of computing:68Q55 Semantics Mots-clés : proof theory  realisability  abstract machines  linear logic  game semantics Index. décimale : 03B Publication collective Interactive models of computation and program behavior [texte imprimé] / Pierre-Louis Curien, Auteur ; Hugo Herbelin, Auteur ; Krivine, Jean-Louis, Auteur . - Paris : Société mathématique de France, 2009 . - xvi, 275 p. : fig. ; 24 cm. - (Panoramas et synthèses, ISSN 1272-3835; 27) . ISBN : 978-2-85629-273-0 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F05 Cut-elimination and normal-form theorems 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F52 Linear logic and other substructural logics 68-XX Computer science :68QXX Theory of computing:68Q55 Semantics Mots-clés : proof theory  realisability  abstract machines  linear logic  game semantics Index. décimale : 03B Publication collective

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
18890	03B18	imprimé / autre	CRDM	03/MATHEMATICAL LOGIC AND FOUNDATIONS	Disponible
21864	03B18	imprimé / autre	CRDM	03/MATHEMATICAL LOGIC AND FOUNDATIONS	Disponible

Iterated inductive definitions and subsystems of analysis : recent proof- theoretical studies. / W. Buchholz

Public ISBD Titre : Iterated inductive definitions and subsystems of analysis : recent proof- theoretical studies. Type de document : texte imprimé Auteurs : W. Buchholz ; Feferman, S. Pohlers, W. Editeur : Springer-Verlag Année de publication : 1981 Collection : Lecture Notes in Mathematics, ISSN 0075-8434 num. 897 Importance : v - 383 p. ISBN/ISSN/EAN : 978-0-387-11170-4 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-02 Research exposition (monographs, survey articles) 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F05 Cut-elimination and normal-form theorems 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F10 Functionals in proof theory Mots-clés : predicative theories  virtual well-orderings  spectrum of a theory  collapsing functions  method of local predicativity  accessibility operator  negative arithmetic sentences  logical reflection principle  mathematical reflection principle  set-theoretic models  intuitionistic theories  inductively defined accessibility class  inductive generation  constructive theory of functions and classes  double-negation translation  impredicative subsystems of analysis  inductively defined classes Index. décimale : LNM Iterated inductive definitions and subsystems of analysis : recent proof- theoretical studies. [texte imprimé] / W. Buchholz ; Feferman, S. Pohlers, W. . - [S.l.] : Springer-Verlag, 1981 . - v - 383 p.. - (Lecture Notes in Mathematics, ISSN 0075-8434; 897) . ISBN : 978-0-387-11170-4 Langues : Anglais Catégories : 03-XX Mathematical logic and foundations:03-02 Research exposition (monographs, survey articles) 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F05 Cut-elimination and normal-form theorems 03-XX Mathematical logic and foundations:03FXX Proof theory and constructive mathematics:03F10 Functionals in proof theory Mots-clés : predicative theories  virtual well-orderings  spectrum of a theory  collapsing functions  method of local predicativity  accessibility operator  negative arithmetic sentences  logical reflection principle  mathematical reflection principle  set-theoretic models  intuitionistic theories  inductively defined accessibility class  inductive generation  constructive theory of functions and classes  double-negation translation  impredicative subsystems of analysis  inductively defined classes Index. décimale : LNM

Exemplaires

Code-barres	Cote	Support	Localisation	Section	Disponibilité
5387	LNM/897	imprimé / autre	CRDM	LNM/LECTURES NOTES IN MATHEMATICS	Disponible

---

page 1/1