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-25 [[electronic resource] ] : 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings / / edited by Amy P. Felty, Aart Middeldorp
| Automated Deduction - CADE-25 [[electronic resource] ] : 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings / / edited by Amy P. Felty, Aart Middeldorp |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XXVIII, 640 p. 93 illus.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Optical data processing
Artificial intelligence Algorithms Application software Computers Pattern recognition Image Processing and Computer Vision Artificial Intelligence Algorithm Analysis and Problem Complexity Information Systems Applications (incl. Internet) Computation by Abstract Devices Pattern Recognition |
| ISBN | 3-319-21401-2 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automated deduction.- Foundations -- Applications -- Implementations.- Practical experience. |
| Record Nr. | UNISA-996204581903316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Deduction - CADE-25 : 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings / / edited by Amy P. Felty, Aart Middeldorp
| Automated Deduction - CADE-25 : 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings / / edited by Amy P. Felty, Aart Middeldorp |
| Edizione | [1st ed. 2015.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 |
| Descrizione fisica | 1 online resource (XXVIII, 640 p. 93 illus.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Computer vision
Artificial intelligence Algorithms Application software Computer science Pattern recognition systems Computer Vision Artificial Intelligence Computer and Information Systems Applications Theory of Computation Automated Pattern Recognition |
| ISBN | 3-319-21401-2 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automated deduction.- Foundations -- Applications -- Implementations.- Practical experience. |
| Record Nr. | UNINA-9910485052603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Deduction – CADE 26 [[electronic resource] ] : 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings / / edited by Leonardo de Moura
| Automated Deduction – CADE 26 [[electronic resource] ] : 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings / / edited by Leonardo de Moura |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XI, 582 p. 87 illus.) |
| Disciplina | 511.36028563 |
| 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 |
| ISBN | 3-319-63046-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automated deduction -- Including foundations -- Applications.-Implementations -- Practical experience. |
| Record Nr. | UNISA-996466306303316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Deduction – CADE 26 : 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings / / edited by Leonardo de Moura
| Automated Deduction – CADE 26 : 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6–11, 2017, Proceedings / / edited by Leonardo de Moura |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XI, 582 p. 87 illus.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Machine theory Computer science Software engineering Algorithms Artificial Intelligence Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Software Engineering |
| ISBN | 3-319-63046-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automated deduction -- Including foundations -- Applications.-Implementations -- Practical experience. |
| Record Nr. | UNINA-9910483401903321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Deduction – CADE 27 [[electronic resource] ] : 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings / / edited by Pascal Fontaine
| Automated Deduction – CADE 27 [[electronic resource] ] : 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings / / edited by Pascal Fontaine |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XXIII, 582 p. 1901 illus., 56 illus. in color.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Software engineering Computer system failures Mathematical logic Computer logic Artificial Intelligence Software Engineering System Performance and Evaluation Mathematical Logic and Formal Languages Logics and Meanings of Programs |
| ISBN | 3-030-29436-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automated Reasoning for Security Protocols -- Computer Deduction and (Formal) Proofs in Mathematics -- From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT -- The CADE-27 ATP System Competition - CASC-27 -- Unification modulo Lists with Reverse - Relation with Certain Word Equations -- On the Width of Regular Classes of Finite Structures -- Extending SMT solvers to Higher-Order Logic -- Superposition with Lambdas -- Restricted Combinatory Unification -- dLi: Definite Descriptions in Differential Dynamic Logic -- SPASS-SATT { A CDCL(LA) Solver -- GRUNGE: A Grand Unified ATP Challenge -- Model Completeness, Covers and Superposition -- A Tableaux Calculus for Default Intuitionistic Logic -- NIL: Learning Nonlinear Interpolants -- ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E -- Towards Physical Hybrid Systems -- SCL -- Clause Learning from Simple Models -- Names are not just Sound and Smoke: Word Embeddings for Axiom Selection -- Computing Expected Runtimes for Constant Probability Programs -- Automatic Generation of Logical Models with AGES -- Automata Terms in a Lazy WSkS Decision Procedure -- Confluence by Critical Pair Analysis Revisited -- Composing Proof Terms -- Combining ProVerif and Automated Theorem Provers for Security Protocol Verification -- Towards Bit-Width-Independent Proofs in SMT Solvers -- On Invariant Synthesis for Parametric Systems -- The Aspect Calculus -- Uniform Substitution At One Fell Swoop -- A Formally Verified Abstract Account of Gödel's Incompleteness Theorems -- Old or Heavy? Decaying Gracefully with Age/Weight Shapes -- Induction in Saturation-Based Proof Search -- Faster, Higher, Stronger: E 2.3 -- Certified Equational Reasoning via Ordered Completion -- JGXYZ - An ATP System for Gap and Glut Logics -- GKC: a Reasoning System for Large Knowledge Bases -- Optimization Modulo the Theory of Floating-Point Numbers -- FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. . |
| Record Nr. | UNISA-996466439203316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Deduction – CADE 27 : 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings / / edited by Pascal Fontaine
| Automated Deduction – CADE 27 : 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings / / edited by Pascal Fontaine |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XXIII, 582 p. 1901 illus., 56 illus. in color.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Software engineering Electronic digital computers - Evaluation Machine theory Computer science Artificial Intelligence Software Engineering System Performance and Evaluation Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming |
| ISBN | 3-030-29436-6 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Automated Reasoning for Security Protocols -- Computer Deduction and (Formal) Proofs in Mathematics -- From Counter-Model-based Quantifier Instantiation to Quantifier Elimination in SMT -- The CADE-27 ATP System Competition - CASC-27 -- Unification modulo Lists with Reverse - Relation with Certain Word Equations -- On the Width of Regular Classes of Finite Structures -- Extending SMT solvers to Higher-Order Logic -- Superposition with Lambdas -- Restricted Combinatory Unification -- dLi: Definite Descriptions in Differential Dynamic Logic -- SPASS-SATT { A CDCL(LA) Solver -- GRUNGE: A Grand Unified ATP Challenge -- Model Completeness, Covers and Superposition -- A Tableaux Calculus for Default Intuitionistic Logic -- NIL: Learning Nonlinear Interpolants -- ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E -- Towards Physical Hybrid Systems -- SCL -- Clause Learning from Simple Models -- Names are not just Sound and Smoke: Word Embeddings for Axiom Selection -- Computing Expected Runtimes for Constant Probability Programs -- Automatic Generation of Logical Models with AGES -- Automata Terms in a Lazy WSkS Decision Procedure -- Confluence by Critical Pair Analysis Revisited -- Composing Proof Terms -- Combining ProVerif and Automated Theorem Provers for Security Protocol Verification -- Towards Bit-Width-Independent Proofs in SMT Solvers -- On Invariant Synthesis for Parametric Systems -- The Aspect Calculus -- Uniform Substitution At One Fell Swoop -- A Formally Verified Abstract Account of Gödel's Incompleteness Theorems -- Old or Heavy? Decaying Gracefully with Age/Weight Shapes -- Induction in Saturation-Based Proof Search -- Faster, Higher, Stronger: E 2.3 -- Certified Equational Reasoning via Ordered Completion -- JGXYZ - An ATP System for Gap and Glut Logics -- GKC: a Reasoning System for Large Knowledge Bases -- Optimization Modulo the Theory of Floating-Point Numbers -- FAME(Q): An Automated Tool for Forgetting in Description Logics with Qualified Number Restrictions. . |
| Record Nr. | UNINA-9910349305403321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II / / edited by Nicolas Peltier, Viorica Sofronie-Stokkermans
| Automated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II / / edited by Nicolas Peltier, Viorica Sofronie-Stokkermans |
| Edizione | [1st ed. 2020.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 |
| Descrizione fisica | 1 online resource (521 pages) |
| Disciplina |
004.015113
511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Machine theory
Artificial intelligence Computer science Software engineering Compilers (Computer programs) Computer programming Formal Languages and Automata Theory Artificial Intelligence Computer Science Logic and Foundations of Programming Software Engineering Compilers and Interpreters Programming Techniques |
| ISBN | 3-030-51054-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Interactive Theorem Proving/ HOL -- Competing inheritance paths in dependent type theory: a case study in functional analysis -- A Lean tactic for normalising ring expressions with exponents (short paper) -- Practical proof search for Coq by type inhabitation -- Quotients of Bounded Natural Functors -- Trakhtenbrot’s Theorem in Coq -- Deep Generation of Coq Lemma Names Using Elaborated Terms -- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs -- Validating Mathematical Structures -- Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description) -- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages -- Formalizations -- Formalizing the Face Lattice of Polyhedra -- Algebraically Closed Fields in Isabelle/HOL -- Formalization of Forcing in Isabelle/ZF -- Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL -- Formal Proof of the Group Law for Edwards Elliptic Curves -- Verifying Farad_zev-Read type Isomorph-Free Exhaustive Generation -- Verification -- Verified Approximation Algorithms -- Efficient Verified Implementation of Introsort and Pdqsort -- A Fast Verified Liveness Analysis in SSA form -- Verification of Closest Pair of Points Algorithms -- Reasoning Systems and Tools -- A Polymorphic Vampire (short paper) -- N-PAT: A Nested Model-Checker (system description) -- HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description) -- Implementing superposition in iProver (system description) -- Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description) -- Make E Smart Again -- Automatically Proving and Disproving Feasibility Conditions -- µ-term: Verify Termination Properties Automatically (system description) -- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) -- The Imandra Automated Reasoning System (system description) -- A Programmer’s Text Editor for a Logical Theory: The SUMOjEdit Editor (system description) -- Sequoia: a playground for logicians (system description) -- Prolog Technology Reinforcement Learning Prover (system description). |
| Record Nr. | UNINA-9910409661803321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Reasoning with Analytic Tableaux and Related Methods : 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings / / edited by Serenella Cerrito, Andrei Popescu
| Automated Reasoning with Analytic Tableaux and Related Methods : 28th International Conference, TABLEAUX 2019, London, UK, September 3-5, 2019, Proceedings / / edited by Serenella Cerrito, Andrei Popescu |
| Edizione | [1st ed. 2019.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 |
| Descrizione fisica | 1 online resource (XXI, 477 p. 2851 illus., 28 illus. in color.) |
| Disciplina |
511.3
511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Machine theory Computer science - Mathematics Software engineering Electronic digital computers - Evaluation Artificial Intelligence Formal Languages and Automata Theory Mathematical Applications in Computer Science Software Engineering System Performance and Evaluation |
| ISBN | 3-030-29026-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNINA-9910349303903321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2019 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25–28, 2017, Proceedings / / edited by Renate A. Schmidt, Cláudia Nalon
| Automated Reasoning with Analytic Tableaux and Related Methods [[electronic resource] ] : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25–28, 2017, Proceedings / / edited by Renate A. Schmidt, Cláudia Nalon |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XII, 381 p. 75 illus.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer programming Software engineering Programming languages (Electronic computers) Computer logic Artificial Intelligence Mathematical Logic and Formal Languages Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters Logics and Meanings of Programs |
| ISBN | 3-319-66902-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Sequents systems -- Tableaux -- Transitive closure and cyclic proofs -- Formalization and complexity. |
| Record Nr. | UNISA-996466251803316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25–28, 2017, Proceedings / / edited by Renate A. Schmidt, Cláudia Nalon
| Automated Reasoning with Analytic Tableaux and Related Methods : 26th International Conference, TABLEAUX 2017, Brasília, Brazil, September 25–28, 2017, Proceedings / / edited by Renate A. Schmidt, Cláudia Nalon |
| Edizione | [1st ed. 2017.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
| Descrizione fisica | 1 online resource (XII, 381 p. 75 illus.) |
| Disciplina | 511.36028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Machine theory Computer programming Software engineering Compilers (Computer programs) Computer science Artificial Intelligence Formal Languages and Automata Theory Programming Techniques Software Engineering Compilers and Interpreters Computer Science Logic and Foundations of Programming |
| ISBN | 3-319-66902-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Sequents systems -- Tableaux -- Transitive closure and cyclic proofs -- Formalization and complexity. |
| Record Nr. | UNINA-9910482960003321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
