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 |
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. | UNINA-9910485052603321 |
| Cham : , : Springer International Publishing : , : Imprint : Springer, , 2015 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Logic for Programming, Artificial Intelligence, and Reasoning [[electronic resource] ] : 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013, Proceedings / / edited by Ken McMillan, Aart Middeldorp, Andrei Voronkov
| Logic for Programming, Artificial Intelligence, and Reasoning [[electronic resource] ] : 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013, Proceedings / / edited by Ken McMillan, Aart Middeldorp, Andrei Voronkov |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XIV, 794 p. 178 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Artificial intelligence Computer science Machine theory Computer programming Compilers (Computer programs) Software Engineering Artificial Intelligence Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Programming Techniques Compilers and Interpreters |
| ISBN | 3-642-45221-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics -- May-Happen-in-Parallel Analysis for Priority-Based Scheduling -- The Complexity of Clausal Fragments of LTL -- A Semantic Basis for Proof Queries and Transformations -- Expressive Path Queries on Graphs with Data -- Proving Infinite Satisfiability -- SAT-Based Preprocessing for MaxSAT -- Dynamic and Static Symmetry Breaking in Answer Set Programming -- HOL Based First-Order Modal Logic Provers -- Resourceful Reachability as HORN-LA -- A Seligman-Style Tableau System -- Comparison of LTL to Deterministic Rabin Automata Translators -- Tree Interpolation in Vampire -- Polarizing Double-Negation Translations -- Revisiting the Equivalence of Shininess and Politeness -- Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gödel Logic -- Multi-objective Discounted Reward Verification in Graphs and MDPs -- Description Logics, Rules and Multi-context Systems -- Complexity Analysis in Presence of Control Operators and Higher-Order Functions -- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo -- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving -- Verifying Temporal Properties in Real Models -- A Graphical Language for Proof Strategies -- A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus -- Relaxing Synchronization Constraints in Behavioral Programs -- Characterizing Subset Spaces as Bi-topological Structures -- Proof-Pattern Recognition and Lemma Discovery in ACL2 -- Semantic A-translations and Super-Consistency Entail Classical Cut Elimination -- Blocked Clause Decomposition -- Maximal Falsifiability: Definitions, Algorithms, and Applications -- Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning -- On QBF Proofs and Preprocessing -- Partial Backtracking in CDCL Solvers -- Lemma Mining over HOL Light -- On Module-Based Abstraction and Repair of Behavioral Programs -- Prediction and Explanation over DL-Lite Data Streams -- Forgetting Concept and Role Symbols in ALCH-Ontologies -- Simulating Parity Reasoning -- Herbrand Theorems for Substructural Logics -- On Promptness in Parity Games -- Defining Privacy Is Supposed to Be Easy -- Reachability Modules for the Description Logic SRIQ -- An Event Structure Model for Probabilistic Concurrent Kleene Algebra -- Three SCC-Based Emptiness Checks for Generalized Büchi Automata -- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification -- Incremental Tabling for Query-Driven Propagation of Logic Program Updates -- Tracking Data-Flow with Open Closure Types -- Putting Newton into Practice: A Solver for Polynomial Equations over Semirings -- System Description: E 1.8 -- Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light -- On Minimality and Integrity Constraints in Probabilistic Abduction -- POLAR: A Framework for Proof Refactoring. |
| Record Nr. | UNISA-996465503503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Logic for Programming, Artificial Intelligence, and Reasoning : 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013, Proceedings / / edited by Ken McMillan, Aart Middeldorp, Andrei Voronkov
| Logic for Programming, Artificial Intelligence, and Reasoning : 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013, Proceedings / / edited by Ken McMillan, Aart Middeldorp, Andrei Voronkov |
| Edizione | [1st ed. 2013.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 |
| Descrizione fisica | 1 online resource (XIV, 794 p. 178 illus.) |
| Disciplina | 005.1 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Software engineering
Artificial intelligence Computer science Machine theory Computer programming Compilers (Computer programs) Software Engineering Artificial Intelligence Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Programming Techniques Compilers and Interpreters |
| ISBN | 3-642-45221-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics -- May-Happen-in-Parallel Analysis for Priority-Based Scheduling -- The Complexity of Clausal Fragments of LTL -- A Semantic Basis for Proof Queries and Transformations -- Expressive Path Queries on Graphs with Data -- Proving Infinite Satisfiability -- SAT-Based Preprocessing for MaxSAT -- Dynamic and Static Symmetry Breaking in Answer Set Programming -- HOL Based First-Order Modal Logic Provers -- Resourceful Reachability as HORN-LA -- A Seligman-Style Tableau System -- Comparison of LTL to Deterministic Rabin Automata Translators -- Tree Interpolation in Vampire -- Polarizing Double-Negation Translations -- Revisiting the Equivalence of Shininess and Politeness -- Towards Rational Closure for Fuzzy Logic: The Case of Propositional Gödel Logic -- Multi-objective Discounted Reward Verification in Graphs and MDPs -- Description Logics, Rules and Multi-context Systems -- Complexity Analysis in Presence of Control Operators and Higher-Order Functions -- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo -- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving -- Verifying Temporal Properties in Real Models -- A Graphical Language for Proof Strategies -- A Proof of Strong Normalisation of the Typed Atomic Lambda-Calculus -- Relaxing Synchronization Constraints in Behavioral Programs -- Characterizing Subset Spaces as Bi-topological Structures -- Proof-Pattern Recognition and Lemma Discovery in ACL2 -- Semantic A-translations and Super-Consistency Entail Classical Cut Elimination -- Blocked Clause Decomposition -- Maximal Falsifiability: Definitions, Algorithms, and Applications -- Solving Geometry Problems Using a Combination of Symbolic and Numerical Reasoning -- On QBF Proofs and Preprocessing -- Partial Backtracking in CDCL Solvers -- Lemma Mining over HOL Light -- On Module-Based Abstraction and Repair of Behavioral Programs -- Prediction and Explanation over DL-Lite Data Streams -- Forgetting Concept and Role Symbols in ALCH-Ontologies -- Simulating Parity Reasoning -- Herbrand Theorems for Substructural Logics -- On Promptness in Parity Games -- Defining Privacy Is Supposed to Be Easy -- Reachability Modules for the Description Logic SRIQ -- An Event Structure Model for Probabilistic Concurrent Kleene Algebra -- Three SCC-Based Emptiness Checks for Generalized Büchi Automata -- PeRIPLO: A Framework for Producing Effective Interpolants in SAT-Based Software Verification -- Incremental Tabling for Query-Driven Propagation of Logic Program Updates -- Tracking Data-Flow with Open Closure Types -- Putting Newton into Practice: A Solver for Polynomial Equations over Semirings -- System Description: E 1.8 -- Formalization of Laplace Transform Using the Multivariable Calculus Theory of HOL-Light -- On Minimality and Integrity Constraints in Probabilistic Abduction -- POLAR: A Framework for Proof Refactoring. |
| Record Nr. | UNINA-9910484332703321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2013 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Processes, Terms and Cycles: Steps on the Road to Infinity [[electronic resource] ] : Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday / / edited by Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, Roel de Vrijer
| Processes, Terms and Cycles: Steps on the Road to Infinity [[electronic resource] ] : Essays Dedicated to Jan Willem Klop on the Occasion of his 60th Birthday / / edited by Aart Middeldorp, Vincent van Oostrom, Femke van Raamsdonk, Roel de Vrijer |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (XVIII, 642 p.) |
| Disciplina | 005.131 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Machine theory
Computer science Artificial intelligence Mathematical logic Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Artificial Intelligence Mathematical Logic and Foundations |
| ISBN | 3-540-32425-9 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | The Spectra of Words -- On the Undecidability of Coherent Logic -- Löb’s Logic Meets the ?-Calculus -- A Characterisation of Weak Bisimulation Congruence -- Böhm’s Theorem, Church’s Delta, Numeral Systems, and Ershov Morphisms -- Explaining Constraint Programming -- Sharing in the Weak Lambda-Calculus -- Term Rewriting Meets Aspect-Oriented Programming -- Observing Reductions in Nominal Calculi Via a Graphical Encoding of Processes -- Primitive Rewriting -- Infinitary Rewriting: From Syntax to Semantics -- Reducing Right-Hand Sides for Termination -- Reduction Strategies for Left-Linear Term Rewriting Systems -- Higher-Order Rewriting: Framework, Confluence and Termination -- Timing the Untimed: Terminating Successfully While Being Conservative -- Confluence of Graph Transformation Revisited -- Compositional Reasoning for Probabilistic Finite-State Behaviors -- Finite Equational Bases in Process Algebra: Results and Open Questions -- Skew and ?-Skew Confluence and Abstract Böhm Semantics -- A Mobility Calculus with Local and Dependent Types -- Model Theory for Process Algebra -- Expression Reduction Systems and Extensions: An Overview -- Axiomatic Rewriting Theory I: A Diagrammatic Standardization Theorem. |
| Record Nr. | UNISA-996465541503316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Rewriting Techniques and Applications [[electronic resource] ] : 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001. Proceedings / / edited by Aart Middeldorp
| Rewriting Techniques and Applications [[electronic resource] ] : 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001. Proceedings / / edited by Aart Middeldorp |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XII, 368 p.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Programming languages (Electronic computers)
Mathematical logic Computer logic Artificial intelligence Computer science—Mathematics Programming Languages, Compilers, Interpreters Mathematical Logic and Formal Languages Logics and Meanings of Programs Artificial Intelligence Symbolic and Algebraic Manipulation |
| ISBN | 3-540-45127-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Computing and Proving -- Rewriting for Deduction and Verification -- Regular Papers -- Universal Interaction Systems with Only Two Agents -- General Recursion on Second Order Term Algebras -- Beta Reduction Constraints -- From Higher-Order to First-Order Rewriting -- Combining Pattern E-Unification Algorithms -- Matching Power -- Dependency Pairs for Equational Rewriting -- Termination Proofs by Context-Dependent Interpretations -- Uniform Normalisation beyond Orthogonality -- Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order -- Relating Accumulative and Non-accumulative Functional Programs -- Context Unification and Traversal Equations -- Weakly Regular Relations and Applications -- On the Parallel Complexity of Tree Automata -- Transfinite Rewriting Semantics for Term Rewriting Systems -- Goal-Directed E-Unification -- The Unification Problem for Confluent Right-Ground Term Rewriting Systems -- On Termination of Higher-Order Rewriting -- Matching with Free Function Symbols — A Simple Extension of Matching? -- Deriving Focused Calculi for Transitive Relations -- A Formalised First-Order Con uence Proof for the ?-Calculus Using One-Sorted Variable Names (Barendregt Was Right after all ... almost) -- A Normal Form for Church-Rosser Language Systems -- Confluence and Termination of Simply Typed Term Rewriting Systems -- Parallel Evaluation of Interaction Nets with MPINE -- Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5. |
| Record Nr. | UNISA-996466166903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Rewriting Techniques and Applications : 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001. Proceedings / / edited by Aart Middeldorp
| Rewriting Techniques and Applications : 12th International Conference, RTA 2001, Utrecht, The Netherlands, May 22-24, 2001. Proceedings / / edited by Aart Middeldorp |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XII, 368 p.) |
| Disciplina | 005.131 |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Programming languages (Electronic computers)
Mathematical logic Computer logic Artificial intelligence Computer science—Mathematics Programming Languages, Compilers, Interpreters Mathematical Logic and Formal Languages Logics and Meanings of Programs Artificial Intelligence Symbolic and Algebraic Manipulation |
| ISBN | 3-540-45127-7 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Talks -- Computing and Proving -- Rewriting for Deduction and Verification -- Regular Papers -- Universal Interaction Systems with Only Two Agents -- General Recursion on Second Order Term Algebras -- Beta Reduction Constraints -- From Higher-Order to First-Order Rewriting -- Combining Pattern E-Unification Algorithms -- Matching Power -- Dependency Pairs for Equational Rewriting -- Termination Proofs by Context-Dependent Interpretations -- Uniform Normalisation beyond Orthogonality -- Verifying Orientability of Rewrite Rules Using the Knuth-Bendix Order -- Relating Accumulative and Non-accumulative Functional Programs -- Context Unification and Traversal Equations -- Weakly Regular Relations and Applications -- On the Parallel Complexity of Tree Automata -- Transfinite Rewriting Semantics for Term Rewriting Systems -- Goal-Directed E-Unification -- The Unification Problem for Confluent Right-Ground Term Rewriting Systems -- On Termination of Higher-Order Rewriting -- Matching with Free Function Symbols — A Simple Extension of Matching? -- Deriving Focused Calculi for Transitive Relations -- A Formalised First-Order Con uence Proof for the ?-Calculus Using One-Sorted Variable Names (Barendregt Was Right after all ... almost) -- A Normal Form for Church-Rosser Language Systems -- Confluence and Termination of Simply Typed Term Rewriting Systems -- Parallel Evaluation of Interaction Nets with MPINE -- Stratego: A Language for Program Transformation Based on Rewriting Strategies System Description of Stratego 0.5. |
| Record Nr. | UNINA-9910143604603321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||