scholarly journals Batched evaluation of linear tabled logic programs

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.

Author(s):  
GRIGORIS ANTONIOU

A modularity concept for structuring and developing large logic programs and logical knowledge bases is presented. The concept is motivated from work in the field of algebraic specification, and enforces an extreme modularity discipline that goes beyond the one found in imperative or logic programming languages. As concrete programming languages (respectively knowledge representation formalisms), we consider Horn logic and equational logic programming. We give formal semantics for single modules and discuss correctness and verification issues. Large systems are constructed as interconnections of single modules. We introduce the so-called module operations of composition, actualization, and union, and give results concerning compositionality of semantics and correctness preservation.


2004 ◽  
Vol 15 (02) ◽  
pp. 417-443 ◽  
Author(s):  
MANOLIS GERGATSOULIS ◽  
CHRISTOS NOMIKOS

In this paper, we propose a new resolution proof procedure for the branching-time logic programming language Cactus. The particular strength of the new proof procedure, called CSLD-resolution, is that it can handle, in a more general way, open-ended queries, i.e. goal clauses that include atoms which do not refer to specific moments in time, without the need of enumerating all their canonical instances. We also prove soundness, completeness and independence of the computation rule for CSLD-resolution. The new proof procedure overcomes the limitations of a family of proof procedures for temporal logic programming languages, which were based on the notions of canonical program and goal clauses. Moreover, it applies directly to Chronolog programs and it can be easily extended to apply to multi-dimensional logic programs as well as to Chronolog(MC) programs.


2020 ◽  
Author(s):  
Paulo Garcia ◽  
Josh Fryer

<div>The shift towards reconfigurable systems -hardware</div><div>and software that adapt themselves to an external context-</div><div>promises to unlock unprecedented performance, power consumption, and quality of service. However, reconfiguration imposes several challenges on the design of cyber-physical systems. Current design practices, including software frameworks and programming languages, are ill-prepared for supporting reconfiguration.</div><div>In this paper, we explore Asynchronous Graph Programming, a programming paradigm and an associated model of computation designed for efficient and automated parallelization across processing elements, efficient reconfiguration (i.e., mapping of computational tasks across processing elements), and combining synchronous and asynchronous I/O handling within the same conceptual programming model. We also introduce an analytical model of parallelization, unlocked by Asynchronous Graph Programming, that can inform reconfiguration strategies.</div><div>We analyze the implications of our model through an analysis of reconfiguration scenarios given a program’s characteristics; our analysis quantifies the benefits of reconfiguring software for higher levels of parallelism, given an amount of data left to process. We also introduce Horde, an open source Asynchronous Graph Programming interpreter, and use it to empirically validate the performance advantage of its automatic parallelism capabilities; in our experiments, automatic parallelization from one to four cores improves average case execution time by a factor of 2 and worst case execution time by a factor of 3.</div><div><br></div><div>This manuscript has been accepted at the IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2020)</div><div><br></div>


Author(s):  
James D. Jones

