Automated Reasoning / Peltier, Nicolas ; Sofronie-Stokkermans, Viorica  

Público ISBD Ningún comentario para este registro. Título : Automated Reasoning : 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. Idioma : Inglés (eng) 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 Clasificación: 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. Tipo de medio : Computadora Summary : This two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods). The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics: Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools *The conference was held virtually due to the COVID-19 pandemic. Chapter 'Constructive Hybrid Games' is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Automated Reasoning : 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. Idioma : Inglés (eng) 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 Clasificación: 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. Tipo de medio : Computadora Summary : This two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods). The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics: Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools *The conference was held virtually due to the COVID-19 pandemic. Chapter 'Constructive Hybrid Games' is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]

Automated Reasoning / Peltier, Nicolas ; Sofronie-Stokkermans, Viorica  

Público ISBD Ningún comentario para este registro. Título : Automated Reasoning : 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. Idioma : Inglés (eng) 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 Clasificación: 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). Tipo de medio : Computadora Summary : This two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods). The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics: Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools *The conference was held virtually due to the COVID-19 pandemic. Chapter 'A Fast Verified Liveness Analysis in SSA Form' is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] Automated Reasoning : 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. Idioma : Inglés (eng) 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 Clasificación: 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). Tipo de medio : Computadora Summary : This two-volume set LNAI 12166 and 12167 constitutes the refereed proceedings of the 10th International Joint Conference on Automated Reasoning, IJCAR 2020, held in Paris, France, in July 2020.* In 2020, IJCAR was a merger of the following leading events, namely CADE (International Conference on Automated Deduction), FroCoS (International Symposium on Frontiers of Combining Systems), ITP (International Conference on Interactive Theorem Proving), and TABLEAUX (International Conference on Analytic Tableaux and Related Methods). The 46 full research papers, 5 short papers, and 11 system descriptions presented together with two invited talks were carefully reviewed and selected from 150 submissions. The papers focus on the following topics: Part I: SAT; SMT and QBF; decision procedures and combination of theories; superposition; proof procedures; non classical logics Part II: interactive theorem proving/ HOL; formalizations; verification; reasoning systems and tools *The conference was held virtually due to the COVID-19 pandemic. Chapter 'A Fast Verified Liveness Analysis in SSA Form' is available open access under a Creative Commons Attribution 4.0 International License via link.springer.com. Enlace de acceso : https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...]

---

1 (1 - 2 / 2) Ver por página : 25 50 100 200