المؤلفون: Henkel, Elisabeth, Hoenicke, Jochen, Schindler, Tanja

المصدر: urn:isbn:978-3-03-138498-1
Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings, 248–265 (2023); International Conference on Automated Deduction, Rome, Italy [IT], 01-07-2023 au 04-07-2023

مصطلحات موضوعية: Quantified Formulas, SMT, Tree Interpolation, Generic tree, Interpolants, Interpolation algorithms, Linear arithmetic, Literals, Quantified formula, Tree interpolation, Uninterpreted Functions, Theoretical Computer Science, Computer Science (all), Engineering, computing & technology, Computer science, Ingénierie, informatique & technologie, Sciences informatiques

Relation: https://link.springer.com/content/pdf/10.1007/978-3-031-38499-8_15

URL الوصول: https://orbi.uliege.be/handle/2268/314100

المؤلفون: Bromberger, Martin, Leutgeb, Lorenz, Weidenbach, Christoph

المساهمون: Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft, Max Planck Institute for Informatics Saarbrücken

المصدر: Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023 ; https://inria.hal.science/hal-04313817 ; Frontiers of Combining Systems - 14th International Symposium, FroCoS 2023, Sep 2023, Prague (CZ), Czech Republic. pp.137 - 155, ⟨10.1007/978-3-031-43369-6_8⟩

مصطلحات موضوعية: Bernays-Schönfinkel Fragment, Linear Arithmetic, Horn Clauses, Superposition, Model Construction, Bernays-Schönfinkel Fragment Linear Arithmetic Horn Clauses Superposition Model Construction, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: Prague (CZ), Czech Republic

الاتاحة: https://inria.hal.science/hal-04313817
https://inria.hal.science/hal-04313817v1/document
https://inria.hal.science/hal-04313817v1/file/978-3-031-43369-6_8.pdf
https://doi.org/10.1007/978-3-031-43369-6_8

المؤلفون: Henriksson, Mikael, 1996, Gustafsson, Oscar, 1973

المصدر: eLLIIT – The Linköping – Lund Initiative on IT and Mobile Communication Proceeding of the IEEE Nordic Circuits and Systems Conference (NorCAS).

مصطلحات موضوعية: streaming data processing, matrix transposition, linear arithmetic, interleaver, FPGA, distributed memories

وصف الملف: electronic

URL الوصول: https://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-199025
https://liu.diva-portal.org/smash/get/diva2:1810365/FULLTEXT02.pdf

المؤلفون: Korovin, Konstantin, Kovács, Laura, Reger, Giles, Schoisswohl, Johannes, Voronkov, Andrei

المصدر: Korovin , K , Kovács , L , Reger , G , Schoisswohl , J & Voronkov , A 2023 , ALASCA: Reasoning in Quantified Linear Arithmetic . in Proceedings of the 29th on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'23) . , Chapter 33 , Tools and Algorithms for the Construction and Analysis of Systems , vol. 13993 , Springer Cham , pp. 647-665 . https://doi.org/10.1007/978-3-031-30823-9_33

مصطلحات موضوعية: Automated Reasoning, Linear Arithmetic, SMT, quantifed First-Order Logic, Theorem Proving

Relation: https://research.manchester.ac.uk/en/publications/17270168-928e-4dad-bcb1-59bb73d44317; urn:ISBN:978-3-031-30822-2

الاتاحة: https://research.manchester.ac.uk/en/publications/17270168-928e-4dad-bcb1-59bb73d44317
https://doi.org/10.1007/978-3-031-30823-9_33

المؤلفون: Bromberger, Martin, Leutgeb, Lorenz, Weidenbach, Christoph

المساهمون: Max Planck Institute for Informatics Saarbrücken, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)

المصدر: IJCAR 2022 - International Joint Conference in Automated Reasoning ; https://inria.hal.science/hal-03881893 ; IJCAR 2022 - International Joint Conference in Automated Reasoning, Aug 2022, Haifa, Israel. pp.147-168, ⟨10.1007/978-3-031-10769-6_10⟩

مصطلحات موضوعية: Bernays-Schönfinkel Fragment, Linear Arithmetic, Redundancy Elimination, Subsumption, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC]

جغرافية الموضوع: Haifa, Israel

الاتاحة: https://inria.hal.science/hal-03881893
https://inria.hal.science/hal-03881893v1/document
https://inria.hal.science/hal-03881893v1/file/paper.pdf
https://doi.org/10.1007/978-3-031-10769-6_10

المؤلفون: Tian, Chao

المساهمون: Fan, Wenfei, Libkin, Leonid

مصطلحات موضوعية: 005.75, graph analysis, graph querying, graph data management, graph dependencies, NGDs, clean graphs, scalability, quality, subgraph isomorphism, linear arithmetic expressions

URL الوصول: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.743652

المؤلفون: Lechner, Antonia

المساهمون: Worrell, James

مصطلحات موضوعية: 006.3, Automata Theory, Linear Arithmetic, Computational Complexity Theory, reachability problems, Presburger arithmetic, p-adic numbers, one-counter automata

URL الوصول: https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.735876

