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-19 [[electronic resource] ] : 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings / / edited by Franz Baader
| Automated Deduction - CADE-19 [[electronic resource] ] : 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings / / edited by Franz Baader |
| Edizione | [1st ed. 2003.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
| Descrizione fisica | 1 online resource (XII, 512 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Programming languages (Electronic computers) Computer logic Mathematical logic Artificial Intelligence Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages |
| ISBN | 3-540-45085-8 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1: Invited Talk -- SAT-Based Counterexample Guided Abstraction Refinement in Model Checking -- Session 2 -- Equational Abstractions -- Deciding Inductive Validity of Equations -- Automating the Dependency Pair Method -- An AC-Compatible Knuth-Bendix Order -- Session 3 -- The Complexity of Finite Model Reasoning in Description Logics -- Optimizing a BDD-Based Modal Solver -- A Translation of Looping Alternating Automata into Description Logics -- Session 4 -- Foundational Certified Code in a Metalogical Framework -- Proving Pointer Programs in Higher-Order Logic -- ? -- Subset Types and Partial Functions -- Session 5 -- Reasoning about Quantifiers by Matching in the E-graph -- Session 6 -- A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols -- Superposition Modulo a Shostak Theory -- Canonization for Disjoint Unions of Theories -- Matching in a Class of Combined Non-disjoint Theories -- Session 7 -- Reasoning about Iteration in Gödel’s Class Theory -- Algorithms for Ordinal Arithmetic -- Certifying Solutions to Permutation Group Problems -- Session 8: System Descriptions -- TRP++ 2.0: A Temporal Resolution Prover -- IsaPlanner: A Prototype Proof Planner in Isabelle -- ’Living Book’ :- ’Deduction’, ’Slicing’, ’Interaction’ -- The Homer System -- Session 9: CASC-19 Results -- The CADE-19 ATP System Competition -- Session 10: Invited Talk -- Proof Search and Proof Check for Equational and Inductive Theorems -- Session 11: System Descriptions -- The New WALDMEISTER Loop at Work -- About VeriFun -- How to Prove Inductive Theorems? QuodLibet! -- Session 12: Invited Talk -- Reasoning about Qualitative Representations of Space and Time -- Session 13 -- Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation -- The Model Evolution Calculus -- Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms -- Efficient Instance Retrieval with Standard and Relational Path Indexing -- Session 14 -- Monodic Temporal Resolution -- A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae -- Schematic Saturation for Decision and Unification Problems -- Session 15 -- Unification Modulo ACUI Plus Homomorphisms/Distributivity -- Source-Tracking Unification -- Optimizing Higher-Order Pattern Unification -- Decidability of Arity-Bounded Higher-Order Matching. |
| Record Nr. | UNISA-996465693603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Automated Deduction - CADE-19 : 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings / / edited by Franz Baader
| Automated Deduction - CADE-19 : 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28 - August 2, 2003, Proceedings / / edited by Franz Baader |
| Edizione | [1st ed. 2003.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
| Descrizione fisica | 1 online resource (XII, 512 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Programming languages (Electronic computers) Computer logic Mathematical logic Artificial Intelligence Programming Languages, Compilers, Interpreters Logics and Meanings of Programs Mathematical Logic and Formal Languages |
| ISBN | 3-540-45085-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Session 1: Invited Talk -- SAT-Based Counterexample Guided Abstraction Refinement in Model Checking -- Session 2 -- Equational Abstractions -- Deciding Inductive Validity of Equations -- Automating the Dependency Pair Method -- An AC-Compatible Knuth-Bendix Order -- Session 3 -- The Complexity of Finite Model Reasoning in Description Logics -- Optimizing a BDD-Based Modal Solver -- A Translation of Looping Alternating Automata into Description Logics -- Session 4 -- Foundational Certified Code in a Metalogical Framework -- Proving Pointer Programs in Higher-Order Logic -- ? -- Subset Types and Partial Functions -- Session 5 -- Reasoning about Quantifiers by Matching in the E-graph -- Session 6 -- A Randomized Satisfiability Procedure for Arithmetic and Uninterpreted Function Symbols -- Superposition Modulo a Shostak Theory -- Canonization for Disjoint Unions of Theories -- Matching in a Class of Combined Non-disjoint Theories -- Session 7 -- Reasoning about Iteration in Gödel’s Class Theory -- Algorithms for Ordinal Arithmetic -- Certifying Solutions to Permutation Group Problems -- Session 8: System Descriptions -- TRP++ 2.0: A Temporal Resolution Prover -- IsaPlanner: A Prototype Proof Planner in Isabelle -- ’Living Book’ :- ’Deduction’, ’Slicing’, ’Interaction’ -- The Homer System -- Session 9: CASC-19 Results -- The CADE-19 ATP System Competition -- Session 10: Invited Talk -- Proof Search and Proof Check for Equational and Inductive Theorems -- Session 11: System Descriptions -- The New WALDMEISTER Loop at Work -- About VeriFun -- How to Prove Inductive Theorems? QuodLibet! -- Session 12: Invited Talk -- Reasoning about Qualitative Representations of Space and Time -- Session 13 -- Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation -- The Model Evolution Calculus -- Translation of Resolution Proofs into Short First-Order Proofs without Choice Axioms -- Efficient Instance Retrieval with Standard and Relational Path Indexing -- Session 14 -- Monodic Temporal Resolution -- A Principle for Incorporating Axioms into the First-Order Translation of Modal Formulae -- Schematic Saturation for Decision and Unification Problems -- Session 15 -- Unification Modulo ACUI Plus Homomorphisms/Distributivity -- Source-Tracking Unification -- Optimizing Higher-Order Pattern Unification -- Decidability of Arity-Bounded Higher-Order Matching. |
| Record Nr. | UNINA-9910768470103321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The description logic handbook [[electronic resource] ] : theory, implementation, and applications / / edited by Franz Baader ... [et al.]
| The description logic handbook [[electronic resource] ] : theory, implementation, and applications / / edited by Franz Baader ... [et al.] |
| Pubbl/distr/stampa | Cambridge, UK ; ; New York, : Cambridge University Press, 2003 |
| Descrizione fisica | 1 online resource (575 p.) |
| Disciplina | 006.3/32 |
| Altri autori (Persone) | BaaderFranz |
| Soggetto topico | Description logics |
| Soggetto genere / forma | Electronic books. |
| ISBN |
1-107-12924-9
1-280-41799-4 9786610417995 1-139-13014-5 0-511-17880-8 1-139-14649-1 0-511-06694-5 0-511-06063-7 0-511-06907-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Cover; Half-title; Title; Copyright; Contents; Contributors; Preface; 1 An Introduction to Description Logics; Part I Theory; Part II Implementation; Part III Applications; Appendix Description Logic Terminology; Bibliography; Index |
| Record Nr. | UNINA-9910450526303321 |
| Cambridge, UK ; ; New York, : Cambridge University Press, 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The description logic handbook [[electronic resource] ] : theory, implementation, and applications / / edited by Franz Baader ... [et al.]
| The description logic handbook [[electronic resource] ] : theory, implementation, and applications / / edited by Franz Baader ... [et al.] |
| Pubbl/distr/stampa | Cambridge, UK ; ; New York, : Cambridge University Press, 2003 |
| Descrizione fisica | 1 online resource (575 p.) |
| Disciplina | 006.3/32 |
| Altri autori (Persone) | BaaderFranz |
| Soggetto topico | Description logics |
| ISBN |
1-107-12924-9
1-280-41799-4 9786610417995 1-139-13014-5 0-511-17880-8 1-139-14649-1 0-511-06694-5 0-511-06063-7 0-511-06907-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Cover; Half-title; Title; Copyright; Contents; Contributors; Preface; 1 An Introduction to Description Logics; Part I Theory; Part II Implementation; Part III Applications; Appendix Description Logic Terminology; Bibliography; Index |
| Record Nr. | UNINA-9910783143703321 |
| Cambridge, UK ; ; New York, : Cambridge University Press, 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
The description logic handbook : theory, implementation, and applications / / edited by Franz Baader ... [et al.]
| The description logic handbook : theory, implementation, and applications / / edited by Franz Baader ... [et al.] |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Cambridge, UK ; ; New York, : Cambridge University Press, 2003 |
| Descrizione fisica | 1 online resource (575 p.) |
| Disciplina | 006.3/32 |
| Altri autori (Persone) | BaaderFranz |
| Soggetto topico | Description logics |
| ISBN |
1-107-12924-9
1-280-41799-4 9786610417995 1-139-13014-5 0-511-17880-8 1-139-14649-1 0-511-06694-5 0-511-06063-7 0-511-06907-3 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Cover; Half-title; Title; Copyright; Contents; Contributors; Preface; 1 An Introduction to Description Logics; Part I Theory; Part II Implementation; Part III Applications; Appendix Description Logic Terminology; Bibliography; Index |
| Record Nr. | UNINA-9910827386403321 |
| Cambridge, UK ; ; New York, : Cambridge University Press, 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
KI 2001: Advances in Artificial Intelligence [[electronic resource] ] : Joint German/Austrian Conference on AI, Vienna, Austria, September 19-21, 2001. Proceedings / / edited by Franz Baader, Gerhard Brewka, Thomas Eiter
| KI 2001: Advances in Artificial Intelligence [[electronic resource] ] : Joint German/Austrian Conference on AI, Vienna, Austria, September 19-21, 2001. Proceedings / / edited by Franz Baader, Gerhard Brewka, Thomas Eiter |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XIV, 474 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Artificial Intelligence |
| ISBN | 3-540-45422-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Computational Game Theory and AI -- Optimal Agent Section -- Selected Papers -- Towards First-Order Temporal Resolution -- Approximating Most Specific Concepts in Description Logics with Existential Restrictions -- Bayesian Learning and Evolutionary Parameter Optimization -- Papers on Foundations -- Abductive Partial Order Planning with Dependent Fluents -- Constraint-Based Optimization of Priority Schemes for Decoupled Path Planning Techniques -- Possible Worlds Semantics for Credulous and Contraction Inference -- The Point Algebra for Branching Time Revisited -- Exploiting Conditional Equivalences in Connection Calculi -- Propositional Satisfiability in Answer-Set Programming -- Prediction of Regular Search Tree Growth by Spectral Analysis -- Theory and Practice of Time-Space Trade-Offs in Memory Limited Search -- Hierarchical Diagnosis of Large Configurator Knowledge Bases -- Towards Distributed Configuration -- Belief Update in the pGOLOG Framework -- Finding Optimal Solutions to Atomix -- History-Based Diagnosis Templates in the Framework of the Situation Calculus -- A Defense Model for Games with Incomplete Information -- Towards Inferring Labelling Heuristics for CSP Application Domains -- Addressing the Qualification Problem in FLUX -- Extracting Situation Facts from Activation Value Histories in Behavior-Based Robots -- Learning Search Control Knowledge for Equational Theorem Proving -- Intelligent Structuring and Reducing of Association Rules with Formal Concept Analysis -- Comparing Two Models for Software Debugging -- Inferring Implicit State Knowledge and Plans with Sensing Actions -- Papers on Applications -- Multi-agent Systems as Intelligent Virtual Environments -- OilEd: A Reason-able Ontology Editor for the Semantic Web -- Experiments with an Agent-Oriented Reasoning System -- Learning to Execute Navigation Plans -- DiKe - A Model-Based Diagnosis Kernel and Its Application -- Industrial Papers -- Constraints Applied to Configurations -- From Theory to Practice: AI Planning for High Performance Elevator Control -- Semantic Networks in a Knowledge Management Portal -- Collaborative Supply Net Management. |
| Record Nr. | UNISA-996465796803316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
KI 2001: Advances in Artificial Intelligence : Joint German/Austrian Conference on AI, Vienna, Austria, September 19-21, 2001. Proceedings / / edited by Franz Baader, Gerhard Brewka, Thomas Eiter
| KI 2001: Advances in Artificial Intelligence : Joint German/Austrian Conference on AI, Vienna, Austria, September 19-21, 2001. Proceedings / / edited by Franz Baader, Gerhard Brewka, Thomas Eiter |
| Edizione | [1st ed. 2001.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
| Descrizione fisica | 1 online resource (XIV, 474 p.) |
| Disciplina | 006.3 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Artificial intelligence
Artificial Intelligence |
| ISBN | 3-540-45422-5 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Invited Contributions -- Computational Game Theory and AI -- Optimal Agent Section -- Selected Papers -- Towards First-Order Temporal Resolution -- Approximating Most Specific Concepts in Description Logics with Existential Restrictions -- Bayesian Learning and Evolutionary Parameter Optimization -- Papers on Foundations -- Abductive Partial Order Planning with Dependent Fluents -- Constraint-Based Optimization of Priority Schemes for Decoupled Path Planning Techniques -- Possible Worlds Semantics for Credulous and Contraction Inference -- The Point Algebra for Branching Time Revisited -- Exploiting Conditional Equivalences in Connection Calculi -- Propositional Satisfiability in Answer-Set Programming -- Prediction of Regular Search Tree Growth by Spectral Analysis -- Theory and Practice of Time-Space Trade-Offs in Memory Limited Search -- Hierarchical Diagnosis of Large Configurator Knowledge Bases -- Towards Distributed Configuration -- Belief Update in the pGOLOG Framework -- Finding Optimal Solutions to Atomix -- History-Based Diagnosis Templates in the Framework of the Situation Calculus -- A Defense Model for Games with Incomplete Information -- Towards Inferring Labelling Heuristics for CSP Application Domains -- Addressing the Qualification Problem in FLUX -- Extracting Situation Facts from Activation Value Histories in Behavior-Based Robots -- Learning Search Control Knowledge for Equational Theorem Proving -- Intelligent Structuring and Reducing of Association Rules with Formal Concept Analysis -- Comparing Two Models for Software Debugging -- Inferring Implicit State Knowledge and Plans with Sensing Actions -- Papers on Applications -- Multi-agent Systems as Intelligent Virtual Environments -- OilEd: A Reason-able Ontology Editor for the Semantic Web -- Experiments with an Agent-Oriented Reasoning System -- Learning to Execute Navigation Plans -- DiKe - A Model-Based Diagnosis Kernel and Its Application -- Industrial Papers -- Constraints Applied to Configurations -- From Theory to Practice: AI Planning for High Performance Elevator Control -- Semantic Networks in a Knowledge Management Portal -- Collaborative Supply Net Management. |
| Record Nr. | UNINA-9910143623503321 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Logic for Programming, Artificial Intelligence, and Reasoning [[electronic resource] ] : 11th International Workshop, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings / / edited by Franz Baader, Andrei Voronkov
| Logic for Programming, Artificial Intelligence, and Reasoning [[electronic resource] ] : 11th International Workshop, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings / / edited by Franz Baader, Andrei Voronkov |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
| Descrizione fisica | 1 online resource (XII, 560 p.) |
| Disciplina | 005.1/15 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Software engineering
Artificial intelligence Mathematical logic Computer logic Computer programming Software Engineering/Programming and Operating Systems Artificial Intelligence Mathematical Logic and Formal Languages Logics and Meanings of Programs Software Engineering Programming Techniques |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | CERES in Many-Valued Logics -- A Decomposition Rule for Decision Procedures by Resolution-Based Calculi -- Abstract DPLL and Abstract DPLL Modulo Theories -- Combining Lists with Non-stably Infinite Theories -- Abstract Model Generation for Preprocessing Clause Sets -- Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying -- Applications of General Exact Satisfiability in Propositional Logic Modelling -- BCiC: A System for Code Authentication and Verification -- Ordered Resolution with Selection for -- On a Semantic Subsumption Test -- Suitable Graphs for Answer Set Programming -- Weighted Answer Sets and Applications in Intelligence Analysis -- How to Fix It: Using Fixpoints in Different Contexts -- Reasoning About Systems with Transition Fairness -- Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games -- How the Location of * Influences Complexity in Kleene Algebra with Tests -- The Equational Theory of ??, 0, 1,?+?, ×, ?? Is Decidable, but Not Finitely Axiomatisable -- A Trichotomy in the Complexity of Propositional Circumscription -- Exploiting Fixable, Removable, and Implied Values in Constraint Satisfaction Problems -- Evaluating QBFs via Symbolic Skolemization -- The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs -- Automated Termination Analysis for Incompletely Defined Programs -- Automatic Certification of Heap Consumption -- A Formalization of Off-Line Guessing for Security Protocol Analysis -- Abstraction-Carrying Code -- A Verification Environment for Sequential Imperative Programs in Isabelle/HOL -- Can a Higher-Order and a First-Order Theorem Prover Cooperate? -- A Generic Framework for Interprocedural Analyses of Numerical Properties -- Second-Order Matching via Explicit Substitutions -- Knowledge-Based Synthesis of Distributed Systems Using Event Structures -- The Inverse Method for the Logic of Bunched Implications -- Cut-Elimination: Experiments with CERES -- Uniform Rules and Dialogue Games for Fuzzy Logics -- Nonmonotonic Description Logic Programs: Implementation and Experiments -- Implementing Efficient Resource Management for Linear Logic Programming -- Layered Clausal Resolution in the Multi-modal Logic of Beliefs and Goals. |
| Record Nr. | UNISA-996465968103316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Logic for programming, artificial intelligence, and reasoning : 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005 : proceedings / / Franz Baader, Andrei Voronkov (eds.)
| Logic for programming, artificial intelligence, and reasoning : 11th international conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005 : proceedings / / Franz Baader, Andrei Voronkov (eds.) |
| Edizione | [1st ed. 2005.] |
| Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2005 |
| Descrizione fisica | 1 online resource (XII, 560 p.) |
| Disciplina | 005.1/15 |
| Altri autori (Persone) |
BaaderFranz
VoronkovA <1959-> (Andrei) |
| Collana | Lecture notes in computer science,Lecture notes in artificial intelligence |
| Soggetto topico |
Logic programming
Automatic theorem proving Artificial intelligence |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | CERES in Many-Valued Logics -- A Decomposition Rule for Decision Procedures by Resolution-Based Calculi -- Abstract DPLL and Abstract DPLL Modulo Theories -- Combining Lists with Non-stably Infinite Theories -- Abstract Model Generation for Preprocessing Clause Sets -- Flat and One-Variable Clauses: Complexity of Verifying Cryptographic Protocols with Single Blind Copying -- Applications of General Exact Satisfiability in Propositional Logic Modelling -- BCiC: A System for Code Authentication and Verification -- Ordered Resolution with Selection for -- On a Semantic Subsumption Test -- Suitable Graphs for Answer Set Programming -- Weighted Answer Sets and Applications in Intelligence Analysis -- How to Fix It: Using Fixpoints in Different Contexts -- Reasoning About Systems with Transition Fairness -- Entanglement – A Measure for the Complexity of Directed Graphs with Applications to Logic and Games -- How the Location of * Influences Complexity in Kleene Algebra with Tests -- The Equational Theory of ??, 0, 1,?+?, ×, ?? Is Decidable, but Not Finitely Axiomatisable -- A Trichotomy in the Complexity of Propositional Circumscription -- Exploiting Fixable, Removable, and Implied Values in Constraint Satisfaction Problems -- Evaluating QBFs via Symbolic Skolemization -- The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs -- Automated Termination Analysis for Incompletely Defined Programs -- Automatic Certification of Heap Consumption -- A Formalization of Off-Line Guessing for Security Protocol Analysis -- Abstraction-Carrying Code -- A Verification Environment for Sequential Imperative Programs in Isabelle/HOL -- Can a Higher-Order and a First-Order Theorem Prover Cooperate? -- A Generic Framework for Interprocedural Analyses of Numerical Properties -- Second-Order Matching via Explicit Substitutions -- Knowledge-Based Synthesis of Distributed Systems Using Event Structures -- The Inverse Method for the Logic of Bunched Implications -- Cut-Elimination: Experiments with CERES -- Uniform Rules and Dialogue Games for Fuzzy Logics -- Nonmonotonic Description Logic Programs: Implementation and Experiments -- Implementing Efficient Resource Management for Linear Logic Programming -- Layered Clausal Resolution in the Multi-modal Logic of Beliefs and Goals. |
| Altri titoli varianti | LPAR 2004 |
| Record Nr. | UNINA-9910484247503321 |
| Berlin ; ; New York, : Springer, c2005 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Term Rewriting and Applications [[electronic resource] ] : 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings / / edited by Franz Baader
| Term Rewriting and Applications [[electronic resource] ] : 18th International Conference, RTA 2007, Paris, France, June 26-28, 2007, Proceedings / / edited by Franz Baader |
| Edizione | [1st ed. 2007.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
| Descrizione fisica | 1 online resource (XII, 422 p.) |
| Disciplina | 006.3 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Compilers (Computer programs)
Machine theory Computer science Artificial intelligence Computer science—Mathematics Compilers and Interpreters Formal Languages and Automata Theory Computer Science Logic and Foundations of Programming Artificial Intelligence Symbolic and Algebraic Manipulation |
| ISBN | 3-540-73449-X |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Formal Verification of an Optimizing Compiler -- Challenges in Satisfiability Modulo Theories -- On a Logical Foundation for Explicit Substitutions -- Intruders with Caps -- Tom: Piggybacking Rewriting on Java -- Rewriting Approximations for Fast Prototyping of Static Analyzers -- Determining Unify-Stable Presentations -- Confluence of Pattern-Based Calculi -- A Simple Proof That Super-Consistency Implies Cut Elimination -- Bottom-Up Rewriting Is Inverse Recognizability Preserving -- Adjunction for Garbage Collection with Application to Graph Rewriting -- Non Strict Confluent Rewrite Systems for Data-Structures with Pointers -- Symbolic Model Checking of Infinite-State Systems Using Narrowing -- Delayed Substitutions -- Innermost-Reachability and Innermost-Joinability Are Decidable for Shallow Term Rewrite Systems -- Termination of Rewriting with Right-Flat Rules -- Abstract Critical Pairs and Confluence of Arbitrary Binary Relations -- On the Completeness of Context-Sensitive Order-Sorted Specifications -- KOOL: An Application of Rewriting Logic to Language Prototyping and Analysis -- Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi -- Proving Termination of Rewrite Systems Using Bounds -- Sequence Unification Through Currying -- The Termination Competition -- Random Descent -- Correctness of Copy in Calculi with Letrec -- A Characterization of Medial as Rewriting Rule -- The Maximum Length of Mu-Reduction in Lambda Mu-Calculus -- On Linear Combinations of ?-Terms -- Satisfying KBO Constraints -- Termination by Quasi-periodic Interpretations. |
| Record Nr. | UNISA-996465337003316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
