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 reasoning : 4th International Joint Conference, IJCAR 2008, Sydney, NSW, Australia, August 12-15, 2008, proceedings / / Alessandro Armando, Peter Baumgartner, Gilles Dowek (Eds.)
| Automated reasoning : 4th International Joint Conference, IJCAR 2008, Sydney, NSW, Australia, August 12-15, 2008, proceedings / / Alessandro Armando, Peter Baumgartner, Gilles Dowek (Eds.) |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [2008] |
| Descrizione fisica | 1 online resource (XII, 556 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Artificial intelligence
Computer science |
| ISBN | 3-540-71070-1 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1: Invited Talk -- Software Verification: Roles and Challenges for Automatic Decision Procedures -- Session 2: Specific Theories -- Proving Bounds on Real-Valued Functions with Computations -- Linear Quantifier Elimination -- Quantitative Separation Logic and Programs with Lists -- On Automating the Calculus of Relations -- Session 3: Automated Verification -- Towards SMT Model Checking of Array-Based Systems -- Preservation of Proof Obligations from Java to the Java Virtual Machine -- Efficient Well-Definedness Checking -- Session 4: Protocol Verification -- Proving Group Protocols Secure Against Eavesdroppers -- Session 5: System Descriptions 1 -- Automated Implicit Computational Complexity Analysis (System Description) -- LogAnswer - A Deduction-Based Question Answering System (System Description) -- A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description) -- The Abella Interactive Theorem Prover (System Description) -- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) -- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) -- The Complexity of Conjunctive Query Answering in Expressive Description Logics -- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments -- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse -- Session 8: Herbrand Award Ceremony -- Automata-Based Axiom Pinpointing -- Individual Reuse in Description Logic Reasoning -- The Logical Difference Problem for Description Logic Terminologies -- Session 10: System Descriptions 2 -- Aligator: A Mathematica Package for Invariant Generation (System Description) -- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) -- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description) -- An Experimental Evaluation of Global Caching for (System Description) -- Multi-completion with Termination Tools (System Description) -- MTT: The Maude Termination Tool (System Description) -- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) -- Canonicity! -- Unification and Matching Modulo Leaf-Permutative Equational Presentations -- Modularity of Confluence -- Automated Complexity Analysis Based on the Dependency Pair Method -- Canonical Inference for Implicational Systems -- Challenges in the Automated Verification of Security Protocols -- Session 14: Theorem Proving 1 -- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets -- Proof Systems for Effectively Propositional Logic -- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance -- CASC-J4 The 4th IJCAR ATP System Competition -- Session 16: Theorem Proving 2 -- Labelled Splitting -- Engineering DPLL(T) + Saturation -- THF0 – The Core of the TPTP Language for Higher-Order Logic -- Focusing in Linear Meta-logic -- Certifying a Tree Automata Completion Checker -- Automated Induction with Constrained Tree Automata. |
| Record Nr. | UNINA-9910484590403321 |
| Berlin ; ; Heidelberg : , : Springer, , [2008] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Automated reasoning : 4th International Joint Conference, IJCAR 2008, Sydney, NSW, Australia, August 12-15, 2008, proceedings / / Alessandro Armando, Peter Baumgartner, Gilles Dowek (Eds.)
| Automated reasoning : 4th International Joint Conference, IJCAR 2008, Sydney, NSW, Australia, August 12-15, 2008, proceedings / / Alessandro Armando, Peter Baumgartner, Gilles Dowek (Eds.) |
| Edizione | [1st ed. 2008.] |
| Pubbl/distr/stampa | Berlin ; ; Heidelberg : , : Springer, , [2008] |
| Descrizione fisica | 1 online resource (XII, 556 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Artificial intelligence
Computer science |
| ISBN | 3-540-71070-1 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1: Invited Talk -- Software Verification: Roles and Challenges for Automatic Decision Procedures -- Session 2: Specific Theories -- Proving Bounds on Real-Valued Functions with Computations -- Linear Quantifier Elimination -- Quantitative Separation Logic and Programs with Lists -- On Automating the Calculus of Relations -- Session 3: Automated Verification -- Towards SMT Model Checking of Array-Based Systems -- Preservation of Proof Obligations from Java to the Java Virtual Machine -- Efficient Well-Definedness Checking -- Session 4: Protocol Verification -- Proving Group Protocols Secure Against Eavesdroppers -- Session 5: System Descriptions 1 -- Automated Implicit Computational Complexity Analysis (System Description) -- LogAnswer - A Deduction-Based Question Answering System (System Description) -- A High-Level Implementation of a System for Automated Reasoning with Default Rules (System Description) -- The Abella Interactive Theorem Prover (System Description) -- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description) -- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) -- The Complexity of Conjunctive Query Answering in Expressive Description Logics -- A General Tableau Method for Deciding Description Logics, Modal Logics and Related First-Order Fragments -- Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse -- Session 8: Herbrand Award Ceremony -- Automata-Based Axiom Pinpointing -- Individual Reuse in Description Logic Reasoning -- The Logical Difference Problem for Description Logic Terminologies -- Session 10: System Descriptions 2 -- Aligator: A Mathematica Package for Invariant Generation (System Description) -- leanCoP 2.0 and ileanCoP 1.2: High Performance Lean Theorem Proving in Classical and Intuitionistic Logic (System Descriptions) -- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description) -- An Experimental Evaluation of Global Caching for (System Description) -- Multi-completion with Termination Tools (System Description) -- MTT: The Maude Termination Tool (System Description) -- Celf – A Logical Framework for Deductive and Concurrent Systems (System Description) -- Canonicity! -- Unification and Matching Modulo Leaf-Permutative Equational Presentations -- Modularity of Confluence -- Automated Complexity Analysis Based on the Dependency Pair Method -- Canonical Inference for Implicational Systems -- Challenges in the Automated Verification of Security Protocols -- Session 14: Theorem Proving 1 -- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets -- Proof Systems for Effectively Propositional Logic -- MaLARea SG1 - Machine Learner for Automated Reasoning with Semantic Guidance -- CASC-J4 The 4th IJCAR ATP System Competition -- Session 16: Theorem Proving 2 -- Labelled Splitting -- Engineering DPLL(T) + Saturation -- THF0 – The Core of the TPTP Language for Higher-Order Logic -- Focusing in Linear Meta-logic -- Certifying a Tree Automata Completion Checker -- Automated Induction with Constrained Tree Automata. |
| Record Nr. | UNISA-996465913903316 |
| Berlin ; ; Heidelberg : , : Springer, , [2008] | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Higher-Order Algebra, Logic, and Term Rewriting [[electronic resource] ] : Second International Workshop, HOA '95, Paderborn, Germany, September 1995. Selected Papers / / edited by Gilles Dowek, Jan Heering, Karl Meinke, Bernhard Möller
| Higher-Order Algebra, Logic, and Term Rewriting [[electronic resource] ] : Second International Workshop, HOA '95, Paderborn, Germany, September 1995. Selected Papers / / edited by Gilles Dowek, Jan Heering, Karl Meinke, Bernhard Möller |
| Edizione | [1st ed. 1996.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 |
| Descrizione fisica | 1 online resource (VIII, 296 p.) |
| Disciplina | 511.3 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Computers
Computer logic Mathematical logic Theory of Computation Logics and Meanings of Programs Mathematical Logic and Formal Languages Mathematical Logic and Foundations |
| ISBN | 3-540-68389-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Term graph rewriting -- Approximation and normalization results for typeable term rewriting systems -- Modular properties of algebraic type systems -- Collapsing partial combinatory algebras -- A complete proof system for Nested Term Graphs -- R n - and G n -logics -- The variable containment problem -- Higher-order equational logic for specification, simulation and testing -- The correctness of a higher-order lazy functional language implementation: An exercise in mechanical theorem proving -- Assertions and recursions -- Development closed critical pairs -- Two different strong normalization proofs? -- Third-order matching in the polymorphic lambda calculus -- Higher-order algebra with transfinite types -- Abstraction of hardware construction. |
| Record Nr. | UNISA-996465596103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Logique, dynamique et cognition / / Jean-Baptiste Joinet
| Logique, dynamique et cognition / / Jean-Baptiste Joinet |
| Autore | Bailly Francis |
| Pubbl/distr/stampa | Paris, : Éditions de la Sorbonne, 2014 |
| Descrizione fisica | 1 online resource (239 p.) |
| Altri autori (Persone) |
BonnayDenis
DehornoyPatrick DowekGilles GirardJean-Yves JoinetJean-Baptiste LivetPierre LongoGiuseppe PaulThierry TronçonSamuel |
| Soggetto topico |
Philosophy
logique mathématique temps sciences de la nature mécanique quantique |
| Soggetto non controllato |
logique mathématique
sciences de la nature temps mécanique quantique |
| ISBN | 9782859448103 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | fre |
| Record Nr. | UNINA-9910168752803321 |
Bailly Francis
|
||
| Paris, : Éditions de la Sorbonne, 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Rewriting and Typed Lambda Calculi [[electronic resource] ] : Joint International Conferences, RTA and TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings / / edited by Gilles Dowek
| Rewriting and Typed Lambda Calculi [[electronic resource] ] : Joint International Conferences, RTA and TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings / / edited by Gilles Dowek |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXII, 491 p. 58 illus.) |
| Disciplina | 005.131 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science—Mathematics Computer science Artificial intelligence Mathematical logic Formal Languages and Automata Theory Mathematics of Computing Computer Science Logic and Foundations of Programming Symbolic and Algebraic Manipulation Artificial Intelligence Mathematical Logic and Foundations |
| ISBN | 3-319-08918-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Process Types as a Descriptive Tool for Interaction: Control and the Pi-Calculus -- Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk) -- Unnesting of Copatterns -- Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams -- Predicate Abstraction of Rewrite Theories -- Unification and Logarithmic Space -- Ramsey Theorem as an Intuitionistic Property of Well Founded Relations -- A Model of Countable Nondeterminism in Guarded Type Theory -- Cut Admissibility by Saturation -- Automatic Evaluation of Context-Free Grammars (System Description) -- Tree Automata with Height Constraints between Brothers -- A Coinductive Confluence Proof for Infinitary Lambda-Calculus -- An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting -- Preciseness of Subtyping on Intersection and Union Types -- Abstract Datatypes for Real Numbers in Type Theory -- Self Types for Dependently Typed Lambda Encodings -- First-Order Formative Rules -- Automated Complexity Analysis Based on Context-Sensitive Rewriting -- Amortised Resource Analysis and Typed Polynomial Interpretations -- Confluence by Critical Pair Analysis -- Proof Terms for Infinitary Rewriting -- Construction of Retractile Proof Structures -- Local States in String Diagrams -- Reduction System for Extensional Lambda-mu Calculus -- The Structural Theory of Pure Type Systems -- Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB -- Implicational Relevance Logic is 2-ExpTime-Complete -- Near Semi-rings and Lambda Calculus -- All-Path Reachability Logic -- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs -- Conditional Confluence (System Description) -- Nagoya Termination Tool -- Termination of Cycle Rewriting. |
| Record Nr. | UNISA-996213697503316 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Rewriting and Typed Lambda Calculi : Joint International Conferences, RTA and TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings / / edited by Gilles Dowek
| Rewriting and Typed Lambda Calculi : Joint International Conferences, RTA and TLCA 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014, Proceedings / / edited by Gilles Dowek |
| Edizione | [1st ed. 2014.] |
| Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 |
| Descrizione fisica | 1 online resource (XXII, 491 p. 58 illus.) |
| Disciplina | 005.131 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science—Mathematics Computer science Artificial intelligence Mathematical logic Formal Languages and Automata Theory Mathematics of Computing Computer Science Logic and Foundations of Programming Symbolic and Algebraic Manipulation Artificial Intelligence Mathematical Logic and Foundations |
| ISBN | 3-319-08918-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Process Types as a Descriptive Tool for Interaction: Control and the Pi-Calculus -- Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk) -- Unnesting of Copatterns -- Proving Confluence of Term Rewriting Systems via Persistency and Decreasing Diagrams -- Predicate Abstraction of Rewrite Theories -- Unification and Logarithmic Space -- Ramsey Theorem as an Intuitionistic Property of Well Founded Relations -- A Model of Countable Nondeterminism in Guarded Type Theory -- Cut Admissibility by Saturation -- Automatic Evaluation of Context-Free Grammars (System Description) -- Tree Automata with Height Constraints between Brothers -- A Coinductive Confluence Proof for Infinitary Lambda-Calculus -- An Implicit Characterization of the Polynomial-Time Decidable Sets by Cons-Free Rewriting -- Preciseness of Subtyping on Intersection and Union Types -- Abstract Datatypes for Real Numbers in Type Theory -- Self Types for Dependently Typed Lambda Encodings -- First-Order Formative Rules -- Automated Complexity Analysis Based on Context-Sensitive Rewriting -- Amortised Resource Analysis and Typed Polynomial Interpretations -- Confluence by Critical Pair Analysis -- Proof Terms for Infinitary Rewriting -- Construction of Retractile Proof Structures -- Local States in String Diagrams -- Reduction System for Extensional Lambda-mu Calculus -- The Structural Theory of Pure Type Systems -- Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB -- Implicational Relevance Logic is 2-ExpTime-Complete -- Near Semi-rings and Lambda Calculus -- All-Path Reachability Logic -- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs -- Conditional Confluence (System Description) -- Nagoya Termination Tool -- Termination of Cycle Rewriting. |
| Record Nr. | UNINA-9910484594603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||