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 [[electronic resource] ] : 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings / / edited by Bernhard Gramlich, Dale Miller, Ulrike Sattler
| Automated Reasoning [[electronic resource] ] : 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 26-29, 2012, Proceedings / / edited by Bernhard Gramlich, Dale Miller, Ulrike Sattler |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (XIV, 568 p. 90 illus.) |
| Disciplina | 511.3/6028563 |
| Collana | Lecture Notes in Artificial Intelligence |
| Soggetto topico |
Mathematical logic
Computer logic Artificial intelligence Software engineering Computer science—Mathematics Numerical analysis Mathematical Logic and Formal Languages Logics and Meanings of Programs Artificial Intelligence Software Engineering Mathematics of Computing Numeric Computing |
| Soggetto genere / forma | Conference papers and proceedings. |
| ISBN | 3-642-31365-5 |
| Formato | Materiale a stampa  |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Taking Satisfiability to the Next Level with Z3 ; (Abstract) / Nikolaj Bjørner -- Enlarging the Scope of Applicability of Successful Techniques for Automated Reasoning in Mathematics / Yuri Matiyasevich -- SAT and SMT Are Still Resolution: Questions and Challenges / Robert Nieuwenhuis -- Unification Modulo Synchronous Distributivity / Siva Anantharaman, Serdar Erbatur, Christopher Lynch, Paliath Narendran and Michael Rusinowitch -- SAT Encoding of Unification in ELHR+R+ w.r.t. Cycle-Restricted Ontologies / Franz Baader, Stefan Borgwardt and Barbara Morawska -- UEL: Unification Solver for the Description Logic EL -- System Description / Franz Baader, Julian Mendez and Barbara Morawska -- Effective Finite-Valued Semantics for Labelled Calculi / Matthias Baaz, Ori Lahav and Anna Zamansky -- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic / François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala and Assia Mahboubi, et al. -- How Fuzzy Is My Fuzzy Description Logic? / Stefan Borgwardt, Felix Distel and Rafael Peñaloza -- Truthful Monadic Abstractions / Taus Brock-Nannestad and Carsten Schürmann -- Satallax: An Automatic Higher-Order Prover / Chad E. Brown -- From Strong Amalgamability to Modularity of Quantifier-Free Interpolation / Roberto Bruttomesso, Silvio Ghilardi and Silvio Ranise -- SPARQL Query Containment under RDFS Entailment Regime / Melisachew Wudage Chekol, Jérôme Euzenat, Pierre Genevès and Nabil Layaïda.
Automated Verification of Recursive Programs with Pointers / Frank de Boer, Marcello Bonsangue and Jurriaan Rot -- Security Protocols, Constraint Systems, and Group Theories / Stéphanie Delaune, Steve Kremer and Daniel Pasaila -- Taming Past LTL and Flat Counter Systems / Stéphane Demri, Amit Kumar Dhar and Arnaud Sangnier -- A Calculus for Generating Ground Explanations / Mnacho Echenim and Nicolas Peltier -- EPR-Based Bounded Model Checking at Word Level / Moshe Emmer, Zurab Khasidashvili, Konstantin Korovin, Christoph Sticksel and Andrei Voronkov -- Proving Non-looping Non-termination Automatically / Fabian Emmes, Tim Enger and Jürgen Giesl -- Rewriting Induction + Linear Arithmetic = Decision Procedure / Stephan Falke and Deepak Kapur -- Combination of Disjoint Theories: Beyond Decidability / Pascal Fontaine, Stephan Merz and Christoph Weidenbach -- Automated Analysis of Regular Algebra / Simon Foster and Georg Struth -- [delta]-Complete Decision Procedures for Satisfiability over the Reals / Sicun Gao, Jeremy Avigad and Edmund M. Clarke -- BDD-Based Automated Reasoning for Propositional Bi-Intuitionistic Tense Logics / Rajeev Goré and Jimmy Thomson -- From Linear Temporal Logic Properties to Rewrite Propositions / Pierre-Cyrille Héam, Vincent Hugot and Olga Kouchnarenko -- Tableaux Modulo Theories Using Superdeduction: An Application to the Verification of B Proof Rules with the Zenon Automated Theorem Prover / Mélanie Jacquel, Karim Berkani, David Delahaye and Catherine Dubois. Solving Non-linear Arithmetic / Dejan Jovanović and Leonardo de Moura -- Inprocessing Rules / Matti Järvisalo, Marijn J.H. Heule and Armin Biere -- Logical Difference Computation with CEX2.5 / Boris Konev, Michel Ludwig and Frank Wolter -- Overview and Evaluation of Premise Selection Techniques for Large Theory Mathematics / Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban and Tom Heskes -- Branching Time? Pruning Time! / Markus Latte and Martin Lange -- New Algorithms for Unification Modulo One-Sided Distributivity and Its Variants / Andrew M. Marshall and Paliath Narendran -- Reachability Analysis of Program Variables / Đurica Nikolić and Fausto Spoto -- Playing Hybrid Games with KeYmaera / Jan-David Quesel and André Platzer -- The QMLTP Problem Library for First-Order Modal Logics / Thomas Raths and Jens Otten -- Correctness of Program Transformations as a Termination Problem / Conrad Rau, David Sabel and Manfred Schmidt-Schauss -- Fingerprint Indexing for Paramodulation and Rewriting / Stephan Schulz -- Optimization in SMT with LAA Q Cost Functions / Roberto Sebastiani and Silvia Tomasi -- Synthesis for Unbounded Bit-Vector Arithmetic / Andrej Spielmann and Viktor Kuncak -- Extended Caching, Backjumping and Merging for Expressive Description Logics / Andreas Steigmiller, Thorsten Liebig and Birte Glimm -- KBCV -- Knuth-Bendix Completion Visualizer / Thomas Sternagel and Harald Zankl -- A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance / Martin Suda and Christoph Weidenbach -- Stratification in Logics of Definitions / Alwen Tiu -- Diabelli: A Heterogeneous Proof System / Matej Urbas and Mateja Jamnik. |
| Record Nr. | UNISA-996465531903316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Certified Programs and Proofs [[electronic resource] ] : Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, Proceedings / / edited by Chris Hawblitzel, Dale Miller
| Certified Programs and Proofs [[electronic resource] ] : Second International Conference, CPP 2012, Kyoto, Japan, December 13-15, 2012, Proceedings / / edited by Chris Hawblitzel, Dale Miller |
| Edizione | [1st ed. 2012.] |
| Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 |
| Descrizione fisica | 1 online resource (X, 305 p. 64 illus.) |
| Disciplina | 004.01/51 |
| Collana | Theoretical Computer Science and General Issues |
| Soggetto topico |
Computer science
Machine theory Compilers (Computer programs) Computer science—Mathematics Software engineering Artificial intelligence Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Compilers and Interpreters Symbolic and Algebraic Manipulation Software Engineering Artificial Intelligence |
| ISBN | 3-642-35308-8 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto | Scalable Formal Machine Models -- Mechanized Semantics for Compiler Verification -- Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs -- Program Certification by Higher-Order Model Checking -- A Formally-Verified Alias Analysis -- Mechanized Verification of Computing Dominators for Formalizing Compilers -- On the Correctness of an Optimising Assembler for the Intel MCS-51 Microprocessor -- An Executable Semantics for CompCert C -- Producing Certified Functional Code from Inductive Specifications -- The New Quickcheck for Isabelle: Random, Exhaustive and Symbolic Testing under One Roof -- Proving Concurrent Noninterference -- Noninterference for Operating System Kernels -- Compositional Verification of a Baby Virtual Memory Manager -- Shall We Juggle, Coinductively? -- Proof Pearl: Abella Formalization of λ-Calculus Cube Property -- A String of Pearls: Proofs of Fermat’s Little Theorem -- Compact Proof Certificates for Linear Logic -- Constructive Completeness for Modal Logic with Transitive Closure -- Rating Disambiguation Errors -- A Formal Proof of Square Root and Division Elimination in Embedded Programs -- Coherent and Strongly Discrete Rings in Type Theory -- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. |
| Record Nr. | UNISA-996466275603316 |
| Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2012 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Functional and Logic Programming : 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15-17, 2024, Proceedings
| Functional and Logic Programming : 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15-17, 2024, Proceedings |
| Autore | Gibbons Jeremy |
| Edizione | [1st ed.] |
| Pubbl/distr/stampa | Singapore : , : Springer Singapore Pte. Limited, , 2024 |
| Descrizione fisica | 1 online resource (336 pages) |
| Altri autori (Persone) | MillerDale |
| Collana | Lecture Notes in Computer Science Series |
| ISBN | 981-9723-00-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Record Nr. | UNISA-996601562703316 |
Gibbons Jeremy
|
||
| Singapore : , : Springer Singapore Pte. Limited, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. di Salerno | ||
| ||
Functional and Logic Programming : 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15–17, 2024, Proceedings / / edited by Jeremy Gibbons, Dale Miller
| Functional and Logic Programming : 17th International Symposium, FLOPS 2024, Kumamoto, Japan, May 15–17, 2024, Proceedings / / edited by Jeremy Gibbons, Dale Miller |
| Autore | Gibbons Jeremy |
| Edizione | [1st ed. 2024.] |
| Pubbl/distr/stampa | Singapore : , : Springer Nature Singapore : , : Imprint : Springer, , 2024 |
| Descrizione fisica | 1 online resource (336 pages) |
| Disciplina | 005.1 |
| Altri autori (Persone) | MillerDale |
| Collana | Lecture Notes in Computer Science |
| Soggetto topico |
Software engineering
Artificial intelligence Programming languages (Electronic computers) Computer programming Computer science Computer systems Software Engineering Artificial Intelligence Programming Language Programming Techniques Computer Science Logic and Foundations of Programming Computer System Implementation |
| ISBN | 981-9723-00-0 |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Nota di contenuto |
Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Verse: A New Functional Logic Language -- Continuations from Three Angles -- Verification of Refactoring in Answer Set Programming -- Contents -- Extended Abstract -- Algebraic Connection Between Logic Programming and Machine Learning (Extended Abstract) -- 1 Introduction -- 2 Linear Algebraic Approaches to Logic Programming -- 3 Differentiable Approaches to Logic Programming -- References -- Rewriting -- ACGtk: A Toolkit for Developing and Running Abstract Categorial Grammars -- 1 Introduction -- 2 Abstract Categorial Grammars -- 3 Properties -- 3.1 Expressive Power -- 3.2 ACG Composition -- 3.3 Parsing with Abstract Categorial Grammars and Datalog Reduction -- 4 ACGtk -- 5 Notable Implementation Features -- 5.1 Datalog Evaluation, Tabular Parsing and Shared Forest -- 5.2 Magic Set Rewriting -- 6 Related Work -- 7 Conclusion -- A Typing Rules -- References -- Term Evaluation Systems with Refinements: First-Order, Second-Order, and Contextual Improvement -- 1 Introduction -- 1.1 Examples of TES and TERS -- 2 Preliminaries -- 3 First-Order Term Evaluation and Refinement Systems -- 4 Critical Pair Analysis for Local Coherence -- 5 Second-Order Term Evaluation and Refinement Systems -- 6 Second-Order Critical Pair Analysis for Local Coherence -- 7 Related Work -- 8 Conclusion and Future Work -- A Omitted Proofs -- A.1 Proofs for Sect. 3 and Sect. 4 -- A.2 The TERS Nats -- A.3 On Linearity Conditions -- A.4 Proofs for Sect. 5 and Sect. 6 -- A.5 The TERS CBV"115 and Hndl -- B Critical Pair Analysis of Hndl by Our Prototype Analyzer -- B.1 Definition of TERS Hndl -- B.2 Local Coherence Check -- References -- A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting -- 1 Introduction -- 2 The DP Framework.
3 Probabilistic Annotated Dependency Pairs -- 4 The ADP Framework -- 5 Transforming ADPs -- 6 Conclusion and Evaluation -- References -- Algebra -- Tabulation with Zippers -- 1 Introduction -- 2 Zipper Tabulation of Functions on Trees -- 2.1 Efficient Zipper-Based Attribute Grammars -- 3 Zip with Zipper -- 3.1 zipWithZipper -- 3.2 Tying the Knot -- 3.3 A Generic Zipper Instance of zipWithZipper -- 3.4 A Generic Table -- 4 The Expression Language Revisited -- 5 Performance -- 6 Related Work -- 7 Conclusions -- References -- Declarative Pearl: Rigged Contracts -- 1 Introduction -- 2 The Contract Library -- 2.1 Acquisition Date and Expiry Date -- 2.2 Discount Bonds -- 2.3 Composing Contracts -- 3 Instant Semiring, Just Add Expired -- 3.1 Definition of a Semiring -- 3.2 The Contract Semiring -- 3.3 Beyond Semirings: Groups -- 4 Denotational Semantics: Expiry Date and Worth -- 4.1 A Contract's Expiry Date -- 4.2 The Bottom Line -- 4.3 Comparison with the Original -- 4.4 Executable Semantics -- 5 Conclusion -- References -- Applications -- System Description: DeepLLM, Casting Dialog Threads into Logic Programs -- 1 Introduction -- 2 System Architecture -- 3 Interactors -- 4 Recursors -- 4.1 Synthesizing the Logic Program on Recursive Descent -- 4.2 The Unfolder -- 4.3 The AndOrExplorer -- 4.4 The SVO Relation Extractor -- 4.5 The Logic Programming Connection -- 5 Refiners -- 5.1 The Embeddings Vector Store -- 5.2 Filtering with Semantic Distance to Ground-Truth Facts -- 5.3 Refining Decisions with LLM-Based Oracles -- 5.4 Toward Trustable Generative AI -- 6 The Model Builder: A Propositional Horn Clause Satisfiability Solver -- 7 Applications -- 8 Discussion on Limitations and Variations on the Theme -- 8.1 Limitations -- 8.2 Future Work Directions -- 9 Related Work -- 10 Conclusion -- References. A Constraint-Based Mathematical Modeling Library in Prolog with Answer Constraint Semantics -- 1 Introduction -- 2 Motivating Example -- 2.1 List Recursion Versus Array Iteration in the N-Queens Problem -- 2.2 Breaking Symmetries in the N-Queens Problem -- 2.3 Performance Figures -- 3 Comparison to MiniZinc Modeling Language -- 3.1 Types -- 3.2 Programming Search -- 3.3 Answer Constraint Semantics in Fourier's Example -- 3.4 Model Debuging and Visualization in a Unique IDE -- 4 Modeling Library -- 4.1 Subscripted Variables with Library arrays.pl -- 4.2 Bounded Quantification Meta-predicates in quantifiers.pl -- 4.3 Interface to Constraint Solvers with Library clp.pl -- 4.4 Proposal for a Second-Level of Normalization of ISO-Prolog -- 5 Conclusion -- References -- Grants4Companies: Applying Declarative Methods for Recommending and Reasoning About Business Grants in the Austrian Public Administration (System Description) -- 1 Introduction -- 2 Development History -- 3 Grants4Companies Overview -- 4 Representation and Evaluation of the Grant Conditions -- 4.1 Representation of the Grants -- 4.2 Evaluation of the Grants -- 5 PoC: Extensions and Interfaces -- 5.1 Symbolic Reasoning over Grants -- 5.2 Interface Between Lisp and Prolog -- 6 Conclusion and Outlook -- References -- Program Analysis -- Inferring Non-failure Conditions for Declarative Programs -- 1 Introduction -- 2 Functional Logic Programming and Curry -- 3 Call Types and Abstract Types -- 4 In/Out Types -- 5 Inference and Checking of Call Types -- 5.1 Initial Call Types -- 5.2 Call Type Checking -- 5.3 Iterated Call Type Checking -- 5.4 Extensions -- 6 Evaluation -- 7 Related Work -- 8 Conclusions -- References -- Being Lazy When It Counts -- 1 Introduction -- 2 Presentation of Constant-Time Reference Counting -- 2.1 Eager and Lazy Reference Counting -- 2.2 Allocation Size. 2.3 Implementation in Koka -- 2.4 Soundness and Garbage-Free Guarantee -- 2.5 Eagerly-Deallocating-Allocation Effect -- 3 Preliminary Experiments -- 3.1 Experimental Setup -- 3.2 Performance and Memory Usage -- 3.3 Latency Measurements -- 4 Related Work and Conclusion -- 4.1 Related Work -- 4.2 Conclusion -- A Formalization -- A.1 Syntax -- A.2 Reference Koka Semantics -- A.3 New CTRC Semantics -- A.4 Metatheory -- B CTRC Allocator Source Code -- References -- Metaprogramming -- MetaOCaml: Ten Years Later -- 1 Introduction -- 2 Introduction to Staging and MetaOCaml -- 3 Implementing MetaOCaml -- 3.1 Type-Checking Staged Programs -- 3.2 Optimized Translation of Brackets and Escapes -- 4 Let-Insertion -- 5 Cross-Stage Persistence -- 6 Related Work -- 7 Conclusions -- References -- An ML-Style Module System for Cross-Stage Type Abstraction in Multi-stage Programming -- 1 Introduction -- 1.1 Multi-stage Programming -- 1.2 Point at Issue: Modularity -- 2 Motivating Examples -- 3 Related Work and Our Approach -- 4 Source Language -- 5 Target Language and Its Type Safety -- 6 Elaboration and Its Soundness -- 7 Extension with Cross-Stage Persistence -- 8 Future Work and Provisional Implementation -- 9 Conclusion -- A An Example Elaboration Involving CSP -- B Complete Definitions -- C Proofs for Target Type Safety -- D Proofs for Soundness of Elaboration -- References -- Rhyme: A Data-Centric Multi-paradigm Query Language Based on Functional Logic Metaprogramming -- 1 Introduction -- 2 Rhyme Front End -- 2.1 JSON API -- 2.2 Pipe API -- 2.3 Visualization API -- 3 Rhyme Backend -- 3.1 AST -- 3.2 Structure of the Rhyme IR -- 3.3 Code Generation -- 4 Related Work -- 5 Conclusion -- References -- Proofs -- Language-parameterized Proofs for Functional Languages with Subtyping -- 1 Introduction -- 2 Operational Semantics and Lang-n-Prove (Review). 3 Declarative Subtyping with Lang-n-Prove -- 3.1 Inversion Subtyping Lemmas -- 3.2 Canonical Form Lemmas -- 3.3 Progress Theorem -- 3.4 Inversion Typing Lemmas -- 3.5 Type Preservation Theorem -- 4 Algorithmic Subtyping -- 4.1 Subtyping and Typing Soundness -- 4.2 Subtyping Completeness -- 4.3 Typing Completeness -- 5 Evaluation and Limitations of Our Work -- 6 Related Work -- 7 Conclusion -- A Examples of Inversion Typing Lemmas -- B Examples of Generated Proofs -- C Inversion Typing Lemmas for Errors -- D Examples of Algorithmic Typing Rules -- References -- System Description: A Theorem-Prover for Subregular Systems: The Language Toolkit and Its Interpreter, Plebby -- 1 Introduction -- 2 Generalized Regular Expressions -- 2.1 Factors and Symbol Sets -- 2.2 Booleans, Concatenation, and Iteration -- 2.3 Subsequences and Shuffle Ideals -- 2.4 Tiers and Neutral Letters -- 2.5 Brzozowski Derivatives and Quotients -- 2.6 Summary -- 3 Constraint Analysis -- 4 Algebra and Complexity Analysis -- 4.1 Some Varieties with Shortcuts -- 4.2 Some Other Well-Studied Classes -- 4.3 Summary -- 5 Conclusion -- References -- Author Index. |
| Record Nr. | UNINA-9910861096203321 |
|
Gibbons Jeremy
|
||
| Singapore : , : Springer Nature Singapore : , : Imprint : Springer, , 2024 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming
| Proceedings of the 5th ACM SIGPLAN International Conference on Principles and Practice of Declaritive Programming |
| Pubbl/distr/stampa | [Place of publication not identified], : ACM, 2003 |
| Descrizione fisica | 1 online resource (284 pages) |
| Disciplina | 005.13/1 |
| Collana | ACM Conferences |
| Soggetto topico |
Engineering & Applied Sciences
Computer Science |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti |
Proceedings of the 5th Association for Computing Machinery Special Interest Group on Programming Languages International Conference on Principles and Practice of Declaritive Programming
PPDP '03 5th International Conference on Principles and Practice of Declarative Programming 2003 (co-located with ICFP 2003), Uppsala, Sweden - August 27 - 29, 2003 |
| Record Nr. | UNINA-9910375846503321 |
| [Place of publication not identified], : ACM, 2003 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||
Proceedings of the joint meeting of the twenty-third EACSL annual Conference on Computer Science Logic (CSL) and the twenty-ninth annual ACM/IEEE Symposium on Logic in Computer Science (LICS
| Proceedings of the joint meeting of the twenty-third EACSL annual Conference on Computer Science Logic (CSL) and the twenty-ninth annual ACM/IEEE Symposium on Logic in Computer Science (LICS |
| Autore | Henzinger Thomas |
| Pubbl/distr/stampa | [Place of publication not identified], : ACM, 2014 |
| Descrizione fisica | 1 online resource (764 pages) |
| Collana | ACM Conferences |
| Soggetto topico |
Engineering & Applied Sciences
Computer Science |
| Formato | Materiale a stampa |
| Livello bibliografico | Monografia |
| Lingua di pubblicazione | eng |
| Altri titoli varianti |
Joint meeting of the twenty-third EACSL annual Conference on Computer Science Logic (CSL) and the twenty-ninth annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vienna, Austria - July 14-18, 2014
CSL-LICS '14 |
| Record Nr. | UNINA-9910376364803321 |
|
Henzinger Thomas
|
||
| [Place of publication not identified], : ACM, 2014 | ||
| Materiale a stampa | ||
| Lo trovi qui: Univ. Federico II | ||
| ||