We provide a framework for probabilistic reasoning in Vadalog-based Knowledge Graphs (KGs), satisfying the requirements of ontological reasoning: full recursion, powerful existential quantification, expression of indu...
详细信息
We provide a framework for probabilistic reasoning in Vadalog-based Knowledge Graphs (KGs), satisfying the requirements of ontological reasoning: full recursion, powerful existential quantification, expression of inductive definitions. Vadalog is a Knowledge Representation and Reasoning (KRR) language based on Warded Datalog+/-, a logical core language of existential rules, with a good balance between computational complexity and expressive power. Handling uncertainty is essential for reasoning with KGs. Yet Vadalog and Warded Datalog+/- are not covered by the existing probabilistic logicprogramming and statistical relational learning approaches for several reasons, including insufficient support for recursion with existential quantification and the impossibility to express inductive definitions. In this work, we introduce Soft Vadalog, a probabilistic extension to Vadalog, satisfying these desiderata. A Soft Vadalog program induces what we call a Probabilistic Knowledge Graph (PKG), which consists of a probability distribution on a network of chase instances, structures obtained by grounding the rules over a database using the chase procedure. We exploit PKGs for probabilistic marginal inference. We discuss the theory and present MCMC-chase, a Monte Carlo method to use Soft Vadalog in practice. We apply our framework to solve data management and industrial problems and experimentally evaluate it in the Vadalog system.
Answer set programming is a well-understood and established problem-solving and knowledge representation paradigm. It has become more prominent amongst a wider audience due to its multiple applications in science and ...
详细信息
Answer set programming is a well-understood and established problem-solving and knowledge representation paradigm. It has become more prominent amongst a wider audience due to its multiple applications in science and industry. The constant development of advanced programming and modeling techniques extends the toolset for developers and users regularly. This paper compiles and demonstrates different techniques to reuse logic program parts (multi-shot) by solving the arcade game snake. This game is particularly interesting because a victory can be assured by solving the NP-hard problem of Hamiltonian Cycles. We will demonstrate five hands-on implementations in clingo and compare their performance in an empirical evaluation. In addition, our implementation utilizes clingraph to generate a simple yet informative image representation of the game's progress.
In this survey, we present an overview on (Modal) Temporal logicprogramming in view of its application to Knowledge Representation and Declarative Problem Solving. The syntax of this extension of logic programs is th...
详细信息
In this survey, we present an overview on (Modal) Temporal logicprogramming in view of its application to Knowledge Representation and Declarative Problem Solving. The syntax of this extension of logic programs is the result of combining usual rules with temporal modal operators, as in Linear-time Temporal logic (LTL). In the paper, we focus on the main recent results of the non-monotonic formalism called Temporal Equilibrium logic (TEL) that is defined for the full syntax of LTL but involves a model selection criterion based on Equilibrium logic, a well known logical characterization of Answer Set programming (ASP). As a result, we obtain a proper extension of the stable models semantics for the general case of temporal formulas in the syntax of LTL. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between finite and infinite trace length. We also provide further useful results, such as the translation into other formalisms like Quantified Equilibrium logic and Second-order LTL, and some techniques for computing temporal stable models based on automata constructions. In the remainder of the paper, we focus on practical aspects, defining a syntactic fragment called (modal) temporal logic programs closer to ASP, and explaining how this has been exploited in the construction of the solver telingo, a temporal extension of the well-known ASP solver clingo that uses its incremental solving capabilities.
This paper presents a rich knowledge representation language aimed at formalizing causal knowledge. This language is used for accurately and directly formalizing common benchmark examples from the literature of actual...
详细信息
This paper presents a rich knowledge representation language aimed at formalizing causal knowledge. This language is used for accurately and directly formalizing common benchmark examples from the literature of actual causality. A definition of cause is presented and used to analyze the actual causes of changes with respect to sequences of actions representing those examples.
This paper describes a generalization of Clark's completion that is applicable to logic programs containing arithmetic operations and produces syntactically simple, natural looking formulas. If a set of first-orde...
详细信息
This paper describes a generalization of Clark's completion that is applicable to logic programs containing arithmetic operations and produces syntactically simple, natural looking formulas. If a set of first-order axioms is equivalent to the completion of a program, then we may be able to find standard models of these axioms by running an answer set solver. As an example, we apply this "reverse completion" procedure to the Sum and Product Puzzle.
Automatic differentiation (AD) is a range of algorithms to compute the numeric value of a function's (partial) derivative, where the function is typically given as a computer program or abstract syntax tree. AD ha...
详细信息
Automatic differentiation (AD) is a range of algorithms to compute the numeric value of a function's (partial) derivative, where the function is typically given as a computer program or abstract syntax tree. AD has become immensely popular as part of many learning algorithms, notably for neural networks. This paper uses Prolog to systematically derive gradient-based forward- and reverse-mode AD variants from a simple executable specification: evaluation of the symbolic derivative. Along the way we demonstrate that several Prolog features (DCGs, co-routines) contribute to the succinct formulation of the algorithm. We also discuss two applications in probabilistic programming that are enabled by our Prolog algorithms. The first is parameter learning for the Sum-Product Loop Language and the second consists of both parameter learning and variational inference for probabilistic logicprogramming.
Specifying and implementing a proof system from scratch requires significant effort. logical Frameworks and Higher Order logicprogramming Languages provide dedicated, high-level meta languages to facilitate this task...
详细信息
ISBN:
(纸本)9798400709692
Specifying and implementing a proof system from scratch requires significant effort. logical Frameworks and Higher Order logicprogramming Languages provide dedicated, high-level meta languages to facilitate this task in two ways: 1) variable binding and substitution are for free when meta language binders represent object logic ones;2) proof construction, and proof search, are greatly simplified by leveraging the unification procedure provided by the meta language. Notable examples of meta languages are Elf [21], Twelf [23], lambda Prolog [16], Beluga [24], Abella [8] and Isabelle [31] which have been used to implement or specify many formal systems such as First Order logic [5], Set theory [20], Higher Order logic [19], and the Calculus of Constructions [4]. The object logic we are interested in is Coq's type theory [28]. We aim to develop a higher-order unification-based proof search procedure using the meta language Elpi [3], a dialect of lambda Prolog. Elpi's equational theory includes beta eta-equivalence and features a higher-order unification procedure similar or equal to(m) for the pattern fragment [15]. Elpi offers an encoding of Coq terms that is suitable for meta programming [6, 9, 26, 27] but that restricts similar or equal to(m) to first-order unification problems only. We refer to this basic encoding as O. In this paper we translate unification problems in O to an alternative encoding called M, from which we derive similar or equal to(O), the higher-order unification procedure of O. similar or equal to(O) honours beta eta-equivalence for terms within the pattern fragment, and allows for the use of heuristics when the terms fall outside the pattern fragment. Moreover, as similar or equal to(O) delegates most of the work to similar or equal to(m), it can be used to efficiently simulate a logic program in O by taking advantage of unification-related optimizations of the meta language, such as clause indexing.
logicprogramming is a flexible programming paradigm due to the use of predicates without a fixed data flow. To extend logic languages with the compact notation of functional programming, there are various proposals t...
详细信息
logicprogramming is a flexible programming paradigm due to the use of predicates without a fixed data flow. To extend logic languages with the compact notation of functional programming, there are various proposals to map evaluable functions into predicates in order to stay in the logicprogramming framework. Since amalgamated functional logic languages offer flexible as well as efficient evaluation strategies, we propose an opposite approach in this paper. By mapping logic programs into functional logic programs with a transformation based on inferring functional dependencies, we develop a fully automatic transformation which keeps the flexibility of logicprogramming but can improve computations by reducing infinite search spaces to finite ones.
As the popularity of adhesive joints in industry increases, so does the need for tools to support the process of selecting a suitable adhesive. While some such tools already exist, they are either too limited in scope...
详细信息
As the popularity of adhesive joints in industry increases, so does the need for tools to support the process of selecting a suitable adhesive. While some such tools already exist, they are either too limited in scope or offer too little flexibility in use. This work presents a more advanced tool, that was developed together with a team of adhesive experts. We first extract the experts' knowledge about this domain and formalize it in a Knowledge Base (KB). The IDP-Z3 reasoning system can then be used to derive the necessary functionality from this KB. Together with a user-friendly interactive interface, this creates an easy-to-use tool capable of assisting the adhesive experts. To validate our approach, we performed user testing in the form of qualitative interviews. The experts are very positive about the tool, stating that, among others, it will help save time and find more suitable adhesives.
Argumentation problems are concerned with determining the acceptability of a set of arguments from their relational structure. When the available information is uncertain, probabilistic argumentation frameworks provid...
详细信息
Argumentation problems are concerned with determining the acceptability of a set of arguments from their relational structure. When the available information is uncertain, probabilistic argumentation frameworks provide modeling tools to account for it. The first contribution of this paper is a novel interpretation of probabilistic argumentation frameworks as probabilistic logic programs. Probabilistic logic programs are logic programs in which some of the facts are annotated with probabilities. We show that the programs representing probabilistic argumentation frameworks do not satisfy a common assumption in probabilistic logicprogramming (PLP) semantics, which is, that probabilistic facts fully capture the uncertainty in the domain under investigation. The second contribution of this paper is then a novel PLP semantics for programs where a choice of probabilistic facts does not uniquely determine the truth assignment of the logical atoms. The third contribution of this paper is the implementation of a PLP system supporting this semantics: smProbLog. smProbLog is a novel PLP framework based on the PLP language ProbLog. smProbLog supports many inference and learning tasks typical of PLP, which, together with our first contribution, provide novel reasoning tools for probabilistic argumentation. We evaluate our approach with experiments analyzing the computational cost of the proposed algorithms and their application to a dataset of argumentation problems.
暂无评论