Knowledge representation is a field of artificial intelligence that has been actively pursued since the 1940s.1 The issues at stake are that given a specific domain, how do we represent knowledge in that domain, and how do we reason about that domain? This issue of knowledge representation is of paramount importance, since the knowledge representation scheme may foster or hinder reasoning. The representation scheme can enable reasoning to take place, or it may make the desired reasoning impossible. To some extent, the knowledge representation depends upon the underlying technology. For instance, in order to perform default reasoning with exceptions, one needs weak negation (aka negation as failure. In fact, most complex forms of reasoning will require weak negation. This is a facility that is an integral part of logic programs but is lacking from expert system shells. Many Prolog implementations provide negation as failure, however, they do not understand nor implement the proper semantics. The companion article to this article in this volume, “Logic Programming Languages for Expert Systems,” discusses logic programming and negation as failure.


Formal logic is widely accepted as a program specification language in computing science. It is ideally suited to the representation of knowledge and the description of problems without regard to the choice of programming language. Its use as a specification language is compatible not only with conventional programming languages but also with programming languages based entirely on logic itself. In this paper I shall investigate the relation that holds when both programs and program specifications are expressed in formal logic. In many cases, when a specification completely defines the relations to be computed, there is no syntactic distinction between specification and program. Moreover the same mechanism that is used to execute logic programs, namely automated deduction, can also be used to execute logic specifications. Thus all relations defined by complete specifications are executable. The only difference between a complete specification and a program is one of efficiency. A program is more efficient than a specification.


2020 ◽  
Author(s):  
Paulo Garcia ◽  
Josh Fryer

<div>The shift towards reconfigurable systems -hardware</div><div>and software that adapt themselves to an external context-</div><div>promises to unlock unprecedented performance, power consumption, and quality of service. However, reconfiguration imposes several challenges on the design of cyber-physical systems. Current design practices, including software frameworks and programming languages, are ill-prepared for supporting reconfiguration.</div><div>In this paper, we explore Asynchronous Graph Programming, a programming paradigm and an associated model of computation designed for efficient and automated parallelization across processing elements, efficient reconfiguration (i.e., mapping of computational tasks across processing elements), and combining synchronous and asynchronous I/O handling within the same conceptual programming model. We also introduce an analytical model of parallelization, unlocked by Asynchronous Graph Programming, that can inform reconfiguration strategies.</div><div>We analyze the implications of our model through an analysis of reconfiguration scenarios given a program’s characteristics; our analysis quantifies the benefits of reconfiguring software for higher levels of parallelism, given an amount of data left to process. We also introduce Horde, an open source Asynchronous Graph Programming interpreter, and use it to empirically validate the performance advantage of its automatic parallelism capabilities; in our experiments, automatic parallelization from one to four cores improves average case execution time by a factor of 2 and worst case execution time by a factor of 3.</div><div><br></div><div>This manuscript has been accepted at the IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2020)</div><div><br></div>


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.


2014 ◽  
Author(s):  
Χρυσίδα Γαλανάκη

