Info
- Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.
12 × 12 Schlüsselkonzepte zur Mathematik [[electronic resource] /] / von Oliver Deiser, Caroline Lasser, Elmar Vogt, Dirk Werner
| 12 × 12 Schlüsselkonzepte zur Mathematik [[electronic resource] /] / von Oliver Deiser, Caroline Lasser, Elmar Vogt, Dirk Werner |
| Autore | Deiser Oliver |
| Edizione | [2nd ed. 2016.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer Spektrum, , 2016 |
| Descrizione fisica | 1 online resource (XIII, 355 S. 44 Abb., 1 Abb. in Farbe.) |
| Disciplina | 515 |
| Soggetto topico |
Mathematical analysis
Analysis (Mathematics) Matrix theory Algebra Discrete mathematics Mathematical logic Analysis Linear and Multilinear Algebras, Matrix Theory Discrete Mathematics Mathematical Logic and Foundations |
| ISBN | 3-662-47077-2 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | ger |
| Nota di contenuto | 1 Grundlagen -- 2 Zahlen -- 3 Zahlentheorie -- 4 Diskrete Mathematik -- 5 Lineare Algebra -- 6 Algebra -- 7 Elementare Analysis -- 8 Höhere Analysis -- 9 Topologie und Geometrie -- 10 Numerik -- 11 Stochastik -- 12 Mengenlehre und Logik -- Index. |
| Record Nr. | UNINA-9910484823003321 |
Deiser Oliver
|
||
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer Spektrum, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
8th International Conference on Automated Deduction [[electronic resource] ] : Oxford, England, July 27- August 1, 1986. Proceedings / / edited by Jörg H. Siekmann
| 8th International Conference on Automated Deduction [[electronic resource] ] : Oxford, England, July 27- August 1, 1986. Proceedings / / edited by Jörg H. Siekmann |
| Edizione | [1st ed. 1986.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1986 |
| Descrizione fisica | 1 online resource (XII, 716 p.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Mathematical logic
Artificial intelligence Mathematical Logic and Foundations Mathematical Logic and Formal Languages Artificial Intelligence |
| ISBN | 3-540-39861-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Connections and higher-order logic -- Commutation, transformation, and termination -- Full-commutation and fair-termination in equational (and combined) term-rewriting systems -- An actual implementation of a procedure that mechanically proves termination of rewriting systems based on inequalities between polynomial interpretations -- Proving termination of associative commutative rewriting systems by rewriting -- Relating resolution and algebraic completion for Horn logic -- A simple non-termination test for the Knuth-Bendix method -- A new formula for the execution of categorical combinators -- Proof by induction using test sets -- How to prove equivalence of term rewriting systems without induction -- Sufficient completeness, term rewriting systems and ”anti-unification” -- A new method for establishing refutational completeness in theorem proving -- A theory of diagnosis from first principles -- Some contributions to the logical analysis of circumscription -- Modal theorem proving -- Computational aspects of three-valued logic -- Resolution and quantified epistemic logics -- A commonsense theory of nonmonotonic reasoning -- Negative paramodulation -- The heuristics and experimental results of a new hyperparamodulation: HL-resolution -- ECR: An equality conditional resolution proof procedure -- Using narrowing to do isolation in symbolic equation solving — an experiment in automated reasoning -- Formulation of induction formulas in verification of prolog programs -- Program verifier "Tatzelwurm": Reasoning about systems systems of linear inequalities -- An interactive verification system based on dynamic logic -- What you always wanted to know about clause graph resolution -- Parallel theorem proving with connection graphs -- Theory links in semantic graphs -- Abstraction using generalization functions -- An improvement of deduction plans: Refutation plans -- Controlling deduction with proof condensation and heuristics -- Nested resolution -- Mechanizing constructive proofs -- Implementing number theory: An experiment with Nuprl -- Parallel algorithms for term matching -- Unification in combinations of collapse-free theories with disjoint sets of function symbols -- Combination of unification algorithms -- Unification in the data structure sets -- NP-completeness of the set unification and matching problems -- Matching with distributivity -- Unification in boolean rings -- Some relationships between unification, restricted unification, and matching -- A classification of many-sorted unification problems -- Unification in many-sorted equational theories -- Classes of first order formulas under various satisfiability definitions -- Diamond formulas in the dynamic logic of recursively enumerable programs -- A prolog machine -- A prolog technology theorem prover: Implementation by an extended prolog compiler -- Paths to high-performance automated theorem proving -- Purely functional implementation of a logic -- Causes for events: Their computation and applications -- How to clear a block: Plan formation in situational logic -- Deductive synthesis of sorting programs -- The TPS theorem proving system -- Trspec: A term rewriting based system for algebraic specifications -- Highly parallel inference machine -- Automatic theorem proving in the ISDV system -- The karlsruhe induction theorem proving system -- Overview of a theorem-prover for a computational logic -- GEO-prover — A geometry theorem prover developed at UT -- The markgraf karl refutation procedure (MKRP) -- The J-machine: Functional programming with combinators -- The illinois prover: A general purpose resolution theorem prover -- Theorem proving systems of the Formel project -- The passau RAP system: Prototyping algebraic specifications using conditional narrowing -- RRL: A rewrite rule laboratory -- A geometry theorem prover based on Buchberger's algorithm -- REVE a rewrite rule laboratory -- ITP at argonne national laboratory -- Autologic at university of victoria -- Thinker -- The KLAUS automated deduction system -- The KRIPKE automated theorem proving system -- SHD-prover at university of texas at austin. |
| Record Nr. | UNISA-996465940003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1986 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
9th International Conference on Automated Deduction [[electronic resource] ] : Argonne, Illinois, USA, May 23-26, 1988. Proceedings / / edited by Ewing Lusk, Ross Overbeek
| 9th International Conference on Automated Deduction [[electronic resource] ] : Argonne, Illinois, USA, May 23-26, 1988. Proceedings / / edited by Ewing Lusk, Ross Overbeek |
| Edizione | [1st ed. 1988.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1988 |
| Descrizione fisica | 1 online resource (X, 776 p.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Mathematical logic
Mathematical Logic and Foundations Mathematical Logic and Formal Languages |
| ISBN | 3-540-39216-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | First-order theorem proving using conditional rewrite rules -- Elements of Z-module reasoning -- Learning and applying generalised solutions using higher order resolution -- Specifying theorem provers in a higher-order logic programming language -- Query processing in quantitative logic programming -- An environment for automated reasoning about partial functions -- The use of explicit plans to guide inductive proofs -- Logicalc: An environment for interactive proof development -- Implementing verification strategies in the KIV-system -- Checking natural language proofs -- Consistency of rule-based expert systems -- A mechanizable induction principle for equational specifications -- Finding canonical rewriting systems equivalent to a finite set of ground equations in polynomial time -- Towards efficient "knowledge-based" automated theorem proving for non-standard logics -- Propositional temporal interval logic is PSPACE complete -- Computational metatheory in Nuprl -- Type inference in Prolog -- Procedural interpretation of non-horn logic programs -- Recursive query answering with non-horn clauses -- Case inference in resolution-based languages -- Notes on Prolog program transformations, Prolog style, and efficient compilation to the Warren abstract machine -- Exploitation of parallelism in prototypical deduction problems -- A decision procedure for unquantified formulas of graph theory -- Adventures in associative-commutative unification (A summary) -- Unification in finite algebras is unitary(?) -- Unification in a combination of arbitrary disjoint equational theories -- Partial unification for graph based equational reasoning -- SATCHMO: A theorem prover implemented in Prolog -- Term rewriting: Some experimental results -- Analogical reasoning and proof discovery -- Hyper-chaining and knowledge-based theorem proving -- Linear modal deductions -- A resolution calculus for modal logics -- Solving disequations in equational theories -- On word problems in Horn theories -- Canonical conditional rewrite systems -- Program synthesis by completion with dependent subtypes -- Reasoning about systems of linear inequalities -- A subsumption algorithm based on characteristic matrices -- A restriction of factoring in binary resolution -- Supposition-based logic for automated nonmonotonic reasoning -- Argument-bounded algorithms as a basis for automated termination proofs -- Two automated methods in implementation proofs -- A new approach to universal unfication and its application to AC-unification -- An implementation of a dissolution-based system employing theory links -- Decision procedure for autoepistemic logic -- Logical matrix generation and testing -- Optimal time bounds for parallel term matching -- Challenge equality problems in lattice theory -- Single axioms in the implicational propositional calculus -- Challenge problems focusing on equality and combinatory logic: Evaluating automated theorem-proving programs -- Challenge problems from nonassociative rings for theorem provers -- An interactive enhancement to the Boyer-Moore theorem prover -- A goal directed theorem prover -- m-NEVER system summary -- EFS — An interactive Environment for Formal Systems -- Ontic: A knowledge representation system for mathematics -- Some tools for an inference laboratory (ATINF) -- Quantlog: A system for approximate reasoning in inconsistent formal systems -- LP: The larch prover -- The KLAUS automated deduction system -- A Prolog technology theorem prover -- ?Prolog: An extended logic programming language -- SYMEVAL: A theorem prover based on the experimental logic -- ZPLAN: An automatic reasoning system for situations -- The TPS theorem proving system -- MOLOG: A modal PROLOG -- PARTHENON: A parallel theorem prover for non-horn clauses -- An nH-Prolog implementation -- RRL: A rewrite rule laboratory -- Geometer: A theorem prover for algebraic geometry -- Isabelle: The next seven hundred theorem provers -- The CHIP system : Constraint handling in Prolog. |
| Record Nr. | UNISA-996465689403316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1988 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Abstract State Machines 2004. Advances in Theory and Practice [[electronic resource] ] : 11th International Workshop, ASM 2004, Lutherstadt Wittenberg, Germany, May 24-28, 2004. Proceedings / / edited by Wolf Zimmermann, Bernhard Thalheim
| Abstract State Machines 2004. Advances in Theory and Practice [[electronic resource] ] : 11th International Workshop, ASM 2004, Lutherstadt Wittenberg, Germany, May 24-28, 2004. Proceedings / / edited by Wolf Zimmermann, Bernhard Thalheim |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (XII, 240 p.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Mathematical logic Computers Software engineering Programming languages (Electronic computers) Logics and Meanings of Programs Mathematical Logic and Foundations Theory of Computation Software Engineering Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters |
| ISBN |
1-280-30768-4
9786610307685 3-540-24773-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Intra-step Interaction -- Closed-Loop Modeling and Related Problems of Embedded Control Systems in Engineering -- An ALGOL-View on Turbo ASM -- An ASM Specification of C# Threads and the .NET Memory Model -- Finite Cursor Machines in Database Query Processing -- Research Papers -- Formalizing Liveness-Enriched Sequence Diagrams Using ASMs -- Specification and Validation of the Business Process Execution Language for Web Services -- Monodic ASMs and Temporal Verification -- Towards an Interchange Language for ASMs -- Specification and Implementation Problems for C# -- An ASM Semantics for SSA Intermediate Representations -- Observations on the Decidability of Transitions -- A Security Logic for Abstract State Machines -- Slicing Abstract State Machines -- The Cryptographic Abstract Machine -- Modeling Discretely Timed Systems Using Different Magnitudes of Non-standard Reals. |
| Record Nr. | UNINA-9910144158603321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Abstract State Machines 2004. Advances in Theory and Practice [[electronic resource] ] : 11th International Workshop, ASM 2004, Lutherstadt Wittenberg, Germany, May 24-28, 2004. Proceedings / / edited by Wolf Zimmermann, Bernhard Thalheim
| Abstract State Machines 2004. Advances in Theory and Practice [[electronic resource] ] : 11th International Workshop, ASM 2004, Lutherstadt Wittenberg, Germany, May 24-28, 2004. Proceedings / / edited by Wolf Zimmermann, Bernhard Thalheim |
| Edizione | [1st ed. 2004.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 |
| Descrizione fisica | 1 online resource (XII, 240 p.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computer logic
Mathematical logic Computers Software engineering Programming languages (Electronic computers) Logics and Meanings of Programs Mathematical Logic and Foundations Theory of Computation Software Engineering Mathematical Logic and Formal Languages Programming Languages, Compilers, Interpreters |
| ISBN |
1-280-30768-4
9786610307685 3-540-24773-4 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Intra-step Interaction -- Closed-Loop Modeling and Related Problems of Embedded Control Systems in Engineering -- An ALGOL-View on Turbo ASM -- An ASM Specification of C# Threads and the .NET Memory Model -- Finite Cursor Machines in Database Query Processing -- Research Papers -- Formalizing Liveness-Enriched Sequence Diagrams Using ASMs -- Specification and Validation of the Business Process Execution Language for Web Services -- Monodic ASMs and Temporal Verification -- Towards an Interchange Language for ASMs -- Specification and Implementation Problems for C# -- An ASM Semantics for SSA Intermediate Representations -- Observations on the Decidability of Transitions -- A Security Logic for Abstract State Machines -- Slicing Abstract State Machines -- The Cryptographic Abstract Machine -- Modeling Discretely Timed Systems Using Different Magnitudes of Non-standard Reals. |
| Record Nr. | UNISA-996466226603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2004 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
An Accompaniment to Higher Mathematics [[electronic resource] /] / by George R. Exner
| An Accompaniment to Higher Mathematics [[electronic resource] /] / by George R. Exner |
| Autore | Exner George R |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | New York, NY : , : Springer New York : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (XVII, 200 p.) |
| Disciplina | 511.3 |
| Collana | Undergraduate Texts in Mathematics |
| Soggetto topico |
Mathematical analysis
Analysis (Mathematics) Topology Mathematical logic Analysis Mathematical Logic and Foundations |
| ISBN | 1-4612-3998-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 1 Examples -- 1.1 Propaganda -- 1.2 Basic Examples for Definitions -- 1.3 Basic Examples for Theorems -- 1.4 Extended Examples -- 1.5 Notational Interlude -- 1.6 Examples Again: Standard Sources -- 1.7 Non-examples for Definitions -- 1.8 Non-examples for Theorems -- 1.9 Summary and More Propaganda -- 1.10 What Next? -- 2 Informal Language and Proof -- 2.1 Ordinary Language Clues -- 2.2 Real-Life Proofs vs. Rules of Thumb -- 2.3 Proof Forms for Implication -- 2.4 Two More Proof Forms -- 2.5 The Other Shoe, and Propaganda -- 3 For mal Language and Proof -- 3.1 Propaganda -- 3.2 Formal Language: Basics -- 3.3 Quantifiers -- 3.4 Finding Proofs from Structure -- 3.5 Summary, Propaganda, and What Next? -- 4 Laboratories -- 4.1 Lab I: Sets by Example -- 4.2 Lab II: Functions by Example -- 4.3 Lab III: Sets and Proof -- 4.4 Lab IV: Functions and Proof -- 4.5 Lab V: Function of Sets -- 4.6 Lab VI: Families of Sets -- A Theoretical Apologia -- B Hints -- References. |
| Record Nr. | UNINA-9910480848803321 |
|
Exner George R
|
||
| New York, NY : , : Springer New York : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
An Accompaniment to Higher Mathematics [[electronic resource] /] / by George R. Exner
| An Accompaniment to Higher Mathematics [[electronic resource] /] / by George R. Exner |
| Autore | Exner George R |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | New York, NY : , : Springer New York : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (XVII, 200 p.) |
| Disciplina | 511.3 |
| Collana | Undergraduate Texts in Mathematics |
| Soggetto topico |
Mathematical analysis
Analysis (Mathematics) Topology Mathematical logic Analysis Mathematical Logic and Foundations |
| ISBN | 1-4612-3998-2 |
| Classificazione | 00A05 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | 1 Examples -- 1.1 Propaganda -- 1.2 Basic Examples for Definitions -- 1.3 Basic Examples for Theorems -- 1.4 Extended Examples -- 1.5 Notational Interlude -- 1.6 Examples Again: Standard Sources -- 1.7 Non-examples for Definitions -- 1.8 Non-examples for Theorems -- 1.9 Summary and More Propaganda -- 1.10 What Next? -- 2 Informal Language and Proof -- 2.1 Ordinary Language Clues -- 2.2 Real-Life Proofs vs. Rules of Thumb -- 2.3 Proof Forms for Implication -- 2.4 Two More Proof Forms -- 2.5 The Other Shoe, and Propaganda -- 3 For mal Language and Proof -- 3.1 Propaganda -- 3.2 Formal Language: Basics -- 3.3 Quantifiers -- 3.4 Finding Proofs from Structure -- 3.5 Summary, Propaganda, and What Next? -- 4 Laboratories -- 4.1 Lab I: Sets by Example -- 4.2 Lab II: Functions by Example -- 4.3 Lab III: Sets and Proof -- 4.4 Lab IV: Functions and Proof -- 4.5 Lab V: Function of Sets -- 4.6 Lab VI: Families of Sets -- A Theoretical Apologia -- B Hints -- References. |
| Record Nr. | UNINA-9910664947003321 |
|
Exner George R
|
||
| New York, NY : , : Springer New York : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Advanced Topics in Relation Algebras [[electronic resource] ] : Relation Algebras, Volume 2 / / by Steven Givant
| Advanced Topics in Relation Algebras [[electronic resource] ] : Relation Algebras, Volume 2 / / by Steven Givant |
| Autore | Givant Steven |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XIX, 605 p.) |
| Disciplina | 511.324 |
| Soggetto topico |
Mathematical logic
Algebra Mathematical Logic and Foundations General Algebraic Systems |
| ISBN | 3-319-65945-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Preface -- Introduction -- 14. Canonical Extensions -- 15. Completions -- 16. Representations -- 17. Representation Theorems -- 18. Varieties of Relation Algebras -- 19. Atom Structures -- Epilogue -- References -- Index. . |
| Record Nr. | UNINA-9910254307303321 |
|
Givant Steven
|
||
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Advances in Natural Deduction [[electronic resource] ] : A Celebration of Dag Prawitz's Work / / edited by Luiz Carlos Pereira, Edward Haeusler, Valeria de Paiva
| Advances in Natural Deduction [[electronic resource] ] : A Celebration of Dag Prawitz's Work / / edited by Luiz Carlos Pereira, Edward Haeusler, Valeria de Paiva |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Dordrecht : , : Springer Netherlands : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (288 p.) |
| Disciplina | 160 |
| Collana | Trends in Logic, Studia Logica Library |
| Soggetto topico |
Logic
Mathematical logic Mathematical Logic and Formal Languages Mathematical Logic and Foundations |
| ISBN | 94-007-7548-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Chapter 1. Generalizaed elimination inferences; Schroeder-Heister, Peter -- Chapter 2. Revisiting Zucker's work on the Correspondence between Cut-Elimination and Normalisation; Urban, Christian -- Chapter 3. Proofs, Reasoning and the Metamorphosis of Logic; Joinet, Jean-Baptiste -- Chapter 4. Natural Deduction for Equality: The Missing Entity; de Quieroz, Ruy J.G.B. and de Oliveira, Anjolina G -- Chapter 5. Proof-theoretical Conception of Logic; Legris, Javier -- Chapter 6. On the Structure of Natural deduction Derivations for "Generally"; Vana, Leonardo B., Veloso, Paulo A.S. , and Veloso, Sheila R.M -- Chapter 7. Type Theories from Barendregt's Cube for Theorem Provers; Seldin, Jonathan P -- Chapter 8. What is propositional logic, a theory of, if anything?; Chateaubriand, Oswaldo -- Chapter 9. Categorical Semantics of Linear Logic for All; de Paiva, Valeria -- Chapter 10. Rough sets and proof-theory; Bellin, Gianluigi -- Chapter 11. Decomposition of Reduction; Zimmermann, Ernst -- Chapter 12. An approach to general proof theory and a conjecture of a kind of completeness of intuitionistic logic revisited; Prawitz, Dag. |
| Record Nr. | UNINA-9910300152203321 |
| Dordrecht : , : Springer Netherlands : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Advances in proof theory [[electronic resource] /] / edited by Reinhard Kahle, Thomas Strahm, Thomas Studer
| Advances in proof theory [[electronic resource] /] / edited by Reinhard Kahle, Thomas Strahm, Thomas Studer |
| Edizione | [1st ed. 2016.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Birkhäuser, , 2016 |
| Descrizione fisica | 1 online resource (430 p.) |
| Disciplina | 511.3 |
| Collana | Progress in Computer Science and Applied Logic |
| Soggetto topico |
Mathematical logic
Logic Mathematical Logic and Foundations |
| ISBN | 3-319-29198-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | W. Buchholz: A survey on ordinal notations around the Bachmann-Howard ordinal -- A. Cantini: About truth and types -- R. Dyckhoff: Intuitionistic decision procedures since Gentzen -- S. Feferman: The operational perspective -- R. Gore: Formally verified proof-theory using Isabelle/HOL -- P. Minari: Analytic equational proof systems for combinatory logic and lambda calculus -- W. Pohlers: From subsystems of classical analysis to subsystems of set theory - a personal account -- M. Rathjen: Ordinal analysis and witness extraction -- P. Schuster: Logic completeness via open induction -- H. Schwichtenberg: On the computational content of Higman's lemma -- P. Schroeder-Heister: TBA -- A. Setzer: TBA -- S. Wainer: On weak "pointwise" induction, and a miniaturized predicativity. |
| Record Nr. | UNINA-9910254060903321 |
| Cham : , : Springer International Publishing : , : Imprint : Birkhäuser, , 2016 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
