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-23 [[electronic resource] ] : 23rd International Conference on Automated Deduction, Wrocław, Poland, July 31 -- August 5, 2011, Proceedings / / edited by Nikolaj Bjørner, Viorica Sofronie-Stokkermans
| Automated Deduction -- CADE-23 [[electronic resource] ] : 23rd International Conference on Automated Deduction, Wrocław, Poland, July 31 -- August 5, 2011, Proceedings / / edited by Nikolaj Bjørner, Viorica Sofronie-Stokkermans |
| Edizione | [1st ed. 2011.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 |
| Descrizione fisica | 1 online resource (XIII, 508 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer logic Software engineering Artificial Intelligence Mathematical Logic and Formal Languages Logics and Meanings of Programs Software Engineering |
| ISBN | 3-642-22438-5 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996465476903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Reasoning [[electronic resource] ] : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I / / edited by Nicolas Peltier, Viorica Sofronie-Stokkermans
| Automated Reasoning [[electronic resource] ] : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I / / 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 (553 pages) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Mathematical logic
Artificial intelligence Computer logic Software engineering Programming languages (Electronic computers) Computer programming Mathematical Logic and Formal Languages Artificial Intelligence Logics and Meanings of Programs Software Engineering Programming Languages, Compilers, Interpreters Programming Techniques |
| ISBN | 3-030-51074-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Paper -- Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints -- SAT; SMT and QBF -- An SMT Theory of Fixed-Point Arithmetic -- Covered Clauses Are Not Propagation Redundant -- The Resolution of Keller’s Conjecture -- How QBF Expansion Makes Strategy Extraction Hard -- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates -- Solving bit-vectors with MCSAT: explanations from bits and pieces -- Monadic Decomposition in Integer Linear Arithmetic -- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis -- Decision Procedures and Combination of Theories -- Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols -- Combined Covers and Beth Definability -- Deciding Simple Infinity Axiom Sets with one Binary Relation by Means of Superpostulates -- A Decision Procedure for String to Code Point Conversion -- Politeness for The Theory of Algebraic Datatypes -- Superposition -- A Knuth-Bendix-Like Ordering for Orienting Combinator Equations -- A Combinator-Based Superposition Calculus for Higher-Order Logic -- Subsumption Demodulation in First-Order Theorem Proving -- A Comprehensive Framework for Saturation Theorem Proving -- Proof Procedures -- Possible Models Computation and Revision - A Practical Approach -- SGGS Decision Procedures -- Integrating Induction and Coinduction via Closure Operators and Proof Cycles -- Logic-Independent Proof Search in Logical Frameworks (short paper) -- Layered Clause Selection for Theory Reasoning (short paper) -- Non Classical Logics -- Description Logics with Concrete Domains and General Concept Inclusions Revisited -- A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic -- Constructive Hybrid Games -- Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) -- NP Reasoning in the Monotone µ-Calculus -- Soft subexponentials and multiplexing -- Mechanised Modal Model Theory. |
| Record Nr. | UNISA-996418306103316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Reasoning [[electronic resource] ] : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II / / edited by Nicolas Peltier, Viorica Sofronie-Stokkermans
| Automated Reasoning [[electronic resource] ] : 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 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Mathematical logic
Artificial intelligence Computer logic Software engineering Programming languages (Electronic computers) Computer programming Mathematical Logic and Formal Languages Artificial Intelligence Logics and Meanings of Programs Software Engineering Programming Languages, Compilers, 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. | UNISA-996418305603316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
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 |
Mathematical logic
Artificial intelligence Computer logic Software engineering Programming languages (Electronic computers) Computer programming Mathematical Logic and Formal Languages Artificial Intelligence Logics and Meanings of Programs Software Engineering Programming Languages, Compilers, 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 : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I / / edited by Nicolas Peltier, Viorica Sofronie-Stokkermans
| Automated Reasoning : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I / / 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 (553 pages) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Mathematical logic
Artificial intelligence Computer logic Software engineering Programming languages (Electronic computers) Computer programming Mathematical Logic and Formal Languages Artificial Intelligence Logics and Meanings of Programs Software Engineering Programming Languages, Compilers, Interpreters Programming Techniques |
| ISBN | 3-030-51074-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Paper -- Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints -- SAT; SMT and QBF -- An SMT Theory of Fixed-Point Arithmetic -- Covered Clauses Are Not Propagation Redundant -- The Resolution of Keller’s Conjecture -- How QBF Expansion Makes Strategy Extraction Hard -- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates -- Solving bit-vectors with MCSAT: explanations from bits and pieces -- Monadic Decomposition in Integer Linear Arithmetic -- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis -- Decision Procedures and Combination of Theories -- Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols -- Combined Covers and Beth Definability -- Deciding Simple Infinity Axiom Sets with one Binary Relation by Means of Superpostulates -- A Decision Procedure for String to Code Point Conversion -- Politeness for The Theory of Algebraic Datatypes -- Superposition -- A Knuth-Bendix-Like Ordering for Orienting Combinator Equations -- A Combinator-Based Superposition Calculus for Higher-Order Logic -- Subsumption Demodulation in First-Order Theorem Proving -- A Comprehensive Framework for Saturation Theorem Proving -- Proof Procedures -- Possible Models Computation and Revision - A Practical Approach -- SGGS Decision Procedures -- Integrating Induction and Coinduction via Closure Operators and Proof Cycles -- Logic-Independent Proof Search in Logical Frameworks (short paper) -- Layered Clause Selection for Theory Reasoning (short paper) -- Non Classical Logics -- Description Logics with Concrete Domains and General Concept Inclusions Revisited -- A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic -- Constructive Hybrid Games -- Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) -- NP Reasoning in the Monotone µ-Calculus -- Soft subexponentials and multiplexing -- Mechanised Modal Model Theory. |
| Record Nr. | UNINA-9910409661703321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2020 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Frontiers of Combining Systems [[electronic resource] ] : 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings / / edited by Cesare Tinelli, Viorica Sofronie-Stokkermans
| Frontiers of Combining Systems [[electronic resource] ] : 8th International Symposium, FroCoS 2011, Saarbrücken, Germany, October 5-7, 2011. Proceedings / / edited by Cesare Tinelli, Viorica Sofronie-Stokkermans |
| Edizione | [1st ed. 2011.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 |
| Descrizione fisica | 1 online resource (VIII, 275 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Mathematical logic Computer logic Software engineering Algorithms Computer programming Artificial Intelligence Mathematical Logic and Formal Languages Logics and Meanings of Programs Software Engineering Algorithm Analysis and Problem Complexity Programming Techniques |
| ISBN | 3-642-24364-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996466013903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2011 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||