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.
Computer science--theory and applications : First International Computer Science Symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8-12, 2006 : proceedings / / Dima Grigoriev, John Harrison, Edward A. Hirsch (eds.)
| Computer science--theory and applications : First International Computer Science Symposium in Russia, CSR 2006, St. Petersburg, Russia, June 8-12, 2006 : proceedings / / Dima Grigoriev, John Harrison, Edward A. Hirsch (eds.) |
| Edizione | [1st ed. 2006.] |
| Pubbl/distr/stampa | Berlin, : Springer-Verlag, c2006 |
| Descrizione fisica | 1 online resource (XVI, 684 p.) |
| Disciplina | 004 |
| Altri autori (Persone) |
GrigorievDima
HarrisonJ <1966-> (John) HirschEdward A |
| Collana |
Lecture notes in computer science
LNCS sublibrary. SL 1, Theoretical computer science and general issues |
| Soggetto topico | Computer science |
| ISBN | 3-540-34168-4 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Papers -- Non-black-box Techniques in Cryptography -- Complexity of Polynomial Multiplication over Finite Fields -- Synchronous Elastic Circuits -- Theory Track -- SZK Proofs for Black-Box Group Problems -- Canonical Decomposition of a Regular Factorial Language -- Acyclic Bidirected and Skew-Symmetric Graphs: Algorithms and Structure -- Inductive Type Schemas as Functors -- Unfolding Synthesis of Asynchronous Automata -- Conjugacy and Equivalence of Weighted Automata and Functional Transducers -- Applications of the Linear Matroid Parity Algorithm to Approximating Steiner Trees -- Tuples of Disjoint NP-Sets -- Constructive Equivalence Relations on Computable Probability Measures -- Planar Dimer Tilings -- The Complexity of Equality Constraint Languages -- Window Subsequence Problems for Compressed Texts -- Efficient Algorithms in Zero-Characteristic for a New Model of Representation of Algebraic Varieties -- Relativisation Provides Natural Separations for Resolution-Based Proof Systems -- Bounded-Degree Forbidden Patterns Problems Are Constraint Satisfaction Problems -- Isolation and Reducibility Properties and the Collapse Result -- Incremental Branching Programs -- Logic of Proofs for Bounded Arithmetic -- On a Maximal NFA Without Mergible States -- Expressiveness of Metric Modalities for Continuous Time -- Extending Dijkstra’s Algorithm to Maximize the Shortest Path by Node-Wise Limited Arc Interdiction -- Weighted Logics for Traces -- On Nonforgetting Restarting Automata That Are Deterministic and/or Monotone -- Unwinding a Non-effective Cut Elimination Proof -- Enumerate and Expand: Improved Algorithms for Connected Vertex Cover and Tree Cover -- Shannon Entropy vs. Kolmogorov Complexity -- Language Equations with Symmetric Difference -- On Primitive Recursive Realizabilities -- Evidence Reconstruction of Epistemic Modal Logic S5 -- Linear Temporal Logic with Until and Before on Integer Numbers, Deciding Algorithms -- On the Frequency of Letters in Morphic Sequences -- Functional Equations in Shostak Theories -- All Semi-local Longest Common Subsequences in Subquadratic Time -- Non-approximability of the Randomness Deficiency Function -- Multi-agent Explicit Knowledge -- Applications and Technology Track -- Polarized Subtyping for Sized Types -- Neural-Network Based Physical Fields Modeling Techniques -- Approximate Methods for Constrained Total Variation Minimization -- Dynamic Isoline Extraction for Visualization of Streaming Data -- Improved Technique of IP Address Fragmentation Strategies for DoS Attack Traceback -- Performance Comparison Between Backpropagation, Neuro-Fuzzy Network, and SVM -- Evolutionary Multi-objective Optimisation by Diversity Control -- 3D Facial Recognition Using Eigenface and Cascade Fuzzy Neural Networks: Normalized Facial Image Approach -- A New Scaling Kernel-Based Fuzzy System with Low Computational Complexity -- Bulk Synchronous Parallel ML: Semantics and Implementation of the Parallel Juxtaposition -- A Shortest Path Algorithm Based on Limited Search Heuristics -- A New Hybrid Directory Scheme for Shared Memory Multi-processors -- Manipulator Path Planning in 3-Dimensional Space -- Least Likely to Use: A New Page Replacement Strategy for Improving Database Management System Response Time -- Nonlinear Visualization of Incomplete Data Sets -- A Review of Race Detection Mechanisms -- Fuzzy-Q Knowledge Sharing Techniques with Expertness Measures: Comparison and Analysis -- Explaining Symbolic Trajectory Evaluation by Giving It a Faithful Semantics -- Analytic Modeling of Channel Traffic in n-Cubes -- Capturing an Intruder in the Pyramid -- Speech Enhancement in Short-Wave Channel Based on Empirical Mode Decomposition -- Extended Resolution Proofs for Conjoining BDDs -- Optimal Difference Systems of Sets with Multipliers -- Authentication Mechanism Using One-Time Password for 802.11 Wireless LAN -- Optimizing Personalized Retrieval System Based on Web Ranking -- Instruction Selection for ARM/Thumb Processors Based on a Multi-objective Ant Algorithm -- A New Flow Control Algorithm for High Speed Computer Network -- Nonlinear Systems Modeling and Control Using Support Vector Machine Technique -- Fast Motif Search in Protein Sequence Databases. |
| Altri titoli varianti | CSR 2006 |
| Record Nr. | UNINA-9910483392603321 |
| Berlin, : Springer-Verlag, c2006 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Theorem proving in higher order logics : 13th International Conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000 : proceedings / / Mark Aagaard, John Harrison (editors)
| Theorem proving in higher order logics : 13th International Conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000 : proceedings / / Mark Aagaard, John Harrison (editors) |
| Edizione | [1st ed. 2000.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg ; ; New York : , : Springer, , [2000] |
| Descrizione fisica | 1 online resource (545 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN |
1-280-95654-2
9786610956548 3-540-44659-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Fix-Point Equations for Well-Founded Recursion in Type Theory -- Programming and Computing in HOL -- Proof Terms for Simply Typed Higher Order Logic -- Routing Information Protocol in HOL/SPIN -- Recursive Families of Inductive Types -- Aircraft Trajectory Modeling and Alerting Algorithm Verification -- Intel’s Formal Verification Experience on the Willamette Development -- A Prototype Proof Translator from HOL to Coq -- Proving ML Type Soundness Within Coq -- On the Mechanization of Real Analysis in Isabelle/HOL -- Equational Reasoning via Partial Reflection -- Reachability Programming in HOL98 Using BDDs -- Transcendental Functions and Continuity Checking in PVS -- Verified Optimizations for the Intel IA-64 Architecture -- Formal Verification of IA-64 Division Algorithms -- Fast Tactic-Based Theorem Proving -- Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover -- A Strong and Mechanizable Grand Logic -- Inheritance in Higher Order Logic: Modeling and Reasoning -- Total-Correctness Refinement for Sequential Reactive Systems -- Divider Circuit Verification with Model Checking and Theorem Proving -- Specification and Verification of a Steam-Boiler with Signal-Coq -- Functional Procedures in Higher-Order Logic -- Formalizing Stålmarck’s Algorithm in Coq -- TAS — A Generic Window Inference System -- Weak Alternating Automata in Isabelle/HOL -- Graphical Theories of Interactive Systems: Can a Proof Assistant Help? -- Formal Verification of the Alpha 21364 Network Protocol -- Dependently Typed Records for Representing Mathematical Structure -- Towards a Machine-Checked Java Specification Book -- Another Look at Nested Recursion -- Automating the Search for Answers to Open Questions -- Appendix: Conjectures Concerning Proof, Design, and Verification. |
| Record Nr. | UNISA-996465948503316 |
| Berlin ; ; Heidelberg ; ; New York : , : Springer, , [2000] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Theorem proving in higher order logics : 13th International Conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000 : proceedings / / Mark Aagaard, John Harrison (editors)
| Theorem proving in higher order logics : 13th International Conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000 : proceedings / / Mark Aagaard, John Harrison (editors) |
| Edizione | [1st ed. 2000.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg ; ; New York : , : Springer, , [2000] |
| Descrizione fisica | 1 online resource (545 p.) |
| Disciplina | 004.015113 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico | Automatic theorem proving |
| ISBN |
1-280-95654-2
9786610956548 3-540-44659-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Fix-Point Equations for Well-Founded Recursion in Type Theory -- Programming and Computing in HOL -- Proof Terms for Simply Typed Higher Order Logic -- Routing Information Protocol in HOL/SPIN -- Recursive Families of Inductive Types -- Aircraft Trajectory Modeling and Alerting Algorithm Verification -- Intel’s Formal Verification Experience on the Willamette Development -- A Prototype Proof Translator from HOL to Coq -- Proving ML Type Soundness Within Coq -- On the Mechanization of Real Analysis in Isabelle/HOL -- Equational Reasoning via Partial Reflection -- Reachability Programming in HOL98 Using BDDs -- Transcendental Functions and Continuity Checking in PVS -- Verified Optimizations for the Intel IA-64 Architecture -- Formal Verification of IA-64 Division Algorithms -- Fast Tactic-Based Theorem Proving -- Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover -- A Strong and Mechanizable Grand Logic -- Inheritance in Higher Order Logic: Modeling and Reasoning -- Total-Correctness Refinement for Sequential Reactive Systems -- Divider Circuit Verification with Model Checking and Theorem Proving -- Specification and Verification of a Steam-Boiler with Signal-Coq -- Functional Procedures in Higher-Order Logic -- Formalizing Stålmarck’s Algorithm in Coq -- TAS — A Generic Window Inference System -- Weak Alternating Automata in Isabelle/HOL -- Graphical Theories of Interactive Systems: Can a Proof Assistant Help? -- Formal Verification of the Alpha 21364 Network Protocol -- Dependently Typed Records for Representing Mathematical Structure -- Towards a Machine-Checked Java Specification Book -- Another Look at Nested Recursion -- Automating the Search for Answers to Open Questions -- Appendix: Conjectures Concerning Proof, Design, and Verification. |
| Record Nr. | UNINA-9910767567003321 |
| Berlin ; ; Heidelberg ; ; New York : , : Springer, , [2000] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||