| |
|
|
|
|
|
|
|
|
1. |
Record Nr. |
UNISA996466348903316 |
|
|
Titolo |
Logic for Programming, Artificial Intelligence, and Reasoning [[electronic resource] ] : 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008, Proceedings / / edited by Iliano Cervesato, Helmut Veith, Andrei Voronkov |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2008 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2008.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XIV, 714 p.) |
|
|
|
|
|
|
Collana |
|
Lecture Notes in Artificial Intelligence ; ; 5330 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Artificial intelligence |
Software engineering |
Computer programming |
Computer logic |
Mathematical logic |
Artificial Intelligence |
Software Engineering/Programming and Operating Systems |
Programming Techniques |
Software Engineering |
Logics and Meanings of Programs |
Mathematical Logic and Formal Languages |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
International conference proceedings. |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and index. |
|
|
|
|
|
|
Nota di contenuto |
|
Session 1. Constraint Solving -- Symmetry Breaking for Maximum Satisfiability -- Efficient Generation of Unsatisfiability Proofs and Cores in SAT -- Justification-Based Local Search with Adaptive Noise Strategies -- The Max-Atom Problem and Its Relevance -- Session 2. Knowledge Representation 1 -- Towards Practical Feasibility of Core Computation in Data Exchange -- Data-Oblivious Stream Productivity -- Reasoning about XML with Temporal Logics and Automata -- Distributed Consistency-Based Diagnosis -- Session 3. Proof-Theory 1 -- From One Session to Many: Dynamic Tags for Security Protocols -- A Conditional Logical Framework -- Nominal Renaming Sets -- Imogen: |
|
|
|
|
|
|
|
|
|
|
|
Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic -- Invited Talk -- Model Checking – My 27-Year Quest to Overcome the State Explosion Problem -- Session 4. Automata -- On the Relative Succinctness of Nondeterministic Büchi and co-Büchi Word Automata -- Recurrent Reachability Analysis in Regular Model Checking -- Alternation Elimination by Complementation (Extended Abstract) -- Discounted Properties of Probabilistic Pushdown Automata -- Session 5. Linear Arithmetic -- A Quantifier Elimination Algorithm for Linear Real Arithmetic -- (LIA) - Model Evolution with Linear Integer Arithmetic Constraints -- A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic -- Encoding Queues in Satisfiability Modulo Theories Based Bounded Model Checking -- Session 6. Verification -- On Bounded Reachability of Programs with Set Comprehensions -- Program Complexity in Hierarchical Module Checking -- Valigator: A Verification Tool with Bound and Invariant Generation -- Reveal: A Formal Verification Tool for Verilog Designs -- Invited Talks -- A Formal Language for Cryptographic Pseudocode -- Reasoning Using Knots -- Session 7. Knowledge Representation 2 -- Role Conjunctions in Expressive Description Logics -- Default Logics with Preference Order: Principles and Characterisations -- On Computing Constraint Abduction Answers -- Fast Counting with Bounded Treewidth -- Session 8. Proof-Theory 2 -- Cut Elimination for First Order Gödel Logic by Hyperclause Resolution -- Focusing Strategies in the Sequent Calculus of Synthetic Connectives -- An Algorithmic Interpretation of a Deep Inference System -- Weak ??-Normalization and Normalization by Evaluation for System F -- Session 9. Quantified Constraints -- Variable Dependencies of Quantified CSPs -- Treewidth: A Useful Marker of Empirical Hardness in Quantified Boolean Logic Encodings -- Tractable Quantified Constraint Satisfaction Problems over Positive Temporal Templates -- A Logic of Singly Indexed Arrays -- Session 10. Modal and Temporal Logics -- On the Computational Complexity of Spatial Logics with Connectedness Constraints -- Decidable and Undecidable Fragments of Halpern and Shoham’s Interval Temporal Logic: Towards a Complete Classification -- The Variable Hierarchy for the Lattice ?-Calculus -- A Formalised Lower Bound on Undirected Graph Reachability -- Session 11. Rewriting -- Improving Context-Sensitive Dependency Pairs -- Complexity, Graphs, and the Dependency Pair Method -- Uncurrying for Termination -- Approximating Term Rewriting Systems: A Horn Clause Specification and Its Implementation -- A Higher-Order Iterative Path Ordering -- Variable Dependencies of Quantified CSPs. |
|
|
|
|
|
|
Sommario/riassunto |
|
This book constitutes the refereed proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2008, which took place in Doha, Qatar, during November 22-27, 2008. The 45 revised full papers presented together with 3 invited talks were carefully revised and selected from 153 submissions. The papers address all current issues in automated reasoning, computational logic, programming languages and their applications and are organized in topical sections on automata, linear arithmetic, verification knowledge representation, proof theory, quantified constraints, as well as modal and temporal logics. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
2. |
Record Nr. |
UNISA996465281103316 |
|
|
Titolo |
Combinatorial Optimization [[electronic resource] ] : Second International Symposium, ISCO 2012, Athens, Greece, 19-21, Revised Selected Papers / / edited by A. Ridha Mahjoub, Vangelis Markakis, Ioannis Milis, Vangelis Th. Paschos |
|
|
|
|
|
|
|
Pubbl/distr/stampa |
|
|
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
|
|
|
|
|
|
|
|
|
ISBN |
|
|
|
|
|
|
Edizione |
[1st ed. 2012.] |
|
|
|
|
|
Descrizione fisica |
|
1 online resource (XIV, 476 p. 63 illus.) |
|
|
|
|
|
|
Collana |
|
Theoretical Computer Science and General Issues, , 2512-2029 ; ; 7422 |
|
|
|
|
|
|
Disciplina |
|
|
|
|
|
|
Soggetti |
|
Algorithms |
Computer science—Mathematics |
Discrete mathematics |
Numerical analysis |
Computer networks |
Discrete Mathematics in Computer Science |
Numerical Analysis |
Computer Communication Networks |
|
|
|
|
|
|
|
|
Lingua di pubblicazione |
|
|
|
|
|
|
Formato |
Materiale a stampa |
|
|
|
|
|
Livello bibliografico |
Monografia |
|
|
|
|
|
Note generali |
|
Bibliographic Level Mode of Issuance: Monograph |
|
|
|
|
|
|
Nota di bibliografia |
|
Includes bibliographical references and author index. |
|
|
|
|
|
|
Nota di contenuto |
|
Structure Theorems for Optimum Hyperpaths in Directed Hypergraphs -- Branch-and-Price Guided -- The New Faces of Combinatorial Optimization -- Models and Algorithms for the Train Unit Assignment Problem -- The Minimum Stabbing Triangulation Problem: IP Models and Computational Evaluation -- Using Symmetry to Optimize over the Sherali-Adams Relaxation -- A Second-Order Cone Programming Approximation to Joint Chance-Constrained Linear Programs -- Semidefinite Relaxations for Mixed 0-1 Second-Order Cone Program -- The Non-Disjoint m-Ring-Star Problem : Polyhedral Results and SDH/SONET Network Design.-The Uncapacitated Asymmetric Traveling Salesman Problem with Multiple Stacks -- Polyhedral Analysis and Branch-and-Cut for the Structural Analysis Problem -- Extended Formulations, Nonnegative Factorizations, and Randomized |
|
|
|
|
|
|
|
|
|
|
|
Communication Protocols -- An Algebraic Approach to Symmetric Extended Formulations -- Dual Consistent Systems of Linear Inequalities and Cardinality Constrained Polytopes -- Minimum Ratio Cover of Matrix Columns by Extreme Rays of Its Induced Cone.-The Uncapacitated Asymmetric Traveling Salesman Problem with Multiple Stacks -- Polyhedral Analysis and Branch-and-Cut for the Structural Analysis Problem -- Extended Formulations, Nonnegative Factorizations, and Randomized Communication -- An Algebraic Approach to Symmetric Extended.-On the Hop Constrained Steiner Tree Problem with Multiple Root.-Structure Theorems for Optimum Hyperpaths in Directed Hypergraphs -- A Second-Order Cone Programming Approximation to Joint Chance-Constrained Linear Programs.-Extended Formulations, Nonnegative Factorizations, and Randomized Communication -- An Algebraic Approach to Symmetric Extended.-Gap Inequalities for the Max-Cut Problem: A Cutting-Plane Algorithm. |
|
|
|
|
|
|
Sommario/riassunto |
|
This book constitutes the thoroughly refereed post-conference proceedings of the Second International Symposium on Combinatorial Optimization, ISCO 2012, held in Athens, Greece, in April 2012. The 37 revised full papers presented together with 4 invited talks were carefully reviewed and selected from 94 regular and 30 short submissions. They present original research on all aspects of combinatorial optimization, ranging from mathematical foundations and theory of algorithms to computational studies and practical applications. |
|
|
|
|
|
|
|
| |