المؤلفون: Haase, Christoph, Mansutti, Alessio

المساهمون: Christoph Haase and Alessio Mansutti

مصطلحات موضوعية: linear arithmetic, Büchi arithmetic, p-adic numbers, automatic structures

وصف الملف: application/pdf

Relation: Is Part Of LIPIcs, Volume 202, 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.55

الاتاحة: https://doi.org/10.4230/LIPIcs.MFCS.2021.55
https://nbn-resolving.org/urn:nbn:de:0030-drops-144953
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2021.55

المؤلفون: Boigelot, Bernard, Brusten, Julien, Leroux, Jérôme

المصدر: Lecture Notes in Computer Science, 5663, 469-484 (2009); 22nd International Conference on Automated Deduction, Montreal, Canada [CA], August 2009

مصطلحات موضوعية: automata, mixed integer and linear arithmetic, semenov's theorem, Engineering, computing & technology, Computer science, Ingénierie, informatique & technologie, Sciences informatiques

Relation: http://www.springerlink.com/content/27332vp4g32u9j76/; urn:issn:0302-9743; urn:issn:1611-3349

URL الوصول: https://orbi.uliege.be/handle/2268/33238

المؤلفون: Chistikov, Dmitry, Haase, Christoph

المساهمون: Dmitry Chistikov and Christoph Haase

مصطلحات موضوعية: logical definability, linear arithmetic theories, semi linear sets, ultimately periodic sets, numerical semigroups

وصف الملف: application/pdf

Relation: Is Part Of LIPIcs, Volume 168, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.119

الاتاحة: https://doi.org/10.4230/LIPIcs.ICALP.2020.119
https://nbn-resolving.org/urn:nbn:de:0030-drops-125265
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2020.119

المؤلفون: Dinagar, D. Stephen¹, Manvizhi, M.²

المصدر: International Journal of Fuzzy Mathematical Archive 14(2):199-212. 2017

المؤلفون: Bromberger, Martin, Fleury, Mathias, Schwarz, Simon, Weidenbach, Christoph

المساهمون: Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Pascal Fontaine

المصدر: CADE-27 - The 27th International Conference on Automated Deduction ; https://inria.hal.science/hal-02405524 ; CADE-27 - The 27th International Conference on Automated Deduction, Aug 2019, Natal, Brazil. pp.111-122, ⟨10.1007/978-3-030-29436-6_7⟩

مصطلحات موضوعية: Linear Arithmetic, Integer Arithmetic, SMT, Preprocessing, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: Natal, Brazil

الاتاحة: https://inria.hal.science/hal-02405524
https://inria.hal.science/hal-02405524v1/document
https://inria.hal.science/hal-02405524v1/file/cade27spass.pdf
https://doi.org/10.1007/978-3-030-29436-6_7

المؤلفون: Bromberger, Martin, Sturm, Thomas, Weidenbach, Christoph

المساهمون: Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Saarland University Saarbrücken

المصدر: ISSN: 0747-7171.

مصطلحات موضوعية: Linear arithmetic, SMT, SAT, CDCL, Linear programming, Integer arithmetic, [INFO]Computer Science [cs], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

Relation: hal-02397168; https://inria.hal.science/hal-02397168; https://inria.hal.science/hal-02397168/document; https://inria.hal.science/hal-02397168/file/authors_version.pdf

الاتاحة: https://inria.hal.science/hal-02397168
https://inria.hal.science/hal-02397168/document
https://inria.hal.science/hal-02397168/file/authors_version.pdf
https://doi.org/10.1016/j.jsc.2019.07.021

المؤلفون: Clemente, Lorenzo, Lasota, Slawomir

المساهمون: Lorenzo Clemente and Slawomir Lasota

مصطلحات موضوعية: timed automata, reachability relation, timed pushdown automata, linear arithmetic

وصف الملف: application/pdf

Relation: Is Part Of LIPIcs, Volume 107, 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018); https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.118

الاتاحة: https://doi.org/10.4230/LIPIcs.ICALP.2018.118
https://nbn-resolving.org/urn:nbn:de:0030-drops-91228
https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2018.118

المؤلفون: Vu, Tung Xuan

مصطلحات موضوعية: SMT solving, non-linear arithmetic, interval constraint propagation, subtropical satisfiability, complete efficient framework

وصف الملف: application/pdf

URL الوصول: https://ndlsearch.ndl.go.jp/books/R100000039-I11178491

Degree: 博士(情報科学) -- 北陸先端科学技術大学院大学

المؤلفون: Boulmé, Sylvain, Maréchal, Alexandre

