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