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