| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNINA9910457434803321 |
|
|
Autore |
Sørensen Morten Heine |
|
|
Titolo |
Lectures on the Curry-Howard isomorphism [[electronic resource] /] / Morten Heine Sørensen, Paweł Urzyczyn |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Amsterdam ; ; Boston [MA], : Elsevier, 2006 |
|
|
|
|
|
|
|
ISBN |
|
1-281-05105-5 |
9786611051051 |
0-08-047892-1 |
|
|
|
|
|
|
|
|
Edizione |
[1st ed.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (457 p.) |
|
|
|
|
|
|
Collana |
|
Studies in logic and the foundations of mathematics, , 0049-237X ; ; v. 149 |
|
|
|
|
|
|
|
|
Altri autori (Persone) |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Curry-Howard isomorphism |
Lambda calculus |
Proof theory |
Electronic books. |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Description based upon print version of record. |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references (p. 403-430) and index. |
|
|
|
|
|
|
Nota di contenuto |
|
Cover; Title Page; Copyright Page; Table of Contents; Chapter 1 Type-free Lambda-calculus; 1.1 A gentle introduction; 1.2 Pre-terms and Lambda-terms; 1.3 Reduction; 1.4 The Church-Rosser theorem; 1.5 Leftmost reductions are normalizing; 1.6 Perpetual reductions and the conservation theorem; 1.7 Expressibility and undeeidability; 1.8 Notes; 1.9 Exercises; Chapter 2 Intultionistic logic; 2.1 The BHK interpretation; 2.2 Natural deduction; 2.3 Algebraic semantics of classical logic; 2.4 Heyting algebras; 2.5 Kripke semantics; 2.6 The implicational fragment; 2.7 Notes; 2.8 Exercises |
Chapter 3 Simply typed Lambda-calcuIus3.1 Simply typed Lambda-ealculus a la Curry; 3.2 Type reconstruction algorithm; 3.3 Simply typed Lambda-calculus a la Church; 3.4 Church versus Curry typing; 3.5 Normalization; 3.6 Church-Rosser property; 3.7 Expressibility; 3.8 Notes; 3.9 Exercises; Chapter 4 The Curry-Howard isomorphism; 4.1 Proofs and terms; 4.2 Type inhabitation; 4.3 Not an exact isomorphism; 4.4 Proof normalization; 4.5 Sums and products; 4.6 Prover-skeptic dialogues; 4.7 Prover-skeptic dialogues with absurdity; 4.8 Notes; 4.9 |
|
|
|
|
|
|
|
|
|
|
|
Exercises; Chapter 5 Proofs as combinators |
5.1 Hubert style proofs5.2 Combinatory logic; 5.3 Typed combinators; 5.4 Combinators versus lambda terms; 5.5 Extensionality; 5.6 Relevance and linearity; 5.7 Notes; 5.8 Exercises; Chapter 6 Classical logic and control operators; 6.1 Classical prepositional lope; 6.2 The Lambda meu-calculus; 6.3 Subject reduction, confluence, strong normalization; 6.4 Logical embedding and CPS translation; 6.5 Classical prover-skeptic dialogues; 6.6 The pure implicational fragment; 6.7 Conjunction and disjunction; 6.8 Notes; 6.9 Exercises; Chapter 7 Sequent calculus; 7.1 Gentzen's sequent calculus LK |
7.2 Fragments of LK versus natural deduction7.3 Gentzen's Hauptaatz; 7.4 Cut elimination versus normalization; 7.5 Lorenzen dialogues; 7.6 Notes; 7.7 Exercises; Chapter 8 First-order logic; 8.1 Syntax of first-order logic; 8.2 Informal semantics; 8.3 Proof systems; 8.4 Classical semantics; 8.5 Algebraic semantics of intuitionistie logic; 8.6 Kripke semantics; 8.7 Lambda-calculus; 8.8 Undeddability; 8.9 Notes; 8.10 Exercises; Chapter 9 First-order arithmetic; 9.1 The language of arithmetic; 9.2 Peano Arithmetic; 9.3 Godel's theorems; 9.4 Representable and provably recursive functions |
9.5 Heyting Arithmetic9.6 Kleene's realfeability interpretation; 9.7 Notes; 9.8 Exercises; Chapter 10 Godel's system T; 10.1 From Heyting Arithmetic to system T; 10.2 Syntax; 10.3 Strong normalization; 10.4 Modified realizability; 10.5 Notes; 10.6 Exercises; Chapter 11 Second-order logic and polymorphism; 11.1 Prepositional second-order logic; 11.2 Polymorphic lambda-calculus (system F); 11.3 Expressive power; 11.4 Gurry-style polymorphism; 11.5 Strong normalization; 11.6 The inhabitation problem; 11.7 Higher-order polymorphism; 11.8 Notes; 11.9 Exercises |
Chapter 12 Second-order arithmetic |
|
|
|
|
|
|
Sommario/riassunto |
|
The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance,minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc.The isomorphism has many aspects, even at the syntactic level:formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNINA9910975313803321 |
|
|
Autore |
Bossé Éloi <1956-> |
|
|
Titolo |
Concepts, models, and tools for information fusion / / Eloi Bosse, Jean Roy, Steve Wark |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Norwood, MA, : Artech House, c2007 |
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (392 p.) |
|
|
|
|
|
|
Altri autori (Persone) |
|
|
|
|
|
|
|
|
Disciplina |
|
355.3 |
355.33041 |
355.3304103 |
|
|
|
|
|
|
|
|
Soggetti |
|
Command and control systems |
Information warfare |
Multisensor data fusion |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Description based upon print version of record. |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
Concepts, Models, and Tools for Information Fusion; Contents v; Foreword xiii; Chapter 1 Introduction 1; Chapter 2 Decision-Making Models 11; Chapter 3 Situation Awareness and Analysis Models 27; Chapter 4 Data- and Information-Fusion Models 69; Chapter 5 Situation Analysis and Decision-Support Systems 119; Chapter 6 Knowledge, Belief, and Uncertainty 141; Chapter 7 Qualitative and Symbolic Approaches 151; Chapter 8 Quantitative Approaches 169; Chapter 9 Hybrid and Graphical Approaches 211; Computational Aspects of Information Fusion 231. |
|
|
|
|
|
|
|
|
Sommario/riassunto |
|
In the heat of battle, a split second can be all the time a military commander has to give orders. Information fusion technology enables commanders to lead decisively and confidently during active conflict. Masses of live information are instantaneously integrated to create a coherent and precise picture of a rapidly evolving situation. This book brings together an international panel of leading experts that give a fresh and cohesive perspective on this technology's models, methods, mathematics, and computer systems. It considers the human factors key to the automated analysis process. Providi. |
|
|
|
|
|
|
|
| |