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.
Automated Deduction - CADE-17 [[electronic resource] ] : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester
| Automated Deduction - CADE-17 [[electronic resource] ] : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester |
| Edizione | [1st ed. 2000.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
| Descrizione fisica | 1 online resource (XIV, 526 p.) |
| Disciplina | 006.333 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Computers Mathematical logic Computer logic Artificial Intelligence Theory of Computation Mathematical Logic and Formal Languages Logics and Meanings of Programs Mathematical Logic and Foundations |
| ISBN | 3-540-45101-3 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk: -- High-Level Verification Using Theorem Proving and Formalized Mathematics -- Session 1: -- Machine Instruction Syntax and Semantics in Higher Order Logic -- Proof Generation in the Touchstone Theorem Prover -- Wellfounded Schematic Definitions -- Session 2: -- Abstract Congruence Closure and Specializations -- A Framework for Cooperating Decision Procedures -- Modular Reasoning in Isabelle -- An Infrastructure for Intertheory Reasoning -- Session 3: -- Gödel’s Algorithm for Class Formation -- Automated Proof Construction in Type Theory Using Resolution -- System Description: TPS: A Theorem Proving System for Type Theory -- The Nuprl Open Logical Environment -- System Description: aRa – An Automatic Theorem Prover for Relation Algebras -- Invited Talk: -- Scalable Knowledge Representation and Reasoning Systems -- Session 4: -- Efficient Minimal Model Generation Using Branching Lemmas -- FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure -- Rigid E-Unification Revisited -- Invited Talk: -- Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice -- Session 5: -- Reducing Model Checking of the Many to the Few -- Simulation Based Minimization -- Rewriting for Cryptographic Protocol Verification -- System Description: *sat: A Platform for the Development of Modal Decision Procedures -- System Description: DLP -- Two Techniques to Improve Finite Model Search -- Session 6: -- Eliminating Dummy Elimination -- Extending Decision Procedures with Induction Schemes -- Complete Monotonic Semantic Path Orderings -- Session 7: -- Stratified Resolution -- Support Ordered Resolution -- System Description: IVY -- System Description: SystemOnTPTP -- System Description: PTTP+GLiDeS Semantically Guided PTTP -- Session 8: -- A Formalization of a Concurrent Object Calculus up to ?-Conversion -- A Resolution Decision Procedure for Fluted Logic -- ZRes: The Old Davis–Putnam Procedure Meets ZBDD -- System Description: MBase, an Open Mathematical Knowledge Base -- System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level -- Session 9: -- On Unification for Bounded Distributive Lattices -- Reasoning with Individuals for the Description Logic -- System Description: Embedding Verification into Microsoft Excel -- System Description: Interactive Proof Critics in XBarnacle -- Tutorials: -- Tutorial: Meta-logical Frameworks -- Tutorial: Automated Deduction and Natural Language Understanding -- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic -- Workshops: -- Workshop: Model Computation – Principles, Algorithms, Applications -- Workshop: Automation of Proof by Mathematical Induction -- Workshop: Type-Theoretic Languages: Proof-Search and Semantics -- Workshop: Automated Deduction in Education -- Workshop: The Role of Automated Deduction in Mathematics. |
| Record Nr. | UNISA-996466137803316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Deduction - CADE-17 : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester
| Automated Deduction - CADE-17 : 17th International Conference on Automated Deduction Pittsburgh, PA, USA, June 17-20, 2000 Proceedings / / edited by David McAllester |
| Edizione | [1st ed. 2000.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 |
| Descrizione fisica | 1 online resource (XIV, 526 p.) |
| Disciplina | 006.333 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Computers Logic, Symbolic and mathematical Computer logic Artificial Intelligence Theory of Computation Mathematical Logic and Formal Languages Logics and Meanings of Programs Mathematical Logic and Foundations |
| ISBN | 3-540-45101-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talk: -- High-Level Verification Using Theorem Proving and Formalized Mathematics -- Session 1: -- Machine Instruction Syntax and Semantics in Higher Order Logic -- Proof Generation in the Touchstone Theorem Prover -- Wellfounded Schematic Definitions -- Session 2: -- Abstract Congruence Closure and Specializations -- A Framework for Cooperating Decision Procedures -- Modular Reasoning in Isabelle -- An Infrastructure for Intertheory Reasoning -- Session 3: -- Gödel’s Algorithm for Class Formation -- Automated Proof Construction in Type Theory Using Resolution -- System Description: TPS: A Theorem Proving System for Type Theory -- The Nuprl Open Logical Environment -- System Description: aRa – An Automatic Theorem Prover for Relation Algebras -- Invited Talk: -- Scalable Knowledge Representation and Reasoning Systems -- Session 4: -- Efficient Minimal Model Generation Using Branching Lemmas -- FDPLL — A First-Order Davis-Putnam-Logeman-Loveland Procedure -- Rigid E-Unification Revisited -- Invited Talk: -- Connecting Bits with Floating-Point Numbers: Model Checking and Theorem Proving in Practice -- Session 5: -- Reducing Model Checking of the Many to the Few -- Simulation Based Minimization -- Rewriting for Cryptographic Protocol Verification -- System Description: *sat: A Platform for the Development of Modal Decision Procedures -- System Description: DLP -- Two Techniques to Improve Finite Model Search -- Session 6: -- Eliminating Dummy Elimination -- Extending Decision Procedures with Induction Schemes -- Complete Monotonic Semantic Path Orderings -- Session 7: -- Stratified Resolution -- Support Ordered Resolution -- System Description: IVY -- System Description: SystemOnTPTP -- System Description: PTTP+GLiDeS Semantically Guided PTTP -- Session 8: -- A Formalization of a Concurrent Object Calculus up to ?-Conversion -- A Resolution Decision Procedure for Fluted Logic -- ZRes: The Old Davis–Putnam Procedure Meets ZBDD -- System Description: MBase, an Open Mathematical Knowledge Base -- System Description: Tramp: Transformation of Machine-Found Proofs into Natural Deduction Proofs at the Assertion Level -- Session 9: -- On Unification for Bounded Distributive Lattices -- Reasoning with Individuals for the Description Logic -- System Description: Embedding Verification into Microsoft Excel -- System Description: Interactive Proof Critics in XBarnacle -- Tutorials: -- Tutorial: Meta-logical Frameworks -- Tutorial: Automated Deduction and Natural Language Understanding -- Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic -- Workshops: -- Workshop: Model Computation – Principles, Algorithms, Applications -- Workshop: Automation of Proof by Mathematical Induction -- Workshop: Type-Theoretic Languages: Proof-Search and Semantics -- Workshop: Automated Deduction in Education -- Workshop: The Role of Automated Deduction in Mathematics. |
| Record Nr. | UNINA-9910144146703321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2000 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings / / editors, Jasmin Blanchette, Laura Kovács, Dirk Pattinson
| Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings / / editors, Jasmin Blanchette, Laura Kovács, Dirk Pattinson |
| Autore | Blanchette Jasmin |
| Pubbl/distr/stampa | Cham, : Springer Nature, 2022 |
| Descrizione fisica | 1 online resource (xv, 756 pages) : illustrations (some color) |
| Disciplina | 006.333 |
| Altri autori (Persone) |
BlanchetteJasmin
KovácsLaura PattinsonDirk <1970-> |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Automatic theorem proving
Computer logic |
| Soggetto non controllato |
artificial intelligence
automata theory computer hardware computer networks computer programming computer systems embedded systems formal languages formal logic logic programming network protocols semantics software architecture software design software engineering theoretical computer science |
| ISBN | 3-031-10769-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996483156703316 |
Blanchette Jasmin
|
||
| Cham, : Springer Nature, 2022 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings / / editors, Jasmin Blanchette, Laura Kovács, Dirk Pattinson
| Automated reasoning : 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings / / editors, Jasmin Blanchette, Laura Kovács, Dirk Pattinson |
| Autore | Blanchette Jasmin |
| Pubbl/distr/stampa | Cham, : Springer Nature, 2022 |
| Descrizione fisica | 1 online resource (xv, 756 pages) : illustrations (some color) |
| Disciplina | 006.333 |
| Altri autori (Persone) |
BlanchetteJasmin
KovácsLaura PattinsonDirk <1970-> |
| Collana | Lecture notes in computer science |
| Soggetto topico |
Automatic theorem proving
Computer logic Demostració automàtica de teoremes Lògica informàtica |
| Soggetto genere / forma |
Congressos
Llibres electrònics |
| ISBN | 3-031-10769-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910585785003321 |
|
Blanchette Jasmin
|
||
| Cham, : Springer Nature, 2022 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated technology for verification and analysis : 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013 : proceedings / / Dang Van Hung, Oleg Sokolsky
| Automated technology for verification and analysis : 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013 : proceedings / / Dang Van Hung, Oleg Sokolsky |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2020] |
| Descrizione fisica | 1 online resource (XIV, 574 p. 796 illus., 99 illus. in color.) |
| Disciplina | 006.333 |
| Collana | Programming and Software Engineering |
| Soggetto topico | Artificial intelligence |
| ISBN | 3-030-59152-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Neural Networks and Machine Learning -- Automata -- Logics -- Techniques for Verification, Analysis and Testing -- Model Checking and Decision Procedures -- Synthesis -- Randomization and Probabilistic Systems. |
| Record Nr. | UNINA-9910427707203321 |
| Cham, Switzerland : , : Springer, , [2020] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated technology for verification and analysis : 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013 : proceedings / / Dang Van Hung, Oleg Sokolsky
| Automated technology for verification and analysis : 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18, 2013 : proceedings / / Dang Van Hung, Oleg Sokolsky |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2020] |
| Descrizione fisica | 1 online resource (XIV, 574 p. 796 illus., 99 illus. in color.) |
| Disciplina | 006.333 |
| Collana | Programming and Software Engineering |
| Soggetto topico | Artificial intelligence |
| ISBN | 3-030-59152-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Neural Networks and Machine Learning -- Automata -- Logics -- Techniques for Verification, Analysis and Testing -- Model Checking and Decision Procedures -- Synthesis -- Randomization and Probabilistic Systems. |
| Record Nr. | UNISA-996418291303316 |
| Cham, Switzerland : , : Springer, , [2020] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Technology for Verification and Analysis : 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019, Proceedings / / edited by Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza
| Automated Technology for Verification and Analysis : 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28–31, 2019, Proceedings / / edited by Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (xi, 552 pages) : illustrations |
| Disciplina |
004.015113
006.333 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer logic Mathematical logic Artificial intelligence Algorithms Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages Artificial Intelligence Algorithm Analysis and Problem Complexity |
| ISBN | 3-030-31784-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | A Note on Game Theory and Verification -- Lazy Abstraction-Based Controller Synthesis -- Truth Assignments as Conditional Autarkies -- Can We Trust Autonomous Systems? Boundaries and Risks -- Teaching Stratego to Play Ball : Optimal Synthesis for Continuous Space MDPs -- Using Symmetry Transformations in Equivariant Dynamical Systems for their Safety Verification -- Parametric Timed Model Checking for Guaranteeing Timed Opacity -- Adaptive Online First-Order Monitoring -- Multi-Head Monitoring of Metric Temporal Logic -- An Efficient Algorithm for Computing Causal Trace Sets in Causality Checking -- Conditional Testing: O -the-Shelf Combination of Test-Case Generators -- Enhancing Symbolic Execution of Heap-based Programs with Separation Logic for Test Input Generation -- BUBEN: Automated Library Abstractions Enabling Scalable Bug Detection for Large Programs with I/O and Complex Environment -- KLUZZER: Whitebox Fuzzing on top of LLVM -- Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops -- Chain Free String Constraints -- Synthesizing Efficient Low-Precision Kernels -- New Optimizations and Heuristics for Determinization of Büchi Automata -- Approximate Automata for Omega-regular Languages -- DEQ : Equivalence Checker for Deterministic Register Automata -- LTL3TELA: Small Deterministic or Nondeterministic Automata from LTL -- Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems -- Reactive Synthesis of Graphical User Interface Glue Code -- Semantic Labelling and Learning for Parity Game Solving in LTL Synthesis -- Program Repair for Hyperproperties -- Generic Emptiness Check for Fun and Profit -- Deciding Fast Termination for Probabilistic VASS with Nondeterminism -- Are Parametric Markov Chains Monotonic -- Efficient Information-Flow Verification under Speculative Execution -- Model Checking Data Flows in Concurrent Network Updates.-Performance Evaluation of NDN Data Plane Using Statistical Model Checking. |
| Record Nr. | UNINA-9910349272103321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Technology for Verification and Analysis : 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings / / edited by Shuvendu K. Lahiri, Chao Wang
| Automated Technology for Verification and Analysis : 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7-10, 2018, Proceedings / / edited by Shuvendu K. Lahiri, Chao Wang |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XIII, 560 p. 133 illus.) |
| Disciplina |
004.015113
006.333 |
| Collana | Programming and Software Engineering |
| Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computer security Computer simulation Computer logic Mathematical logic Software Engineering Programming Languages, Compilers, Interpreters Systems and Data Security Simulation and Modeling Logics and Meanings of Programs Mathematical Logic and Formal Languages |
| ISBN | 3-030-01090-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Formal Methods -- Verification -- Program Synthesis -- Model Checking -- Theorem Proving -- Software Verification -- SAT Solver -- SMT Solver -- Automation Logic. |
| Record Nr. | UNINA-9910349402203321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Case-Based Reasoning Research and Development : 27th International Conference, ICCBR 2019, Otzenhausen, Germany, September 8–12, 2019, Proceedings / / edited by Kerstin Bach, Cindy Marling
| Case-Based Reasoning Research and Development : 27th International Conference, ICCBR 2019, Otzenhausen, Germany, September 8–12, 2019, Proceedings / / edited by Kerstin Bach, Cindy Marling |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XXI, 405 p. 158 illus., 88 illus. in color.) |
| Disciplina |
153.43
006.333 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Application software Information storage and retrieval Data mining Artificial Intelligence Computer Appl. in Administrative Data Processing Information Storage and Retrieval Data Mining and Knowledge Discovery |
| ISBN | 3-030-29249-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Comparing Similarity Learning with Taxonomies and One-Mode Projection in Context of the FEATURE-TAK Framework -- An Algorithm Independent Case-Based Explanation Approach for Recommender Systems Using Interaction Graphs -- Explanation of Recommender Systems using Formal Concept Analysis -- FLEA-CBR { A Flexible Alternative to the Classic 4R Cycle of Lazy Learned Screening for Efficient Recruitment -- Case-Based Reasoning -- On the Generalization Capabilities of Sharp Minima in Case-Based Reasoning -- CBR Confidence as a Basis for Confidence in Black Box Systems -- Probabilistic Selection of Case-Based Explanations in an Underwater Mine Clearance Domain -- A Data-Driven Approach for Determining Weights in Global Similarity Functions -- Personalized case-based explanation of matrix factorization Recommendations -- How Case-Based Reasoning Explains Neural Networks -- Predicting Grass Growth for Sustainable Dairy Farming: A CBR System Using Bayesian Case-Exclusion and Post-Hoc, Personalized Explanation-by-Example (XAI) -- Learning Workflow Embeddings to Improve the Performance of Similarity-Based Retrieval for Process-Oriented Case-Based Reasoning -- On Combining Case Adaptation Rules -- Semantic Textual Similarity Measures for Case-Based Retrieval of Argument Graphs -- An approach to case-based reasoning based on local enrichment of the case base -- Improving analogical extrapolation using case pair competence -- Towards Finding Flow in Tetris -- Scoring Performance on the Y-Balance Test -- An Optimal Case-base Maintenance Method for Compositional Adaptation Applications -- Towards Human-like Bots using Online Interactive Case-Based Reasoning -- Show me your friends, I'll tell you who you are: Recommending products based on hidden evidence -- A Tale of Two Communities: An Analysis of Three Decades of Case-Based Reasoning Research -- Going Further with Cases: Using Case-Based Reasoning to Recommend Pacing Strategies for Ultra-Marathon Runners -- NOD-CC: A Hybrid CBR-CNN Architecture for Novel Object Discovery -- Adaptation of Scientific Workflows by Means of Process-Oriented Case-Based Reasoning. |
| Record Nr. | UNINA-9910349301403321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Case-Based Reasoning Research and Development : 26th International Conference, ICCBR 2018, Stockholm, Sweden, July 9-12, 2018, Proceedings / / edited by Michael T. Cox, Peter Funk, Shahina Begum
| Case-Based Reasoning Research and Development : 26th International Conference, ICCBR 2018, Stockholm, Sweden, July 9-12, 2018, Proceedings / / edited by Michael T. Cox, Peter Funk, Shahina Begum |
| Edizione | [1st ed. 2018.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 |
| Descrizione fisica | 1 online resource (XIV, 628 p. 221 illus.) |
| Disciplina |
153.43
006.333 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Application software Information storage and retrieval User interfaces (Computer systems) Mathematical logic Special purpose computers Artificial Intelligence Computer Appl. in Administrative Data Processing Information Storage and Retrieval User Interfaces and Human Computer Interaction Mathematical Logic and Formal Languages Special Purpose and Application-Based Systems |
| ISBN | 3-030-01081-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910349402103321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2018 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