Η διατριβή επικεντρώνεται στη μελέτη της σημασιολογίας λογικών προγραμμάτων και την ανάπτυξη άπειρων παιγνίων πλήρους πληροφόρησης που αποδίδουν αυτή τη σημασιολογία. Αρχικώς, μελετάται ο προτασιακός λογικός προγραμματισμός. Στο άρθρο [M.H. van Emden, Quantitative deduction and its fixpoint theory, Journal of Logic Programming 3(1)(1986) 37-53] περιγράφεται ένα παίγνιο μεταξύ δύο παικτών. Σε αυτό, δεδομένου ενός προτασιακού λογικού προγράμματος χωρίς άρνηση και ενός ατόμου (ground atom) που ανήκει σε αυτό, ο Παίκτης Ι, προσπαθεί να αποδείξει ότι ο ατομικός τύπος είναι αληθής (έχει δηλαδή το ρόλο του Believer), ενώ ο Παίκτης ΙΙ ότι δεν είναι (έχει δηλαδή το ρόλο του Doubter). Έτσι ο στόχος (goal), επιτυγχάνει ως αποτέλεσμα μιας ερώτησης (query) στο πρόγραμμα, αν ο Παίκτης Ι έχει νικηφόρα στρατηγική. Στα πλαίσια της διατριβής, το παίγνιο επεκτείνεται έτσι ώστε να αποδίδει τη σημασιολογία και των προγραμμάτων με άρνηση. Όταν κατά τη διάρκεια του παιχνιδιού εμφανίζεται αρνητικά προσημασμένο άτομο, τότε οι δύο παίκτες αλλάζουν τους μεταξύ τους ρόλους. Ο Believer γίνεται Doubter και το αντίστροφο. Στην περίπτωση άπειρων εναλλαγών ρόλων το παιχνίδι θεωρείται ισόπαλο. Αποδεικνύεται ότι το παίγνιο είναι αποφασισμένο (determined). Στην περίπτωση του παιχνιδιού με τρία δυνατά αποτελέσματα, η ερμηνεία του προγράμματος, η οποία λαμβάνεται χρησιμοποιώντας το παιχνίδι, αποτελεί μοντέλο του και αποδεικνύεται ισοδύναμη με την καλώς θεμελιωμένη σημασιολογία (well-founded semantics) του λογικού προγράμματος. Για την απόδειξη αυτή ορίζεται και χρησιμοποιείται ένα νέο παίγνιο με άπειρα δυνατά αποτελέσματα. Η τιμή του παιχνιδιού εξαρτάται από το πλήθος των εναλλαγών ρόλων (role switches) που λαμβάνουν χώρα κατά τη διάρκειά του. Η ερμηνεία που παίρνουμε χρησιμοποιώντας το παίγνιο αυτό, αποτελεί μοντέλο του λογικού προγράμματος και αποδεικνύεται ισοδύναμη με την απειρότιμη σημασιολογία ελαχίστου μοντέλου, όπως αυτή ορίζεται στο [P. Rondogiannis, W.W.Wadge, Minimum model semantics for logic programs with negation-as-failure, ACM Transactions on Computational Logic 6(2)(2005) 441-467]. Η μελέτη επεκτείνεται στον νοηματικό (intensional) λογικό προγραμματισμό όπως παρουσιαζεται στο [M.A. Orgun, W.W.Wadge, Towards a unified theory of intensional logic programming, 13(4):413-440, 1992] και αποτελεί γενίκευση, μεταξύ άλλων, του χρονικού (temporal) και τροπικού (modal) λογικού προγραμματισμού. Στα πλαίσια της διατριβής αναπτύσσεται ένα νέο παίγνιο πλήρους πληροφόρησης. Και για αυτό, αποδεικνύεται ότι είναι αποφασισμένο (determined) και ότι το αποτέλεσμά του συμπίπτει με τη σημασιολογία ελαχίστου μοντέλου του άρθρου των M.A. Orgun, W.W. Wadge. Στη συνέχεια το παίγνιο επεκτείνεται έτσι ώστε να υποστηρίζει εναλλαγή ρόλων μεταξύ των παικτών και να έχει τρία δυνατά αποτελέσματα (νίκη για τον Παίκτη Ι ή τον Παίκτη ΙΙ ή ισοπαλία). Η ερμηνεία την οποία παίρνουμε χρησιμοποιώντας το παιχνίδι, αποτελεί ελαχιστικό μοντέλο του προγράμματος και αποδίδει τη σημασιολογία νοηματικών λογικών προγραμμάτων με άρνηση και γενικότερα των νοηματικών λογικών προγραμμάτων με οποιoδήποτε μη μονοτονικό τελεστή στο σώμα των κανόνων. Η παιγνιοθεωρητική αυτή προσέγγιση αποτελεί και το πρώτο σημασιολογικό πλαίσιο για τον μη μονοτονικό νοηματικό (intensional) λογικό προγραμματισμό.


2012 ◽  
Vol 12 (4-5) ◽  
pp. 639-657 ◽  
Author(s):  
ILIANO CERVESATO

AbstractIn prior work, we showed that logic programming compilation can be given a proof-theoretic justification for generic abstract logic programming languages, and demonstrated this technique in the case of hereditary Harrop formulas and their linear variant. Compiled clauses were themselves logic formulas except for the presence of a second-order abstraction over the atomic goals matching their head. In this paper, we revisit our previous results into a more detailed and fully logical justification that does away with this spurious abstraction. We then refine the resulting technique to support well-moded programs efficiently.


2001 ◽  
Vol 1 (6) ◽  
pp. 647-690 ◽  
Author(s):  
Roberto Bruni ◽  
Ugo Montanari ◽  
Francesca Rossi

We apply to logic programming some recently emerging ideas from the field of reductionbased communicating systems, with the aim of giving evidence of the hidden interactions and the coordination mechanisms that rule the operational machinery of such a programming paradigm. The semantic framework we have chosen for presenting our results is tile logic, which has the advantage of allowing a uniform treatment of goals and observations and of applying abstract categorical tools for proving the results. As main contributions, we mention the finitary presentation of abstract unification, and a concurrent and coordinated abstract semantics consistent with the most common semantics of logic programming. Moreover, the compositionality of the tile semantics is guaranteed by standard results, as it reduces to check that the tile systems associated to logic programs enjoy the tile decomposition property. An extension of the approach for handling constraint systems is also discussed.


Sign in / Sign up

Export Citation Format

Share Document