septiembre 2011 – Página 2

LI2011-12: Comienzo del curso

PorJosé A. Alonso 25 septiembre 201125 septiembre 2011

Las clases del curso Lógica informática (2011-12) comenzarán el lunes 26 de septiembre.

El problema de la sucesión de Langford

PorJosé A. Alonso 25 septiembre 2011

Un problema en el que se muestra la capacidad deductiva de Prolog es el siguiente problema de Langford.

Se dice que L es una sucesión de Langford si L es una lista de longitud 27 en la cual aparecen 3 veces cada uno de los dígitos del 1 al 9 y que además cumple la propiedad de que entre dos 1 siempre hay un dígito, entre dos 2 hay dos dígitos, entre dos 3 hay tres dígitos, etc. Por ejemplo,

[1,9,1,2,1,8,2,4,6,2,7,9,4,5,8,6,3,4,7,5,3,9,6,8,3,5,7]

es una sucesión de Langford.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Definir la relación langford tal que langford(?L) se verifique si
% L es una sucesión de Langford. Por ejemplo,
%    ?- langford(L).
%    L = [1,9,1,2,1,8,2,4,6,2,7,9,4,5,8,6,3,4,7,5,3,9,6,8,3,5,7] ;
%    L = [1,8,1,9,1,5,2,6,7,2,8,5,2,9,6,4,7,5,3,8,4,6,3,9,7,4,3] 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

langford(L) :-
   length(L,27),
   sublista([1,_,1,_,1],L),
   sublista([2,_,_,2,_,_,2],L),
   sublista([3,_,_,_,3,_,_,_,3],L),
   sublista([4,_,_,_,_,4,_,_,_,_,4],L),
   sublista([5,_,_,_,_,_,5,_,_,_,_,_,5],L),
   sublista([6,_,_,_,_,_,_,6,_,_,_,_,_,_,6],L),
   sublista([7,_,_,_,_,_,_,_,7,_,_,_,_,_,_,_,7],L),
   sublista([8,_,_,_,_,_,_,_,_,8,_,_,_,_,_,_,_,_,8],L),
   sublista([9,_,_,_,_,_,_,_,_,_,9,_,_,_,_,_,_,_,_,_,9],L).

% sublista(?L1,+L2) se verifica si L1 es una sublista de L2.
sublista(L1,L2):-
   append(_,L3,L2),
   append(L1,_,L3).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Definir la relación langford tal que langford(?L) se verifique si

% L es una sucesión de Langford. Por ejemplo,

% ?- langford(L).

% L = [1,9,1,2,1,8,2,4,6,2,7,9,4,5,8,6,3,4,7,5,3,9,6,8,3,5,7] ;

% L = [1,8,1,9,1,5,2,6,7,2,8,5,2,9,6,4,7,5,3,8,4,6,3,9,7,4,3]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

langford(L) :-

length(L,27),

sublista([1,_,1,_,1],L),

sublista([2,_,_,2,_,_,2],L),

sublista([3,_,_,_,3,_,_,_,3],L),

sublista([4,_,_,_,_,4,_,_,_,_,4],L),

sublista([5,_,_,_,_,_,5,_,_,_,_,_,5],L),

sublista([6,_,_,_,_,_,_,6,_,_,_,_,_,_,6],L),

sublista([7,_,_,_,_,_,_,_,7,_,_,_,_,_,_,_,7],L),

sublista([8,_,_,_,_,_,_,_,_,8,_,_,_,_,_,_,_,_,8],L),

sublista([9,_,_,_,_,_,_,_,_,_,9,_,_,_,_,_,_,_,_,_,9],L).

% sublista(?L1,+L2) se verifica si L1 es una sublista de L2.

sublista(L1,L2):-

append(_,L3,L2),

append(L1,_,L3).

I1M2010: Examen de septiembre de 2011

PorJosé A. Alonso 16 septiembre 201124 septiembre 2011

Hoy de se ha realizado el examen de la convocatoria de septiembre de la asignatura de Informática de 1º del Grado en Matemáticas.

A continuación se muestra el examen junto con su solución:
Read More “I1M2010: Examen de septiembre de 2011”

Lecturas compartidas en Twitter (Agosto de 2011)

PorJosé A. Alonso 3 septiembre 2011

Esta entrada es una recopilación de lecturas que he compartido en Twitter. La recopilación de los tweets está ordenada según la fecha de su publicación en Twitter.

Lecturas del Grupo de Lógica Computacional (Agosto de 2011)

PorJosé A. Alonso 2 septiembre 201110 septiembre 2011

Esta entrada es una recopilación de lecturas compartidas en la lista de correo del grupo de lógica computacional durante el mes de agosto de 2011.

La recopilación está ordenada por la fecha de su publicación en la lista. Al final de cada artículo se encuentra etiquetas relativas a los sistemas que usa o a su contenido.

Theorem proving for verification (the early days) #Historia
Selecting attributes for sport forecasting using formal concept analysis #AFC
Lecturas del Grupo de Lógica Computacional (Julio de 2011). #GLC #Vestigium
Formal methods: practice and experience #Métodos_formales
Automated deduction for verification #DAT
Software model checking #Model_checking
The verified software initiative: A Manifesto #Verificación
How can i do that with ACL2 recent enhancements to ACL2 #ACL2
Algebraic proofs over noncommutative formulas #Cálculo_polinomial
Studies in algebraic and propositional proof complexity #Tesis #Cálculo_polinomial
Formalization of an Efficient Representation of Bernstein Polynomials and Applications to Global Optimization #PVS
Automating Algebraic Methods in Isabelle #Isabelle
A Repository for Tarski-Kleene Algebras #Isabelle
Emergence and refinement #Emergencia #Refinamentos
Automated Proving in Geometry using Gröbner Bases in Isabelle/HOL #Isabelle
How Efficient Can Fully Verified Functional Programs Be – A Case Study of Graph Traversal Algorithms #Isabelle
Imperative functional programming with Isabelle/HOL #Isabelle
A Flexible Formal Verification Framework for Industrial Scale Validation #ACL2
Markets are Efficient if and Only if P = NP.
Bit-Blasting ACL2 Theorems #ACL2 #GL
A Verified Framework for Symbolic Execution in the ACL2 Theorem Prover. #ACL2 #GL
Integrating Testing and Interactive Theorem Proving #ACL2
seL4 Enforces Integrity #Isabelle
Peirce’s Truth-functional Analysis and the Origin of Truth Tables. #Historia
Towards Flight Control Verification Using Automated Theorem Proving #MetiTarski
Ott: Effective tool support for the working semanticist. #Ott #Coq #Isabelle #HOL
Lightweight Tools for Heavyweight Semantics. #Lem #Ott #Coq #Isabelle #HOL
Verifying SAT and SMT in Coq for a fully automated decision procedure. #Coq #SAT #SMT
Maximum Cardinality Matching. #Isabelle
Premise Selection for Mathematics by Corpus Analysis and Kernel Methods. #AA
Gauss-Jordan Elimination for Matrices Represented as Functions. #Isabelle
Verification of Dependable Software using Spark and Isabelle. #Isabelle
Verification of Programs in Virtual Memory Using Separation Logic. #Isabelle
Automated Specification Analysis Using an Interactive Theorem Prover. #ACL2
Formal Analysis of Fractional Order Systems in HOL. #HOL

En Mendeley también se encuentran las lecturas del Grupo de Lógica Computacional.