Autor Sofronie-Stokkermans, Viorica
|
|
Documentos disponibles escritos por este autor (2)
Hacer una sugerencia Refinar búsqueda10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I / Peltier, Nicolas ; Sofronie-Stokkermans, Viorica
TÃtulo : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I Tipo de documento: documento electrónico Autores: Peltier, Nicolas, ; Sofronie-Stokkermans, Viorica, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2020 Número de páginas: XXVII, 537 p. 1161 ilustraciones, 9 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-51074-9 Nota general: Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos. Palabras clave: TeorÃa de las máquinas Inteligencia artificial Ciencias de la Computación IngenierÃa de software Compiladores (programas informáticos) Programación de computadoras Lenguajes formales y teorÃa de los autómatas Lógica informática y fundamentos de la programación Compiladores e intérpretes Técnicas de programación Ãndice Dewey: 5.131 Resumen: Este conjunto de dos volúmenes LNAI 12166 y 12167 constituye las actas arbitradas de la 10.ª Conferencia Internacional Conjunta sobre Razonamiento Automatizado, IJCAR 2020, celebrada en ParÃs, Francia, en julio de 2020.* En 2020, IJCAR fue una fusión de los siguientes eventos importantes: a saber, CADE (Conferencia internacional sobre deducción automatizada), FroCoS (Simposio internacional sobre fronteras de sistemas combinados), ITP (Conferencia internacional sobre demostración interactiva de teoremas) y TABLEAUX (Conferencia internacional sobre cuadros analÃticos y métodos relacionados). Los 46 artÃculos de investigación completos, 5 artÃculos breves y 11 descripciones de sistemas presentados junto con dos charlas invitadas fueron cuidadosamente revisados ​​y seleccionados entre 150 presentaciones. Los artÃculos se centran en los siguientes temas: Parte I: SAT; SMT y QBF; procedimientos de decisión y combinación de teorÃas; superposición; procedimientos de prueba; lógicas no clásicas Parte II: demostración interactiva de teoremas/ HOL; formalizaciones; verificación; sistemas y herramientas de razonamiento *La conferencia se realizó de manera virtual debido a la pandemia de COVID-19. El capÃtulo ''Juegos hÃbridos constructivos'' está disponible en acceso abierto bajo una licencia internacional Creative Commons Attribution 4.0 a través de link.springer.com. Nota de contenido: Invited Paper -- Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints -- SAT; SMT and QBF -- An SMT Theory of Fixed-Point Arithmetic -- Covered Clauses Are Not Propagation Redundant -- The Resolution of Keller's Conjecture -- How QBF Expansion Makes Strategy Extraction Hard -- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates -- Solving bit-vectors with MCSAT: explanations from bits and pieces -- Monadic Decomposition in Integer Linear Arithmetic -- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis -- Decision Procedures and Combination of Theories -- Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols -- Combined Covers and Beth Definability -- Deciding Simple Infinity Axiom Sets with one Binary Relation by Means of Superpostulates -- A Decision Procedure for String to Code Point Conversion -- Politeness for The Theory of Algebraic Datatypes -- Superposition -- A Knuth-Bendix-Like Ordering for Orienting Combinator Equations -- A Combinator-Based Superposition Calculus for Higher-Order Logic -- Subsumption Demodulation in First-Order Theorem Proving -- A Comprehensive Framework for Saturation Theorem Proving -- Proof Procedures -- Possible Models Computation and Revision - A Practical Approach -- SGGS Decision Procedures -- Integrating Induction and Coinduction via Closure Operators and Proof Cycles -- Logic-Independent Proof Search in Logical Frameworks (short paper) -- Layered Clause Selection for Theory Reasoning (short paper) -- Non Classical Logics -- Description Logics with Concrete Domains and General Concept Inclusions Revisited -- A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic -- Constructive Hybrid Games -- Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) -- NP Reasoning in the Monotone µ-Calculus -- Soft subexponentials and multiplexing -- Mechanised Modal Model Theory. En lÃnea: https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Link: https://biblioteca.umanizales.edu.co/ils/opac_css/index.php?lvl=notice_display&i 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part I [documento electrónico] / Peltier, Nicolas, ; Sofronie-Stokkermans, Viorica, . - 1 ed. . - [s.l.] : Springer, 2020 . - XXVII, 537 p. 1161 ilustraciones, 9 ilustraciones en color.
ISBN : 978-3-030-51074-9
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Palabras clave: TeorÃa de las máquinas Inteligencia artificial Ciencias de la Computación IngenierÃa de software Compiladores (programas informáticos) Programación de computadoras Lenguajes formales y teorÃa de los autómatas Lógica informática y fundamentos de la programación Compiladores e intérpretes Técnicas de programación Ãndice Dewey: 5.131 Resumen: Este conjunto de dos volúmenes LNAI 12166 y 12167 constituye las actas arbitradas de la 10.ª Conferencia Internacional Conjunta sobre Razonamiento Automatizado, IJCAR 2020, celebrada en ParÃs, Francia, en julio de 2020.* En 2020, IJCAR fue una fusión de los siguientes eventos importantes: a saber, CADE (Conferencia internacional sobre deducción automatizada), FroCoS (Simposio internacional sobre fronteras de sistemas combinados), ITP (Conferencia internacional sobre demostración interactiva de teoremas) y TABLEAUX (Conferencia internacional sobre cuadros analÃticos y métodos relacionados). Los 46 artÃculos de investigación completos, 5 artÃculos breves y 11 descripciones de sistemas presentados junto con dos charlas invitadas fueron cuidadosamente revisados ​​y seleccionados entre 150 presentaciones. Los artÃculos se centran en los siguientes temas: Parte I: SAT; SMT y QBF; procedimientos de decisión y combinación de teorÃas; superposición; procedimientos de prueba; lógicas no clásicas Parte II: demostración interactiva de teoremas/ HOL; formalizaciones; verificación; sistemas y herramientas de razonamiento *La conferencia se realizó de manera virtual debido a la pandemia de COVID-19. El capÃtulo ''Juegos hÃbridos constructivos'' está disponible en acceso abierto bajo una licencia internacional Creative Commons Attribution 4.0 a través de link.springer.com. Nota de contenido: Invited Paper -- Efficient Automated Reasoning about Sets and Multisets with Cardinality Constraints -- SAT; SMT and QBF -- An SMT Theory of Fixed-Point Arithmetic -- Covered Clauses Are Not Propagation Redundant -- The Resolution of Keller's Conjecture -- How QBF Expansion Makes Strategy Extraction Hard -- Removing Algebraic Data Types from Constrained Horn Clauses Using Difference Predicates -- Solving bit-vectors with MCSAT: explanations from bits and pieces -- Monadic Decomposition in Integer Linear Arithmetic -- Scalable Algorithms for Abduction via Enumerative Syntax-Guided Synthesis -- Decision Procedures and Combination of Theories -- Deciding the Word Problem for Ground Identities with Commutative and Extensional Symbols -- Combined Covers and Beth Definability -- Deciding Simple Infinity Axiom Sets with one Binary Relation by Means of Superpostulates -- A Decision Procedure for String to Code Point Conversion -- Politeness for The Theory of Algebraic Datatypes -- Superposition -- A Knuth-Bendix-Like Ordering for Orienting Combinator Equations -- A Combinator-Based Superposition Calculus for Higher-Order Logic -- Subsumption Demodulation in First-Order Theorem Proving -- A Comprehensive Framework for Saturation Theorem Proving -- Proof Procedures -- Possible Models Computation and Revision - A Practical Approach -- SGGS Decision Procedures -- Integrating Induction and Coinduction via Closure Operators and Proof Cycles -- Logic-Independent Proof Search in Logical Frameworks (short paper) -- Layered Clause Selection for Theory Reasoning (short paper) -- Non Classical Logics -- Description Logics with Concrete Domains and General Concept Inclusions Revisited -- A Formally Verified, Optimized Monitor for Metric First-Order Dynamic Logic -- Constructive Hybrid Games -- Formalizing a Seligman-Style Tableau System for Hybrid Logic (short paper) -- NP Reasoning in the Monotone µ-Calculus -- Soft subexponentials and multiplexing -- Mechanised Modal Model Theory. En lÃnea: https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Link: https://biblioteca.umanizales.edu.co/ils/opac_css/index.php?lvl=notice_display&i
TÃtulo : 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II Tipo de documento: documento electrónico Autores: Peltier, Nicolas, ; Sofronie-Stokkermans, Viorica, Mención de edición: 1 ed. Editorial: [s.l.] : Springer Fecha de publicación: 2020 Número de páginas: XVII, 511 p. 2094 ilustraciones, 114 ilustraciones en color. ISBN/ISSN/DL: 978-3-030-51054-1 Nota general: Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos. Palabras clave: TeorÃa de las máquinas Inteligencia artificial Ciencias de la Computación IngenierÃa de software Compiladores (programas informáticos) Programación de computadoras Lenguajes formales y teorÃa de los autómatas Lógica informática y fundamentos de la programación Compiladores e intérpretes Técnicas de programación Ãndice Dewey: 5.131 Resumen: Este conjunto de dos volúmenes LNAI 12166 y 12167 constituye las actas arbitradas de la 10.ª Conferencia Internacional Conjunta sobre Razonamiento Automatizado, IJCAR 2020, celebrada en ParÃs, Francia, en julio de 2020.* En 2020, IJCAR fue una fusión de los siguientes eventos importantes: a saber, CADE (Conferencia internacional sobre deducción automatizada), FroCoS (Simposio internacional sobre fronteras de sistemas combinados), ITP (Conferencia internacional sobre demostración interactiva de teoremas) y TABLEAUX (Conferencia internacional sobre cuadros analÃticos y métodos relacionados). Los 46 artÃculos de investigación completos, 5 artÃculos breves y 11 descripciones de sistemas presentados junto con dos charlas invitadas fueron cuidadosamente revisados ​​y seleccionados entre 150 presentaciones. Los artÃculos se centran en los siguientes temas: Parte I: SAT; SMT y QBF; procedimientos de decisión y combinación de teorÃas; superposición; procedimientos de prueba; lógicas no clásicas Parte II: demostración interactiva de teoremas/ HOL; formalizaciones; verificación; sistemas y herramientas de razonamiento *La conferencia se realizó de manera virtual debido a la pandemia de COVID-19. El capÃtulo ''Un análisis rápido de vida verificado en formato SSA'' está disponible en acceso abierto bajo una licencia internacional Creative Commons Attribution 4.0 a través de link.springer.com. Nota de contenido: Interactive Theorem Proving/ HOL -- Competing inheritance paths in dependent type theory: a case study in functional analysis -- A Lean tactic for normalising ring expressions with exponents (short paper) -- Practical proof search for Coq by type inhabitation -- Quotients of Bounded Natural Functors -- Trakhtenbrot's Theorem in Coq -- Deep Generation of Coq Lemma Names Using Elaborated Terms -- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs -- Validating Mathematical Structures -- Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description) -- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages -- Formalizations -- Formalizing the Face Lattice of Polyhedra -- Algebraically Closed Fields in Isabelle/HOL -- Formalization of Forcing in Isabelle/ZF -- Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL -- Formal Proof of the Group Law for Edwards Elliptic Curves -- Verifying Farad_zev-Read type Isomorph-Free Exhaustive Generation -- Verification -- Verified Approximation Algorithms -- Efficient Verified Implementation of Introsort and Pdqsort -- A Fast Verified Liveness Analysis in SSA form -- Verification of Closest Pair of Points Algorithms -- Reasoning Systems and Tools -- A Polymorphic Vampire (short paper) -- N-PAT: A Nested Model-Checker (system description) -- HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description) -- Implementing superposition in iProver (system description) -- Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description) -- Make E Smart Again -- Automatically Proving and Disproving Feasibility Conditions -- µ-term: Verify Termination Properties Automatically (system description) -- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) -- The Imandra Automated Reasoning System (system description) -- A Programmer's Text Editor for a Logical Theory: The SUMOjEdit Editor (system description) -- Sequoia: a playground for logicians (system description) -- Prolog Technology Reinforcement Learning Prover (system description). En lÃnea: https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Link: https://biblioteca.umanizales.edu.co/ils/opac_css/index.php?lvl=notice_display&i 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II [documento electrónico] / Peltier, Nicolas, ; Sofronie-Stokkermans, Viorica, . - 1 ed. . - [s.l.] : Springer, 2020 . - XVII, 511 p. 2094 ilustraciones, 114 ilustraciones en color.
ISBN : 978-3-030-51054-1
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
Palabras clave: TeorÃa de las máquinas Inteligencia artificial Ciencias de la Computación IngenierÃa de software Compiladores (programas informáticos) Programación de computadoras Lenguajes formales y teorÃa de los autómatas Lógica informática y fundamentos de la programación Compiladores e intérpretes Técnicas de programación Ãndice Dewey: 5.131 Resumen: Este conjunto de dos volúmenes LNAI 12166 y 12167 constituye las actas arbitradas de la 10.ª Conferencia Internacional Conjunta sobre Razonamiento Automatizado, IJCAR 2020, celebrada en ParÃs, Francia, en julio de 2020.* En 2020, IJCAR fue una fusión de los siguientes eventos importantes: a saber, CADE (Conferencia internacional sobre deducción automatizada), FroCoS (Simposio internacional sobre fronteras de sistemas combinados), ITP (Conferencia internacional sobre demostración interactiva de teoremas) y TABLEAUX (Conferencia internacional sobre cuadros analÃticos y métodos relacionados). Los 46 artÃculos de investigación completos, 5 artÃculos breves y 11 descripciones de sistemas presentados junto con dos charlas invitadas fueron cuidadosamente revisados ​​y seleccionados entre 150 presentaciones. Los artÃculos se centran en los siguientes temas: Parte I: SAT; SMT y QBF; procedimientos de decisión y combinación de teorÃas; superposición; procedimientos de prueba; lógicas no clásicas Parte II: demostración interactiva de teoremas/ HOL; formalizaciones; verificación; sistemas y herramientas de razonamiento *La conferencia se realizó de manera virtual debido a la pandemia de COVID-19. El capÃtulo ''Un análisis rápido de vida verificado en formato SSA'' está disponible en acceso abierto bajo una licencia internacional Creative Commons Attribution 4.0 a través de link.springer.com. Nota de contenido: Interactive Theorem Proving/ HOL -- Competing inheritance paths in dependent type theory: a case study in functional analysis -- A Lean tactic for normalising ring expressions with exponents (short paper) -- Practical proof search for Coq by type inhabitation -- Quotients of Bounded Natural Functors -- Trakhtenbrot's Theorem in Coq -- Deep Generation of Coq Lemma Names Using Elaborated Terms -- Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs -- Validating Mathematical Structures -- Teaching Automated Theorem Proving by Example: PyRes 1.2 (system description) -- Beyond Notations: Hygienic Macro Expansion for Theorem Proving Languages -- Formalizations -- Formalizing the Face Lattice of Polyhedra -- Algebraically Closed Fields in Isabelle/HOL -- Formalization of Forcing in Isabelle/ZF -- Reasoning about Algebraic Structures with Implicit Carriers in Isabelle/HOL -- Formal Proof of the Group Law for Edwards Elliptic Curves -- Verifying Farad_zev-Read type Isomorph-Free Exhaustive Generation -- Verification -- Verified Approximation Algorithms -- Efficient Verified Implementation of Introsort and Pdqsort -- A Fast Verified Liveness Analysis in SSA form -- Verification of Closest Pair of Points Algorithms -- Reasoning Systems and Tools -- A Polymorphic Vampire (short paper) -- N-PAT: A Nested Model-Checker (system description) -- HYPNO: Theorem Proving with Hypersequent Calculi for Non-Normal Modal Logics (system description) -- Implementing superposition in iProver (system description) -- Moin: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (system description) -- Make E Smart Again -- Automatically Proving and Disproving Feasibility Conditions -- µ-term: Verify Termination Properties Automatically (system description) -- ENIGMA Anonymous: Symbol-Independent Inference Guiding Machine (system description) -- The Imandra Automated Reasoning System (system description) -- A Programmer's Text Editor for a Logical Theory: The SUMOjEdit Editor (system description) -- Sequoia: a playground for logicians (system description) -- Prolog Technology Reinforcement Learning Prover (system description). En lÃnea: https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Link: https://biblioteca.umanizales.edu.co/ils/opac_css/index.php?lvl=notice_display&i
