top

  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.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.
Algebraic methodology and software technology : 12th International Conference, AMAST 2008 Urbana, il, USA, July 28-31, 2008, proceedings / / Jose Meseguer, Grigore Rosu (Eds.)
Algebraic methodology and software technology : 12th International Conference, AMAST 2008 Urbana, il, USA, July 28-31, 2008, proceedings / / Jose Meseguer, Grigore Rosu (Eds.)
Edizione [1st ed. 2008.]
Pubbl/distr/stampa Berlin ; ; Heidelberg : , : Springer, , [2008]
Descrizione fisica 1 online resource (XIII, 434 p.)
Disciplina 005.1
Collana Lecture Notes in Computer Science
Soggetto topico Software engineering
ISBN 3-540-79980-X
Classificazione 004
DAT 335f
MAT 110f
SS 4800
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Marrying Words and Trees -- Simulation Using Orchestration -- Liberate Computer User from Programming -- An Algebra for Features and Feature Composition -- Petri Nets Are Dioids -- Towards an Efficient Implementation of Tree Automata Completion -- Calculating Invariants as Coreflexive Bisimulations -- Types and Deadlock Freedom in a Calculus of Services, Sessions and Pipelines -- A Declarative Debugger for Maude -- Long-Run Cost Analysis by Approximation of Linear Operators over Dioids -- Towards Validating a Platoon of Cristal Vehicles Using CSP||B -- Explaining Verification Conditions -- Towards Formal Verification of ToolBus Scripts -- A Formal Analysis of Complex Type Flaw Attacks on Security Protocols -- Abstract Interpretation Plugins for Type Systems -- Separation Logic Contracts for a Java-Like Language with Fork/Join -- An Algebraic Semantics for Contract-Based Software Components -- Implementing a Categorical Information System -- Constant Complements, Reversibility and Universal View Updates -- Coinductive Properties of Causal Maps -- Extending Timed Process Algebra with Discrete Stochastic Time -- Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving -- Evolving Specification Engineering -- Verification of Java Programs with Generics -- Domain Axioms for a Family of Near-Semirings -- Generating Specialized Rules and Programs for Demand-Driven Analysis -- Non Expansive ?-Bisimulations -- A Hybrid Approach for Safe Memory Management in C -- Service Specification and Matchmaking Using Description Logic -- System Demonstration of Spiral: Generator for High-Performance Linear Transform Libraries -- The Verification of the On-Chip COMA Cache Coherence Protocol.
Record Nr. UNINA-9910767522803321
Berlin ; ; Heidelberg : , : Springer, , [2008]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Architecture of Computing Systems - ARCS 2012 [[electronic resource] ] : 25th International Conference, Munich, Germany, February 28 - March 2, 2012. Proceedings / / edited by Andreas Herkersdorf, Kay Römer, Uwe Brinkschulte
Architecture of Computing Systems - ARCS 2012 [[electronic resource] ] : 25th International Conference, Munich, Germany, February 28 - March 2, 2012. Proceedings / / edited by Andreas Herkersdorf, Kay Römer, Uwe Brinkschulte
Edizione [1st ed. 2012.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012
Descrizione fisica 1 online resource (XIII, 252 p.)
Disciplina 004.6
Collana Theoretical Computer Science and General Issues
Soggetto topico Computer networks
Computer systems
Operating systems (Computers)
Software engineering
Application software
Information storage and retrieval systems
Computer Communication Networks
Computer System Implementation
Operating Systems
Software Engineering
Computer and Information Systems Applications
Information Storage and Retrieval
Soggetto genere / forma Kongress2012.München
Conference papers and proceedings.
ISBN 3-642-28293-8
Classificazione SS 4800
004
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Record Nr. UNISA-996466029103316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Artificial Intelligence and Cognitive Science [[electronic resource] ] : 20th Irish Conference, AICS 2009, Dublin, Ireland, August 19-21, 2009, Revised Selected Papers / / edited by Lorcan Coyle, Jill Freyne
Artificial Intelligence and Cognitive Science [[electronic resource] ] : 20th Irish Conference, AICS 2009, Dublin, Ireland, August 19-21, 2009, Revised Selected Papers / / edited by Lorcan Coyle, Jill Freyne
Edizione [1st ed. 2010.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Descrizione fisica 1 online resource (XI, 293 p. 108 illus.)
Disciplina 006.3
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Computer communication systems
Application software
Information storage and retrieval
Computers
Database management
Artificial Intelligence
Computer Communication Networks
Information Systems Applications (incl. Internet)
Information Storage and Retrieval
Computation by Abstract Devices
Database Management
Soggetto genere / forma Kongress
ISBN 1-280-39037-9
9786613568298
3-642-17080-3
Classificazione 004
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Use of Enterprise Social Software to Support Organization and People Sensemaking -- Collective Intelligence in the Social Web -- Full Papers -- Robustness Analysis of Model-Based Collaborative Filtering Systems -- Phase and Coordination in Speech Production -- The Effect of Query Length on Normalisation in Information Retrieval -- An Evolutionary Neural Network Approach to Intrinsic Plagiarism Detection -- Investigation of Localised Centrality Metrics for Collaborative Networks: What Can They Reveal? -- Practical Development of Hybrid Intelligent Agent Systems with SoSAA -- Genetic Repair Strategies Inspired by Arabidopsis thaliana -- A Machine Learning System for Identifying Hypertrophy in Histopathology Images -- Creating Visualizations: A Case-Based Reasoning Perspective -- Assessing Context for Age-Related Spanish Temporal Phrases -- Using Shallow Natural Language Processing in a Just-In-Time Information Retrieval Assistant for Bloggers -- Towards Automatic Blotch Detection for Film Restoration by Comparison of Spatio-Temporal Neighbours -- Analysis of the Effect of Unexpected Outliers in the Classification of Spectroscopy Data -- Just Say It: An Evaluation of Speech Interfaces for Augmented Reality Design Applications -- SceneMaker: Intelligent Multimodal Visualisation of Natural Language Scripts -- The Enhanced Ranked List -- A Prediction Market for Toxic Assets -- Learning without Default: A Study of One-Class Classification and the Low-Default Portfolio Problem -- A Survey of Recent Trends in One Class Classification -- Steady State RF Fingerprinting for Identity Verification: One Class Classifier versus Customized Ensemble -- An Analysis of Order Dependence in k-NN -- Norm Convergence in Populations of Dynamically Interacting Agents -- A Comparison of Word Similarity Measures for Noun Compound Disambiguation -- An Assessment of Machine Learning Techniques for Review Recommendation -- Buzzer – Online Real-Time Topical News Article and Source Recommender -- An Evaluation of the GhostWriter System for Case-Based Content Suggestions -- On Using Temporal Features to Create More Accurate Human-Activity Classifiers -- Demo Papers -- Physical Activity Motivating Games -- A Machine Learning System for Tracking Sentiment in Irish Economic News -- The Blogoduct System: A Just-In-Time Information Retrieval Assistant for Bloggers -- Sensing Handshakes for Social Network Development -- A Decision Support System for Energy Storage Traders.
Record Nr. UNISA-996465966703316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Artificial Intelligence and Cognitive Science [[electronic resource] ] : 20th Irish Conference, AICS 2009, Dublin, Ireland, August 19-21, 2009, Revised Selected Papers / / edited by Lorcan Coyle, Jill Freyne
Artificial Intelligence and Cognitive Science [[electronic resource] ] : 20th Irish Conference, AICS 2009, Dublin, Ireland, August 19-21, 2009, Revised Selected Papers / / edited by Lorcan Coyle, Jill Freyne
Edizione [1st ed. 2010.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Descrizione fisica 1 online resource (XI, 293 p. 108 illus.)
Disciplina 006.3
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Computer communication systems
Application software
Information storage and retrieval
Computers
Database management
Artificial Intelligence
Computer Communication Networks
Information Systems Applications (incl. Internet)
Information Storage and Retrieval
Computation by Abstract Devices
Database Management
Soggetto genere / forma Kongress
ISBN 1-280-39037-9
9786613568298
3-642-17080-3
Classificazione 004
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Invited Talks -- Use of Enterprise Social Software to Support Organization and People Sensemaking -- Collective Intelligence in the Social Web -- Full Papers -- Robustness Analysis of Model-Based Collaborative Filtering Systems -- Phase and Coordination in Speech Production -- The Effect of Query Length on Normalisation in Information Retrieval -- An Evolutionary Neural Network Approach to Intrinsic Plagiarism Detection -- Investigation of Localised Centrality Metrics for Collaborative Networks: What Can They Reveal? -- Practical Development of Hybrid Intelligent Agent Systems with SoSAA -- Genetic Repair Strategies Inspired by Arabidopsis thaliana -- A Machine Learning System for Identifying Hypertrophy in Histopathology Images -- Creating Visualizations: A Case-Based Reasoning Perspective -- Assessing Context for Age-Related Spanish Temporal Phrases -- Using Shallow Natural Language Processing in a Just-In-Time Information Retrieval Assistant for Bloggers -- Towards Automatic Blotch Detection for Film Restoration by Comparison of Spatio-Temporal Neighbours -- Analysis of the Effect of Unexpected Outliers in the Classification of Spectroscopy Data -- Just Say It: An Evaluation of Speech Interfaces for Augmented Reality Design Applications -- SceneMaker: Intelligent Multimodal Visualisation of Natural Language Scripts -- The Enhanced Ranked List -- A Prediction Market for Toxic Assets -- Learning without Default: A Study of One-Class Classification and the Low-Default Portfolio Problem -- A Survey of Recent Trends in One Class Classification -- Steady State RF Fingerprinting for Identity Verification: One Class Classifier versus Customized Ensemble -- An Analysis of Order Dependence in k-NN -- Norm Convergence in Populations of Dynamically Interacting Agents -- A Comparison of Word Similarity Measures for Noun Compound Disambiguation -- An Assessment of Machine Learning Techniques for Review Recommendation -- Buzzer – Online Real-Time Topical News Article and Source Recommender -- An Evaluation of the GhostWriter System for Case-Based Content Suggestions -- On Using Temporal Features to Create More Accurate Human-Activity Classifiers -- Demo Papers -- Physical Activity Motivating Games -- A Machine Learning System for Tracking Sentiment in Irish Economic News -- The Blogoduct System: A Just-In-Time Information Retrieval Assistant for Bloggers -- Sensing Handshakes for Social Network Development -- A Decision Support System for Energy Storage Traders.
Record Nr. UNINA-9910484063203321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2010
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Artificial Intelligence in Medicine [[electronic resource] ] : 14th Conference on Artificial Intelligence in Medicine, AIME 2013, Murcia, Spain, May 29 -- June 1, 2013, Proceedings / / edited by Niels Peek, Roque Luis Marín Morales, Mor Peleg
Artificial Intelligence in Medicine [[electronic resource] ] : 14th Conference on Artificial Intelligence in Medicine, AIME 2013, Murcia, Spain, May 29 -- June 1, 2013, Proceedings / / edited by Niels Peek, Roque Luis Marín Morales, Mor Peleg
Edizione [1st ed. 2013.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Descrizione fisica 1 online resource (XX, 316 p. 74 illus.)
Disciplina 610.285
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Health informatics
Data mining
Pattern recognition
Application software
Artificial Intelligence
Health Informatics
Data Mining and Knowledge Discovery
Pattern Recognition
Information Systems Applications (incl. Internet)
Soggetto genere / forma Kongress2013.Murcia
Conference papers and proceedings.
ISBN 3-642-38326-2
Classificazione 004
DAT 700f
DAT 703f
MED 230f
SS 4800
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Decision support, guidelines and protocols -- Semantic technology -- Bioinformatics -- Machine learning -- Probabilistic modeling and reasoning -- Image and signal processing -- Temporal data visualization and analysis -- Natural language processing.
Record Nr. UNISA-996466570203316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Artificial Intelligence in Medicine [[electronic resource] ] : 14th Conference on Artificial Intelligence in Medicine, AIME 2013, Murcia, Spain, May 29 -- June 1, 2013, Proceedings / / edited by Niels Peek, Roque Luis Marín Morales, Mor Peleg
Artificial Intelligence in Medicine [[electronic resource] ] : 14th Conference on Artificial Intelligence in Medicine, AIME 2013, Murcia, Spain, May 29 -- June 1, 2013, Proceedings / / edited by Niels Peek, Roque Luis Marín Morales, Mor Peleg
Edizione [1st ed. 2013.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Descrizione fisica 1 online resource (XX, 316 p. 74 illus.)
Disciplina 610.285
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Health informatics
Data mining
Pattern recognition
Application software
Artificial Intelligence
Health Informatics
Data Mining and Knowledge Discovery
Pattern Recognition
Information Systems Applications (incl. Internet)
Soggetto genere / forma Kongress2013.Murcia
Conference papers and proceedings.
ISBN 3-642-38326-2
Classificazione 004
DAT 700f
DAT 703f
MED 230f
SS 4800
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Decision support, guidelines and protocols -- Semantic technology -- Bioinformatics -- Machine learning -- Probabilistic modeling and reasoning -- Image and signal processing -- Temporal data visualization and analysis -- Natural language processing.
Record Nr. UNINA-9910484128203321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 : proceedings / / Renate A. Schmidt
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 : proceedings / / Renate A. Schmidt
Edizione [1st ed. 2009.]
Pubbl/distr/stampa Berlin, Germany ; ; New York, New York : , : Springer, , [2009]
Descrizione fisica 1 online resource (515 p.)
Disciplina 006.3
Collana Lecture notes in computer science
Lecture notes in artificial intelligence
LNCS sublibrary. SL 7, Artificial intelligence
Soggetto topico Logic, Symbolic and mathematical
Automatic theorem proving
ISBN 1-282-33197-3
9786612331978
3-642-02959-0
Classificazione DAT 706f
DAT 716f
SS 4800
004
510
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Session 1. Invited Talk -- Integrated Reasoning and Proof Choice Point Selection in the Jahob System – Mechanisms for Program Survival -- Session 2. Combinations and Extensions -- Superposition and Model Evolution Combined -- On Deciding Satisfiability by DPLL( ) and Unsound Theorem Proving -- Combinable Extensions of Abelian Groups -- Locality Results for Certain Extensions of Theories with Bridging Functions -- Session 3. Minimal Unsatisfiability and Automated Reasoning Support -- Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis -- Does This Set of Clauses Overlap with at Least One MUS? -- Progress in the Development of Automated Theorem Proving for Higher-Order Logic -- Session 4. System Descriptions -- System Description: H-PILoT -- SPASS Version 3.5 -- Dei: A Theorem Prover for Terms with Integer Exponents -- veriT: An Open, Trustable and Efficient SMT-Solver -- Divvy: An ATP Meta-system Based on Axiom Relevance Ordering -- Session 5. Invited Talk -- Instantiation-Based Automated Reasoning: From Theory to Practice -- Session 6. Interpolation and Predicate Abstraction -- Interpolant Generation for UTVPI -- Ground Interpolation for Combined Theories -- Interpolation and Symbol Elimination -- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction -- Session 7. Resolution-Based Systems for Non-classical Logics -- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method -- A Refined Resolution Calculus for CTL -- Fair Derivations in Monodic Temporal Reasoning -- Session 8. Termination Analysis and Constraint Solving -- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs -- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic -- Session 9. Invited Talk -- Building Theorem Provers -- Session 10. Rewriting, Termination and Productivity -- Termination Analysis by Dependency Pairs and Inductive Theorem Proving -- Beyond Dependency Graphs -- Computing Knowledge in Security Protocols under Convergent Equational Theories -- Complexity of Fractran and Productivity -- Session 11. Models -- Automated Inference of Finite Unsatisfiability -- Decidability Results for Saturation-Based Model Building -- Session 12. Modal Tableaux with Global Caching -- A Tableau Calculus for Regular Grammar Logics with Converse -- An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability -- Session 13. Arithmetic -- Volume Computation for Boolean Combination of Linear Arithmetic Constraints -- A Generalization of Semenov’s Theorem to Automata over Real Numbers -- Real World Verification.
Altri titoli varianti CADE 22
Record Nr. UNINA-9910483050003321
Berlin, Germany ; ; New York, New York : , : Springer, , [2009]
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 : proceedings / / Renate A. Schmidt
Automated deduction - CADE-22 : 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009 : proceedings / / Renate A. Schmidt
Edizione [1st ed. 2009.]
Pubbl/distr/stampa Berlin, Germany ; ; New York, New York : , : Springer, , [2009]
Descrizione fisica 1 online resource (515 p.)
Disciplina 006.3
Collana Lecture notes in computer science
Lecture notes in artificial intelligence
LNCS sublibrary. SL 7, Artificial intelligence
Soggetto topico Logic, Symbolic and mathematical
Automatic theorem proving
ISBN 1-282-33197-3
9786612331978
3-642-02959-0
Classificazione DAT 706f
DAT 716f
SS 4800
004
510
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto Session 1. Invited Talk -- Integrated Reasoning and Proof Choice Point Selection in the Jahob System – Mechanisms for Program Survival -- Session 2. Combinations and Extensions -- Superposition and Model Evolution Combined -- On Deciding Satisfiability by DPLL( ) and Unsound Theorem Proving -- Combinable Extensions of Abelian Groups -- Locality Results for Certain Extensions of Theories with Bridging Functions -- Session 3. Minimal Unsatisfiability and Automated Reasoning Support -- Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis -- Does This Set of Clauses Overlap with at Least One MUS? -- Progress in the Development of Automated Theorem Proving for Higher-Order Logic -- Session 4. System Descriptions -- System Description: H-PILoT -- SPASS Version 3.5 -- Dei: A Theorem Prover for Terms with Integer Exponents -- veriT: An Open, Trustable and Efficient SMT-Solver -- Divvy: An ATP Meta-system Based on Axiom Relevance Ordering -- Session 5. Invited Talk -- Instantiation-Based Automated Reasoning: From Theory to Practice -- Session 6. Interpolation and Predicate Abstraction -- Interpolant Generation for UTVPI -- Ground Interpolation for Combined Theories -- Interpolation and Symbol Elimination -- Complexity and Algorithms for Monomial and Clausal Predicate Abstraction -- Session 7. Resolution-Based Systems for Non-classical Logics -- Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method -- A Refined Resolution Calculus for CTL -- Fair Derivations in Monodic Temporal Reasoning -- Session 8. Termination Analysis and Constraint Solving -- A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs -- Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic -- Session 9. Invited Talk -- Building Theorem Provers -- Session 10. Rewriting, Termination and Productivity -- Termination Analysis by Dependency Pairs and Inductive Theorem Proving -- Beyond Dependency Graphs -- Computing Knowledge in Security Protocols under Convergent Equational Theories -- Complexity of Fractran and Productivity -- Session 11. Models -- Automated Inference of Finite Unsatisfiability -- Decidability Results for Saturation-Based Model Building -- Session 12. Modal Tableaux with Global Caching -- A Tableau Calculus for Regular Grammar Logics with Converse -- An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability -- Session 13. Arithmetic -- Volume Computation for Boolean Combination of Linear Arithmetic Constraints -- A Generalization of Semenov’s Theorem to Automata over Real Numbers -- Real World Verification.
Altri titoli varianti CADE 22
Record Nr. UNISA-996465837603316
Berlin, Germany ; ; New York, New York : , : Springer, , [2009]
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated Deduction -- CADE-24 [[electronic resource] ] : 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings / / edited by Maria Paola Bonacina
Automated Deduction -- CADE-24 [[electronic resource] ] : 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings / / edited by Maria Paola Bonacina
Edizione [1st ed. 2013.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Descrizione fisica 1 online resource (XVI, 466 p. 95 illus.) : digital
Disciplina 511.3
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Mathematical logic
Computer logic
Software engineering
Algorithms
Artificial Intelligence
Mathematical Logic and Formal Languages
Logics and Meanings of Programs
Software Engineering
Algorithm Analysis and Problem Complexity
Soggetto genere / forma Kongress2013.Lake Placid, NY
Conference papers and proceedings.
ISBN 3-642-38574-5
Classificazione 004
510
DAT 706f
DAT 716f
SS 4800
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto One Logic to Use Them All -- The Tree Width of Separation Logic with Recursive Definitions -- Hierarchic Superposition with Weak Abstraction -- Completeness and Decidability Results for First-Order Clauses with Indices -- A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies -- Tractable Inference Systems: An Extension with a Deducibility Predicate -- Computing Tiny Clause Normal Forms -- System Description: E-KRHyper 1.4 Extensions for Unique Names and Description Logic -- Analysing Vote Counting Algorithms via Logic: And Its Application to the CADE Election Scheme -- Automated Reasoning, Fast and Slow -- Foundational Proof Certificates in First-Order Logic -- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals -- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition -- dReal: An SMT Solver for Nonlinear Theories over the Reals -- Solving Difference Constraints over Modular Arithmetic -- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis -- Hierarchical Combination -- PRocH: Proof Reconstruction for HOL Light -- An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description -- Towards Modularly Comparing Programs Using Automated Theorem Provers -- Reuse in Software Verification by Abstract Method Calls -- Dynamic Logic with Trace Semantics -- Temporalizing Ontology-Based Data Access -- Verifying Refutations with Extended Resolution -- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems -- Quantifier Instantiation Techniques for Finite Model Finding in SMT -- Automating Inductive Proofs Using Theory Exploration -- E-MaLeS 1.1 -- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism -- Propositional Temporal Proving with Reductions to a SAT Problem -- InKreSAT: Modal Reasoning via Incremental Reduction to SAT -- bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR -- The 481 Ways to Split a Clause and Deal with Propositional Variables.
Record Nr. UNISA-996465852703316
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Materiale a stampa
Lo trovi qui: Univ. di Salerno
Opac: Controlla la disponibilità qui
Automated Deduction -- CADE-24 [[electronic resource] ] : 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings / / edited by Maria Paola Bonacina
Automated Deduction -- CADE-24 [[electronic resource] ] : 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013, Proceedings / / edited by Maria Paola Bonacina
Edizione [1st ed. 2013.]
Pubbl/distr/stampa Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Descrizione fisica 1 online resource (XVI, 466 p. 95 illus.) : digital
Disciplina 511.3
Collana Lecture Notes in Artificial Intelligence
Soggetto topico Artificial intelligence
Mathematical logic
Computer logic
Software engineering
Algorithms
Artificial Intelligence
Mathematical Logic and Formal Languages
Logics and Meanings of Programs
Software Engineering
Algorithm Analysis and Problem Complexity
Soggetto genere / forma Kongress2013.Lake Placid, NY
Conference papers and proceedings.
ISBN 3-642-38574-5
Classificazione 004
510
DAT 706f
DAT 716f
SS 4800
Formato Materiale a stampa
Livello bibliografico Monografia
Lingua di pubblicazione eng
Nota di contenuto One Logic to Use Them All -- The Tree Width of Separation Logic with Recursive Definitions -- Hierarchic Superposition with Weak Abstraction -- Completeness and Decidability Results for First-Order Clauses with Indices -- A Proof Procedure for Hybrid Logic with Binders, Transitivity and Relation Hierarchies -- Tractable Inference Systems: An Extension with a Deducibility Predicate -- Computing Tiny Clause Normal Forms -- System Description: E-KRHyper 1.4 Extensions for Unique Names and Description Logic -- Analysing Vote Counting Algorithms via Logic: And Its Application to the CADE Election Scheme -- Automated Reasoning, Fast and Slow -- Foundational Proof Certificates in First-Order Logic -- Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals -- A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition -- dReal: An SMT Solver for Nonlinear Theories over the Reals -- Solving Difference Constraints over Modular Arithmetic -- Asymmetric Unification: A New Unification Paradigm for Cryptographic Protocol Analysis -- Hierarchical Combination -- PRocH: Proof Reconstruction for HOL Light -- An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description -- Towards Modularly Comparing Programs Using Automated Theorem Provers -- Reuse in Software Verification by Abstract Method Calls -- Dynamic Logic with Trace Semantics -- Temporalizing Ontology-Based Data Access -- Verifying Refutations with Extended Resolution -- Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems -- Quantifier Instantiation Techniques for Finite Model Finding in SMT -- Automating Inductive Proofs Using Theory Exploration -- E-MaLeS 1.1 -- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism -- Propositional Temporal Proving with Reductions to a SAT Problem -- InKreSAT: Modal Reasoning via Incremental Reduction to SAT -- bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR -- The 481 Ways to Split a Clause and Deal with Propositional Variables.
Record Nr. UNINA-9910483964403321
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013
Materiale a stampa
Lo trovi qui: Univ. Federico II
Opac: Controlla la disponibilità qui