sld resolution
Recently Published Documents


TOTAL DOCUMENTS

28
(FIVE YEARS 0)

H-INDEX

7
(FIVE YEARS 0)

2020 ◽  
Vol 20 (6) ◽  
pp. 818-833 ◽  
Author(s):  
FRANCESCO DAGNINO ◽  
DAVIDE ANCONA ◽  
ELENA ZUCCA

AbstractRecursive definitions of predicates are usually interpreted either inductively or coinductively. Recently, a more powerful approach has been proposed, called flexible coinduction, to express a variety of intermediate interpretations, necessary in some cases to get the correct meaning. We provide a detailed formal account of an extension of logic programming supporting flexible coinduction. Syntactically, programs are enriched by coclauses, clauses with a special meaning used to tune the interpretation of predicates. As usual, the declarative semantics can be expressed as a fixed point which, however, is not necessarily the least, nor the greatest one, but is determined by the coclauses. Correspondingly, the operational semantics is a combination of standard SLD resolution and coSLD resolution. We prove that the operational semantics is sound and complete with respect to declarative semantics restricted to finite comodels.



2019 ◽  
Vol 109 (7) ◽  
pp. 1323-1369
Author(s):  
Andrew Cropper ◽  
Sophie Tourret

AbstractMany forms of inductive logic programming (ILP) use metarules, second-order Horn clauses, to define the structure of learnable programs and thus the hypothesis space. Deciding which metarules to use for a given learning task is a major open problem and is a trade-off between efficiency and expressivity: the hypothesis space grows given more metarules, so we wish to use fewer metarules, but if we use too few metarules then we lose expressivity. In this paper, we study whether fragments of metarules can be logically reduced to minimal finite subsets. We consider two traditional forms of logical reduction: subsumption and entailment. We also consider a new reduction technique called derivation reduction, which is based on SLD-resolution. We compute reduced sets of metarules for fragments relevant to ILP and theoretically show whether these reduced sets are reductions for more general infinite fragments. We experimentally compare learning with reduced sets of metarules on three domains: Michalski trains, string transformations, and game rules. In general, derivation reduced sets of metarules outperform subsumption and entailment reduced sets, both in terms of predictive accuracies and learning times.





Gödel '96 ◽  
2017 ◽  
pp. 257-266
Author(s):  
Leonard Paulík
Keyword(s):  


2016 ◽  
Vol 10 (3) ◽  
pp. 1-13
Author(s):  
Phan Dinh Dieu ◽  
Phan Hong Giang

This paper presents an approximate method for probabilistic entailment problem in knowledge bases where a portion of knowledge is given by a sentence in propositional logic accompanied with an interval presenting its truth probalibity. This method reduces the entailment problem to one  of finding “prime implicants” of the target sentence expressed through sentences in the  given knowledge base. It is  shown that in the case of probabilistic logic programs the set of such prime implicants can be found by using the SLD-resolution method for  usual definte 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.



2009 ◽  
Vol 225 ◽  
pp. 141-159 ◽  
Author(s):  
Ekaterina Komendantskaya ◽  
Anthony Karel Seda


2006 ◽  
Vol 6 (5) ◽  
pp. 509-538 ◽  
Author(s):  
LEE NAISH

This paper describes a simpler way for programmers to reason about the correctness of their code. The study of semantics of logic programs has shown strong links between the model theoretic semantics (truth and falsity of atoms in the programmer's interpretation of a program), procedural semantics (for example, SLD resolution) and fixpoint semantics (which is useful for program analysis and alternative execution mechanisms). Most of this work assumes that intended interpretations are two-valued: a ground atom is true (and should succeed according to the procedural semantics) or false (and should not succeed). In reality, intended interpretations are less precise. Programmers consider that some atoms “should not occur” or are “ill-typed” or “inadmissible”. Programmers don't know and don't care whether such atoms succeed. In this paper we propose a three-valued semantics for (essentially) pure Prolog programs with (ground) negation as failure which reflects this. The semantics of Fitting is similar but only associates the third truth value with non-termination. We provide tools to reason about correctness of programs without the need for unnatural precision or undue restrictions on programming style. As well as theoretical results, we provide a programmer-oriented synopsis. This work has come out of work on declarative debugging, where it has been recognised that inadmissible calls are important.



Sign in / Sign up

Export Citation Format

Share Document