المساهمون: VERIMAG (VERIMAG - IMAG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes 2016-2019 (UGA 2016-2019 ), ANR-11-INSE-0003,VERASCO,Vérification formelle d'analyseurs statiques et de compilateurs(2011), European Project: 306595,EC:FP7:ERC,ERC-2012-StG_20111012,STATOR(2013)

المصدر: ISSN: 0168-7433.

مصطلحات موضوعية: Continuation-Passing Style, Linear arithmetic, Refinement calculus, Abstract Interpretation, The Coq proof assistant, Monad, Weakest precondition, Certified Software, Proof Assistants, Result Certification, [INFO]Computer Science [cs]

Relation: info:eu-repo/grantAgreement/EC/FP7/306595/EU/STATic analysis with ORiginal methods/STATOR

الاتاحة: https://hal.science/hal-01133865
https://hal.science/hal-01133865v4/document
https://hal.science/hal-01133865v4/file/hal_main.pdf
https://doi.org/10.1007/s10817-018-9492-2

المؤلفون: Borralleras Andreu, Cristina, Larraz Hurtado, Daniel, Rodríguez Carbonell, Enric, Oliveras Llunell, Albert, Rubio Gimeno, Alberto

المساهمون: Universitat Politècnica de Catalunya. Departament de Ciències de la Computació, Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació

مصطلحات موضوعية: Àrees temàtiques de la UPC::Informàtica::Informàtica teòrica, Integer programming, Non-linear arithmetic, Satisfiability modulo theories, Programació en nombres enters

وصف الملف: application/pdf

Relation: info:eu-repo/grantAgreement/EC/H2020/648276/EU/A Unified Theory of Algorithmic Relaxations/AUTAR; info:eu-repo/grantAgreement/MINECO//TIN2015-69175-C4-3-R/ES/SOLUCIONES EFECTIVAS BASADAS EN LA LOGICA/; info:eu-repo/grantAgreement/AEI/Plan Estatal de Investigación Científica y Técnica y de Innovación 2017-2020/RTI2018-094403-B-C33/ES/RAZONAMIENTO FORMAL PARA TECNOLOGIAS FACILITADORAS Y EMERGENTES/; Borralleras, C. [et al.]. Incomplete SMT techniques for solving non-linear formulas over the integers. "ACM transactions on computational logic", 1 Agost 2019, vol. 20, núm. 4, article 25, p. 25:1-25:36.; http://hdl.handle.net/2117/177600

الاتاحة: http://hdl.handle.net/2117/177600
https://doi.org/10.1145/3340923

المؤلفون: Voigt, Marco

المساهمون: Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft, Clare Dixon and Marcelo Finger

المصدر: FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems ; https://inria.hal.science/hal-01592169 ; FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. pp.244-261, ⟨10.1007/978-3-319-66167-4_14⟩

مصطلحات موضوعية: combination of theories, difference constraints, linear arithmetic constraints, Bernays–Schönfinkel–Ramsey fragment, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: Brasilia, Brazil

الاتاحة: https://inria.hal.science/hal-01592169
https://inria.hal.science/hal-01592169v1/document
https://inria.hal.science/hal-01592169v1/file/VoigtFroCoS.pdf
https://doi.org/10.1007/978-3-319-66167-4_14

المؤلفون: Bromberger, Martin, Weidenbach, Christoph

المساهمون: Saarbrücken Graduate School of Computer Science, Université de la Sarre, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Nicola Olivetti and Ashish Tiwari

المصدر: Automated Reasoning - 8th International Joint Conference (IJCAR 2016) ; https://inria.hal.science/hal-01403200 ; Automated Reasoning - 8th International Joint Conference (IJCAR 2016), 2016, Coimbra, Portugal. pp.116-132, ⟨10.1007/978-3-319-40229-1_9⟩

مصطلحات موضوعية: Linear Arithmetic, SMT, Integer Arithmetic, Constraint Solving, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]

جغرافية الموضوع: Coimbra, Portugal

الاتاحة: https://inria.hal.science/hal-01403200
https://inria.hal.science/hal-01403200v1/document
https://inria.hal.science/hal-01403200v1/file/IJCAR2016.pdf
https://doi.org/10.1007/978-3-319-40229-1_9

المؤلفون: Candeago, L., Larraz Hurtado, Daniel, Oliveras Llunell, Albert, Rodríguez Carbonell, Enric, Rubio Gimeno, Alberto

المساهمون: Universitat Politècnica de Catalunya. Departament de Ciències de la Computació, Universitat Politècnica de Catalunya. LOGPROG - Lògica i Programació

مصطلحات موضوعية: Àrees temàtiques de la UPC::Informàtica::Intel·ligència artificial, Boolean satisfiability problem, Formal logic, Graph theory, Reconfigurable hardware, Semantics, Constraint based method, Integer arithmetic, Invariant generations, Linear arithmetic, Non terminations, Program analysis, Program semantics, Verification systems, Computer circuits, Problema de satisfacibilitat booleana

وصف الملف: 18 p.

Relation: http://link.springer.com/chapter/10.1007%2F978-3-319-40970-2_18; Candeago, L., Larraz, D., Oliveras, A., Rodriguez, E., Rubio, A. Speeding up the constraint-based method in difference logic. A: International Conference on Theory and Applications of Satisfiability Testing. "Theory and Applications of Satisfiability Testing – SAT 2016, 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings". Bordeaux: 2016, p. 284-301.; http://hdl.handle.net/2117/102254

الاتاحة: http://hdl.handle.net/2117/102254
https://doi.org/10.1007/978-3-319-40970-2_18