Prolog – Página 3

Reseña: Deriving a fast inverse of the generalized Cantor N-tupling bijection

PorJosé A. Alonso 30 agosto 20128 marzo 2013

La semana que viene (6 de septiembre) se presentará en el ICLP’12 (28th International Conference on Logic Programming) un trabajo sobre resolución lógica de problemas combinatorios titulado Deriving a fast inverse of the generalized Cantor N-tupling bijection.

Su autor es Paul Tarau (de la University of North Texas, Denton, Texas, USA).

Su resumen es

We attack an interesting open problem (an efficient algorithm to invert the generalized Cantor N-tupling bijection) and solve it through a sequence of equivalence preserving transformations of logic programs, that take advantage of unique strengths of this programming paradigm. An extension to set and multiset tuple encodings, as well as a simple application to a “fair-search” mechanism illustrate practical uses of our algorithms.

The code in the paper (a literate Prolog program, tested with SWI-Prolog and Lean Prolog) is available at http://logic.cse.unt.edu/tarau/research/2012/pcantor.pl.

Reseña: Logic + control: An example of program construction

PorJosé A. Alonso 28 agosto 20128 marzo 2013

Se ha publicado un trabajo sobre metodología de la programación en Prolog titulado Logic + control: An example of program construction.

Su autor es Wlodzimierz Drabent (de la Univ. de Linköping, Suecia).

El trabajo se presentará el 6 de Septiembre en el ICLP’12 (28th International Conference on Logic Programming).

Su resumen es

We present a Prolog program (the SAT solver of Howe and King) as a logic program with added control. The control consists of a selection rule (delays of Prolog) and pruning the search space. We construct the logic program together with proofs of its correctness and completeness, with respect to a formal specification. This is augmented by a proof of termination under any selection rule. Correctness and termination are inherited by the Prolog program, the change of selection rule preserves completeness. We prove that completeness is also preserved by one case of pruning; for the other an informal justification is presented.

For proving correctness we use a method, which should be well known but is often neglected. A contribution of this paper is a method for proving completeness. In particular we introduce a notion of semi-completeness, for which a local sufficient condition exists.

We compare the proof methods with declarative diagnosis (algorithmic debugging). We introduce a method of proving that a certain kind of pruning preserves completeness. We argue that the proof methods correspond to natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.

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).