|
|
| (No se muestran 8 ediciones intermedias de 2 usuarios) |
| Línea 1: |
Línea 1: |
| − | == Lecturas compartidas ==
| + | En esta sección se recopila las lecturas compartidas en la lista de correo del Grupo de Lógica Computacional. La lecturas están ordenadas por la fecha de su publicación en la lista del GLC: |
| − | En esta sección se recopilada la lecturas compartidas en en lista de correo del Grupo de Lógica Computacional, ordenadas por orden cronológico según su publicación en la lista. | + | * [[Lecturas del año 2010]]. |
| | + | * [[Lecturas del año 2011]]. |
| | + | * [[Lecturas del año 2012]]. |
| | + | * [[Lecturas del año 2013]]. |
| | + | * [[Lecturas del año 2014]]. |
| | | | |
| − | === Lecturas del 27-Oct-2010 al 1-Jul-2011 ===
| + | Antes del 2010, las lecturas se comentaban en la wiki y su relación se encuentra [[Lecturas comentadas | aquí]]. |
| − | * [http://goo.gl/Mpz03 Ejercicios de programación en Haskell] #Haskell #V
| |
| − | * [http://goo.gl/0FwrK El valor del fracaso digno] #CM
| |
| − | * [http://goo.gl/aWC1 Computational science: ... Error (... why scientific programming does not compute)] #Verificación
| |
| − | * [http://goo.gl/5mUCh El tipo abstracto de datos de las pilas en Haskell] #Haskell #V
| |
| − | * [http://goo.gl/rwY3S The free-form linguistics revolution in mathematica]
| |
| − | * [http://goo.gl/3hNgt A preliminary survey on functional programming] #PF
| |
| − | * [http://goo.gl/HDZyb Desarrollo del comando wc de Unix en Haskell] #Haskell #V
| |
| − | * [http://goo.gl/AVXPW Lógica Computacional en Sevilla (30 años en una hora)] #V
| |
| − | * [http://goo.gl/V7Sud Problema sobre números naturales] #Haskell #V
| |
| − | * [http://goo.gl/PkVYW Rompecabeza de Ullman en Haskell] #Haskell #V
| |
| − | * [http://goo.gl/hWPRa Lisp bot wins Google AI challenge — Will Lisp win in the semantic web, too?] #Lisp #IA
| |
| − | * [http://goo.gl/NRnls Decálogo de la didáctica matemática] #Enseñanza #V
| |
| − | * [http://goo.gl/b9gFY El decálogo del profesor (según Polya)] #Enseñanza #V
| |
| − | * [http://goo.gl/CnWj0 Proceedings Workshop on Partiality and Recursion in Interactive Theorem Provers en] #Libro #AR
| |
| − | * [http://goo.gl/87Z9o Parallelizing a CLIPS-based course timetabling expert system] #SE
| |
| − | * [http://goo.gl/s4etS Certifying compilers using higher-order theorem provers as certificate checkers] #Verificación #V
| |
| − | * [http://goo.gl/wo8BN Teorías y aplicaciones] #V
| |
| − | * [http://goo.gl/95csF Does Godel's theorem matter to mathematics?]
| |
| − | * [http://goo.gl/LBsyx Distributed SAT] #SAT
| |
| − | * [http://posgrado.escom.ipn.mx/biblioteca/Semantic%20web%20reasoners%20and%20languages.pdf Semantic web reasoners and languages] #WS
| |
| − | * [http://bit.ly/emHhvZ El 2011 y los números primos (en Haskell)] #Haskell #V
| |
| − | * [http://bit.ly/ebNi54 The Dialectica interpertation in Coq] #Coq
| |
| − | * [http://bit.ly/heSTJJ Errores aritméticos en Haskell y en Lisp] #Haskell #Lisp #V
| |
| − | * [http://bit.ly/gLU60K Why Lisp is a big hack (and haskell is doomed to succeed)] #Lisp #Haskell
| |
| − | * [http://bit.ly/h5v14x ProofWiki y la verificación de las demostraciones matemáticas] #Verificación #MKM #V
| |
| − | * [http://bit.ly/fMi9V7 A quick and gentle guide to constraint logic programming via ECLiPSe] #PL #Restricciones
| |
| − | * [http://bit.ly/gb4Dn9 A language for mathematical knowledge management] #MKM
| |
| − | * [http://bit.ly/eLkbsW Automated inference of finite unsatisfiability] #AR
| |
| − | * [http://bit.ly/evywxv The free vector space on a type] http://bit.ly/e9c5Zl #Haskell
| |
| − | * [http://goo.gl/6t8YI Formal methods applied to a floating-point number system] #Z
| |
| − | * [http://goo.gl/WT6G3 A machine-checked theory of floating point arithmetic] #HOL_Light
| |
| − | * [http://goo.gl/k6NJJ Formal verification of floating point trigonometric functions] #HOL_Light
| |
| − | * [http://goo.gl/RRb7p A case study in formal verification of register-transfer logic with ACL2: The floating point adder of the AMD Athlon TM processor] #ACL2
| |
| − | * [http://goo.gl/gvh4C A Generic Library for Floating-Point Numbers and Its Application to Exact Computing] #Coq.
| |
| − | * [http://goo.gl/oEgxU A High-Level Formalization of Floating-Point Numbers in PVS] #PVS
| |
| − | * [http://goo.gl/4CHMF Formal verification of floating-point programs] #Coq
| |
| − | * [http://goo.gl/W9svV The pitfalls of verifying floating-point computations] #Verificación
| |
| − | * [http://goo.gl/xs5IG Floats and Ropes: A Case Study for Formal Numerical Program Verification] #Coq.
| |
| − | * [http://bit.ly/grfNfD Algorithms Take Control of Wall Street] #IA
| |
| − | * [http://bit.ly/gC0m7p Formal reliability analysis of combinational circuits using theorem proving] #HOL
| |
| − | * [http://bit.ly/f8Nvpv Determinación, esperanza y éxitos en la resolución de problemas] #Enseñanza #V
| |
| − | * [http://bit.ly/gZYKNJ Lectures in Game Theory for Computer Scientists] #Libro
| |
| − | * [http://bit.ly/dNvlXU Reactive Valuations] #TFM
| |
| − | * [http://slidesha.re/f8SKgI Oportunidades para la economía basada en la Ingeniería del Conocimiento en Internet]
| |
| − | * [http://bit.ly/haeTax Algunas aplicaciones de las bases de Groebner]
| |
| − | * [http://bit.ly/hrwBXD Programación funcional con Haskell] #Libro #Haskell
| |
| − | * [http://bit.ly/eGqBDZ Certifying compilers using higher-order theorem provers as certificate checker] #Isabelle #Coq
| |
| − | * [http://bit.ly/ht6544 El tipo abstracto de datos de las colas en Haskell] #Haskell #V
| |
| − | * [http://bit.ly/eZiRVL Deducción natural en lógica proposicional con Isabelle/Isar] #Isabelle #V
| |
| − | * [http://bit.ly/hTYRXf Deducción natural en lógica de primer orden con Isabelle/Isar] #Isabelle #V
| |
| − | * [http://bit.ly/h2co0D fKenzo: A user interface for computations in Algebraic Topology]
| |
| − | * [http://bit.ly/hZdkPN A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL]. #Isabelle
| |
| − | * [http://bit.ly/gcvJNz El tipo abstracto de datos de las colas de prioridad en Haskell] #Haskell #V
| |
| − | * [http://bit.ly/epypbt Program Verification and Functioning of Operative Computing Revisited: How about Mathematics Engineering?] #Verificación
| |
| − | * [http://bit.ly/hIeQQi El próximo después de 1811] #Haskell #V
| |
| − | * [http://bit.ly/hWod4k Humanos más capaces y robots que están en las nubes] #IA
| |
| − | * [http://bit.ly/fTekAA Charming Proofs: A Journey Into Elegant Mathematics] #Libro #DAO
| |
| − | * [http://bit.ly/fpnnu7 Functional Binomial Queues] #RF #Isabelle
| |
| − | * [http://bit.ly/glOw9x Lower Semicontinuous Functions] #RF #Isabelle
| |
| − | * [http://bit.ly/hvqHiB Lógica Informática (2010-11)] #V
| |
| − | * [http://bit.ly/e6TgsN Inconsistent heuristics in theory and practice] #IA
| |
| − | * [http://goo.gl/Igcbu On proof and progress in mathematics] #CM
| |
| − | * [http://bit.ly/i9FH8v Artificial Intelligence (Foundations of Computational Agents)] #Libro #IA
| |
| − | * [http://bit.ly/eLUOMY Are Mathematicians In Jeopardy?] #IA
| |
| − | * [http://bit.ly/fMVueD Give me that good old-fashioned AI] #IA
| |
| − | * [http://bit.ly/evZnr7 Building Watson: An Overview of the DeepQA Project] #IA
| |
| − | * [http://bit.ly/hJWFDv Software verification turns maintstream] #Verificación
| |
| − | * [http://rok.strnisa.com/thesis/thesis.pdf Formalising, improving, and reusing the Java Module System] http://bit.ly/dF68vF #Tesis #Isabelle
| |
| − | * [http://goo.gl/D4L3j SMT solvers: new oracles for the HOL theorem prover] #SMT #HOL4
| |
| − | * [http://bit.ly/e3QiRU Isabelle como un lenguaje funcional] #Isabelle #V
| |
| − | * [http://bit.ly/fKKC3D El tipo abstracto de datos de las pilas en Haskell] #Haskell #V
| |
| − | * [http://bit.ly/hBKzIz El tipo abstracto de datos de las colas en Haskell] #Haskell #V
| |
| − | * [http://goo.gl/oUlcY Executable Transitive Closures of Finite Relations] #RF #Isabelle
| |
| − | * [http://goo.gl/epNrc Solución española para un problema de John Nash] Reduced Ordered Binary Decision Diagram with Implied Literals: A New knowledge Compilation Approach http://goo.gl/FoL94 #AR
| |
| − | * [http://bit.ly/gHpfXL Teaching FP to freshmen] #Enseñanza #PF
| |
| − | * [http://goo.gl/2fK3d Introduction to Artificial Intelligence] #Libro #IA
| |
| − | * [http://bit.ly/hZ9TWG La Universidad Carnegie-Mellon elimina la programación OO de su primer curso] #Enseñanza
| |
| − | * [http://goo.gl/NXhJI Experience Report: Functional Programming through Deep Time (Modeling the first complex ecosystems on Earth)] #Haskell
| |
| − | * [http://bit.ly/eEvWOO A Comparative Study on ILP-based Concept Discovery Systems] #ILP
| |
| − | * [http://bit.ly/gE69RT Logic-Based Artificial Intelligence] #Libro #IA
| |
| − | * [http://bit.ly/f4JcZN A Formalization of the C99 Standard in HOL, Isabelle and Coq] #HOL #Isabelle #Coq
| |
| − | * [http://bit.ly/gQRpsr Formal methods in agent-oriented software engineering] #MF
| |
| − | * [http://bit.ly/hO9ewV The cognitive agents specification language and verification environment] #Verificación
| |
| − | * [http://bit.ly/hjBReD Software Bugs and Scientific Progress] #Verificación
| |
| − | * [http://bit.ly/ffR1jT Representing model theory in a type-theoretical logical framework] #RF #Twelfe
| |
| − | * [http://goo.gl/vCDeE Towards a verification framework for faulty message passing systems in PVS] #PVS
| |
| − | * [http://bit.ly/g2tz4T Por qué y cómo se hace investigación en matemáticas] #CM
| |
| − | * [http://goo.gl/Y6pl Introduction to newLISP] #Libro #Lisp
| |
| − | * [http://goo.gl/23une Verified Firewall Policy Transformations for Test Case Generation] #Isabelle
| |
| − | * [http://goo.gl/bxSx7 An Approach to Modular and Testable Security Models of Real-world Health-care Applications] #Isabelle
| |
| − | * [http://bit.ly/fTzgF0 Psi-calculi: a framework for mobile processes with nominal data and logic] #Isabelle
| |
| − | * [http://goo.gl/ZAqRw Artificial Intelligence and Human Thinking] #IA
| |
| − | * [http://goo.gl/aKNFv Simplification Rules for Intuitionistic Propositional Tableaux] #AR
| |
| − | * [http://bit.ly/e0qElc A Fast and Verified Algorithm for Proving Store-and-Forward Networks Deadlock-Free] #ACL2
| |
| − | * [http://bit.ly/h7oESi Gestión mecanizada del conocimiento matemático en Topología algebraica] #Tesis #ACL2
| |
| − | * [http://bit.ly/faUvcE The first formalized math wiki is here] #MKM
| |
| − | * [http://bit.ly/fAt2n2 Los matemáticos no buscan resultados, van tras la belleza] #CM
| |
| − | * [http://bit.ly/hXvjFF Extending Sledgehammer with SMT Solvers] #Isabelle #SMT
| |
| − | * [http://bit.ly/eTdbPY Book of proof] #Libro #DAO
| |
| − | * [http://bit.ly/hTeyJl The General Triangle Is Unique] #RF #Isabelle
| |
| − | * [http://bit.ly/fPmmPo NASA Formal Methods] #Libro #MF #Verificación
| |
| − | * [http://bit.ly/eK1u3z How To Read A Mathematics Textbook] #Enseñanza
| |
| − | * [http://bit.ly/eGDE9E Haskell for the cloud] #Haskell
| |
| − | * [http://bit.ly/gx9OfA The OpenTheory Standard Theory Library] #Verificación
| |
| − | * [http://bit.ly/ghnBkQ A Coq-based Library for Interactive and Automated Theorem Proving in Plane Geometry] #RF #Coq
| |
| − | * [http://bit.ly/esoyE5 Mechanical Support for Efficient Dissemination on the CAN Overlay Network] #Isabelle
| |
| − | * [http://bit.ly/g0ybyb A Wiki for Formal Mathematics] #MKM
| |
| − | * [http://bit.ly/eNHWj1 Recent Developments in Computing and Philosophy] #Prover9
| |
| − | * [http://www.ps.uni-saarland.de/Publications/documents/DoczkalSmolka_2011_Constructive.pdf Constructive formalization of classical modal logic]. #Coq
| |
| − | * [http://bit.ly/f7uyEs Numbers as Data Structures: The Prime Successor Function as Primitive] #Enseñanza
| |
| − | * [http://bit.ly/iYb67t Proving Equality between Streams"] #Coq
| |
| − | * [http://bit.ly/dOkauQ The limits of correctness] #Verificación
| |
| − | * [http://bit.ly/e2aqGc A formal proof of the Riesz representation theorem] #RF #PVS
| |
| − | * [http://bit.ly/lXvY1G A formal proof that π₁(S¹)=Z] #RF #Coq
| |
| − | * [http://bit.ly/f0FX0O On a Strongly Normalizing STG Machine] #Tesis
| |
| − | * [http://bit.ly/hi9u3T Balancing Weight-Balanced Trees] #Coq #Haskell
| |
| − | * [http://bit.ly/gDCUy0 A Formal Programming Model of Orléans Skeleton Library] #Coq
| |
| − | * [http://bit.ly/gxGyjq Formal Verification of a small real-time operating system] #Tesis #Isabelle
| |
| − | * [http://bit.ly/io1joM Deus ex machina]. #Prover9
| |
| − | * [http://bit.ly/jdhTBc Computationally-discovered simplification of the ontological argument]. #Prover9
| |
| − | * [http://bit.ly/eI3roc Satisfiability of Acyclic and Almost Acyclic CNF Formulas (II)] #AR
| |
| − | * [http://bit.ly/f9tTAC Heaps and Data Structures: A Challenge for Automated Provers] #AR
| |
| − | * [http://bit.ly/jkEZGy Haskell: Not pure enough?] #Haskell
| |
| − | * [http://bit.ly/lT7IZ3 Verified Stack-Based Genetic Programming via Dependent Types] #RF #Agda #IA
| |
| − | * [http://bit.ly/lDrbjG Sorpresa sumando potencias de 2 en Haskell] #Haskell #V
| |
| − | * [http://bit.ly/kzKmwS A List-Machine Benchmark for Mechanized Metatheory] #AR
| |
| − | * [http://bit.ly/ls0jmQ The Locally Nameless Representation] #AR
| |
| − | * [http://bit.ly/j1Ma1D Formalização da prova do teorema de existência de unificadores mais gerais em teorias de primeira-ordem] #TFM #PVS
| |
| − | * [http://bit.ly/lxkECl Solving Rubik's Cube Using SAT Solvers] #SAT
| |
| − | * [http://bit.ly/kU11XQ Entusiasmo, clave del buen maestro] #Enseñanza
| |
| − | * [http://slidesha.re/iwSxsW Programação Funcional: Novos Horizontes para a Expansão da Consciência] #PF
| |
| − | * [http://bit.ly/lL64ln Computer certified efficient exact reals in Coq] #Coq
| |
| − | * [http://bit.ly/ieX6gS Parallel and Concurrent Programming in Haskell] #Haskell
| |
| − | * [http://bit.ly/lvyAWJ TRX: A Formally Verified Parser Interpreter] #Coq
| |
| − | * [http://bit.ly/lgbo2i Computational Meta-Ethics: Towards the Meta-Ethical Robot] #Prover9
| |
| − | * [http://bit.ly/j8R2cA Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover] #RF #Matita
| |
| − | * [http://bit.ly/kYxElW ALPprolog — A New Logic Programming Method for Dynamic Domains] #PL
| |
| − | * [http://bit.ly/mBQXgl Logical Formalization of Semantic Business Vocabulary and Rules"] #RC
| |
| − | * [http://bit.ly/illSo The Proof is in the Pudding (The Changing Nature of Mathematical Proof)] #Libro
| |
| − | * [http://goo.gl/JzUX7 Knowledge-Based Programs] #RF #Isabelle
| |
| − | * [http://bit.ly/kH7Xz7 Elegance and Power] #Haskell
| |
| − | * [http://bit.ly/iiAhk5 Validated Compilation through Logic] #Verificación
| |
| − | * [http://bit.ly/jXmH4d Teaching Computational Logic: Technology-enhanced Learning and Animations] #Enseñanza
| |
| − | * [http://bit.ly/k0HycO Sigma: An Integrated Development Environment for Formal Ontology] #RC
| |
| − | * [http://bit.ly/m3Qmr3 Termination of Isabelle Functions via Termination of Rewriting] #AR #Isabelle
| |
| − | * [http://bit.ly/koQ4Ti Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logics] #AR
| |
| − | * [http://bit.ly/jzGZo1 Rationality and Escalation in Infinite Extensive Games] #Libro #RF #Coq
| |
| − | * [http://bit.ly/lHXxS8 Efficient Interactive Construction of Machine-Checked Protocol Security Proofs in the Context of Dynamically Compromising Adversaries] #TFM #RF #Isabelle
| |
| − | * [http://bit.ly/iir2wI Specification and Verification: The Spec# Experience] #Verificación
| |
| − | * [http://bit.ly/lhybds Formal Verification of Chess Endgames Tables] #HOL4 #IA
| |
| − | * [http://bit.ly/l5BtTc Integrating Testing and Interactive Theorem Proving] #ACL2
| |
| − | * [http://bit.ly/l5gjtf Conway’s Games and Some of Their Basic Properties] #Mizar
| |
| − | * [http://bit.ly/jZeiPa A verified runtime for a verified theorem prover] #HOL4
| |
| − | * [http://bit.ly/jnkpNT Modelling distributed cognition systems in PVS] #PVS
| |
| − | * [http://bit.ly/kuY9Ad Three Chapters of Measure Theory in Isabelle/HOL] #RF #Isabelle
| |
| − | * [http://bit.ly/kbX6ZI seL4 Enforces Integrity] #Verificación #Isabelle
| |
| − | * [http://bit.ly/m4r6a7#RF Initial Semantics for higher-order typed syntax in Coq] #Coq
| |
| − | * [http://bit.ly/lGZVoa Initial Semantics for higher-order typed syntax in Coq] #RF #Coq
| |
| − | * [http://bit.ly/jXe3QN Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination] #RF #Coq
| |
| − | * [http://bit.ly/mOh20v Specification of imperative languages using operational semantics in Coq] #RF #Coq
| |
| − | * [http://bit.ly/mlftfm A First-Order Calculus for Allegories] #AR
| |
| − | * [http://bit.ly/imjeTQ Generating Schemata of Resolution Proofs] #AR
| |
| − | * [http://bit.ly/iGWaxr On the Generation of Positivstellensatz Witnesses in Degenerate Cases] #RF #Coq
| |
| − | * [http://bit.ly/lAHBc0 Deciding Kleene Algebras in Coq] #RF #Coq
| |
| − | * [http://bit.ly/lH7T3a Glasgow Haskell vs. Lispworks] #Haskell #Lisp
| |
| − | * [http://bit.ly/jzm3hG On the expressive power of unit resolution] #AR
| |
| − | * [http://bit.ly/jo9RKj Proceedings 15th International Refinement Workshop] #AR
| |
| − | * [http://bit.ly/mLskMG Solving the Unsolvable] #AR
| |
| − | * [http://bit.ly/kJTmix Type classes for efficient exact real arithmetic in Coq] #Coq
| |
| − | * [http://bit.ly/lbXy2P Un problema de las olimpiadas rusas en Haskell] #Haskell #V
| |
| − | * [http://bit.ly/lcO4n8 BDDs verified in a proof assistant] #Isabelle
| |
| − | * [http://arxiv.org/pdf/1106.3685v3 Embedding and Automating Conditional Logics in Classical Higher-Order Logic]
| |
| − | * [http://bit.ly/iJwaDm Incidence simplicial matrices formalized in Coq/SSReflect]. #RF #Coq
| |
| − | * [http://bit.ly/mTuPbK What’s Fun About Teaching] #Enseñanza
| |
| − | * [http://bit.ly/khYlHh Isabelle Repository for Relational and Algebraic Methods] #Isabelle
| |
| − | * [http://bit.ly/kPQSDw Automated Engineering of Relational and Algebraic Methods in Isabelle/HOL] #Isabelle
| |
| − | * [http://bit.ly/kANpSp SAT solver of Howe & King as a logic program] #SAT #PL
| |
| − | | |
| − | == Lecturas comentadas ==
| |
| − | En esta sección se recogen los comentarios de los miembros del Grupo de algunas de las lecturas de publicaciones relacionadas con los temas de investigación del Grupo.
| |
| − | # K.R. Apt y M.G. Wallace (2007) <br>''[[Constraint Logic Programming using Eclipse]]''.
| |
| − | # B. Buchberger (1991) <br> ''[[Logic for Computer Science]]''
| |
| − | # M. Cayli, A. G. Karatop, E. Kavlak, H. Kaynar, F. Ture y E. Erdem. (2007) <br>''[[Solving challenging grid puzzles with answer set programming]]''.
| |
| − | # G. Gonthier (2008) <br> ''[[Formal Proof: The Four-Color Theorem]]''
| |
| − | # T.C. Hales (2008) <br> ''[[Formal Proof]]''
| |
| − | # J. Harrison (1998) <br>''[[Formalizing basic first order model theory]]''
| |
| − | # J. Harrison (2007) <br>''[[A short survey of automated reasoning]]''
| |
| − | # J. Harrison (2008) <br> ''[[Formal Proof: Theory and Practice]]''
| |
| − | # C. Kaliszyk, F. van Raamsdonk, F. Wiedijk, H. Wupper, M. Hendriks y R. de Vrijer (2008) <br> ''[[Deduction using the ProofWeb system]]''.
| |
| − | # M. Krötzsch, D. Vrandecic, M. Völkel, H. Haller y R. Studer (2007) <br> ''[[Semantic Wikipedia]]''.
| |
| − | # N. Magaud, J Narboux y P. Schreck (2009) <br> ''[[Formalizing Desargues' theorem in Coq using ranks]]''.
| |
| − | # J. Rehmeyer (2008) <br> ''[[How to (really) trust a mathematical proof]]''.
| |
| − | # C.E. Veni Madhavan (2005) <br>''[[Mathematics and computer science: The interplay]]''.
| |
| − | # P. Marić y P. Janicić (2009)<br>''[[Formal Correctness Proof for DPLL Procedure]]''.
| |
| | | | |
| | [[Category:Lecturas]] | | [[Category:Lecturas]] |
