scholarly journals ■ Logic Programming Paradigm

2013 ◽  
pp. 402-439
2007 ◽  
Vol 8 (01) ◽  
pp. 121-128 ◽  
Author(s):  
MICHAEL CODISH ◽  
VITALY LAGOON ◽  
PETER J. STUCKEY

AbstractThis paper presents a Prolog interface to the MiniSat satisfiability solver. Logic programming with satisfiability combines the strengths of the two paradigms: logic programming for encoding search problems into satisfiability on the one hand and efficient SAT solving on the other. This synergy between these two exposes a programming paradigm that we propose here as a logic programming pearl. To illustrate logic programming with SAT solving, we give an example Prolog program that solves instances of Partial MAXSAT.


1996 ◽  
Vol 11 (4) ◽  
pp. 333-345 ◽  
Author(s):  
Leon Sterling ◽  
Ümit Yalçinalp

AbstractLogic programming is a programming paradigm with potential to contribute to software engineering. This paper is concerned with one dimension of that potential, the impact that experience with developing logic programs can have on software design. We present a logic programming perspective on programming patterns, systematic program development, design for provability, and the paradigm of meta-programming.


2005 ◽  
Vol 5 (3) ◽  
pp. 305-354 ◽  
Author(s):  
GOPALAN NADATHUR

The logic programming paradigm provides the basis for a new intensional view of higher-order notions. This view is realized primarily by employing the terms of a typed lambda calculus as representational devices and by using a richer form of unification for probing their structures. These additions have important meta-programming applications but they also pose non-trivial implementation problems. One issue concerns the machine representation of lambda terms suitable to their intended use: an adequate encoding must facilitate comparison operations over terms in addition to supporting the usual reduction computation. Another aspect relates to the treatment of a unification operation that has a branching character and that sometimes calls for the delaying of the solution of unification problems. A final issue concerns the execution of goals whose structures become apparent only in the course of computation. These various problems are exposed in this paper and solutions to them are described. A satisfactory representation for lambda terms is developed by exploiting the nameless notation of de Bruijn as well as explicit encodings of substitutions. Special mechanisms are molded into the structure of traditional Prolog implementations to support branching in unification and carrying of unification problems over other computation steps; a premium is placed in this context on exploiting determinism and on emulating usual first-order behaviour. An extended compilation model is presented that treats higher-order unification and also handles dynamically emergent goals. The ideas described here have been employed in the Teyjus implementation of the $\lambda$Prolog language, a fact that is used to obtain a preliminary assessment of their efficacy.


2013 ◽  
Vol 10 (4) ◽  
pp. 1775-1797
Author(s):  
Miguel Areias ◽  
Ricardo Rocha

Logic Programming languages, such as Prolog, provide a highlevel, declarative approach to programming. Despite the power, flexibility and good performance that Prolog systems have achieved, some deficiencies in Prolog?s evaluation strategy - SLD resolution - limit the potential of the logic programming paradigm. Tabled evaluation is a recognized and powerful technique that overcomes SLD?s susceptibility in dealing with recursion and redundant sub-computations. In a tabled evaluation, there are several points where we may have to choose between different tabling operations. The decision on which operation to perform is determined by the scheduling algorithm. The two most successful tabling scheduling algorithms are local scheduling and batched scheduling. In previous work, we have developed a framework, on top of the Yap Prolog system, that supports the combination of different linear tabling strategies for local scheduling. In this work, we propose the extension of our framework to support batched scheduling. In particular, we are interested in the two most successful linear tabling strategies, the DRA and DRE strategies. To the best of our knowledge, no other Prolog system supports both strategies simultaneously for batched scheduling. Our experimental results show that the combination of the DRA and DRE strategies can effectively reduce the execution time for batched evaluation.


Sign in / Sign up

Export Citation Format

Share Document