Concolic testing is a well-known validation technique for imperative and object oriented programs. In a previous paper, we have introduced an adaptation of this technique to logic programming. At the heart of our fram...
详细信息
Concolic testing is a well-known validation technique for imperative and object oriented programs. In a previous paper, we have introduced an adaptation of this technique to logic programming. At the heart of our framework lies a specific procedure that we call "selective unification". It is used to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. In this paper, we show that the existing algorithm for selective unification is not complete in the presence of non-linear atoms. We then prove soundness and completeness for a restricted version of the problem where some atoms are required to be linear. We also consider concolic testing in the context of constraint logic programming and extend the notion of selective unification accordingly.
Learning Prolog is a challenge on many levels. In relation to other programming languages, it carries additional weight in understanding due to its declarative nature, which is significantly different in relation to p...
详细信息
ISBN:
(数字)9789532331035
ISBN:
(纸本)9781665484343
Learning Prolog is a challenge on many levels. In relation to other programming languages, it carries additional weight in understanding due to its declarative nature, which is significantly different in relation to procedural languages. Prolog is an extremely important programming language because it is the foundation of artificial intelligence, knowledge-based systems, and other modern systems. The question arises of how to motivate students in the best possible way and make it easier for them to understand Prolog. The literature points to problems in learning the language, but also to possible approaches to quality teaching. This paper describes five-year research on the quality of teaching based on the feedback from students at the end of the semester. The research is an analysis of contact teaching and online teaching in the last part. The results of the research show observed problems in understanding the SWI-Prolog, but also the efforts of teachers to try to alleviate the perceived problems of students in the best possible way. In this way, efforts were made to raise the quality of teaching from year to year, thus making it easier for students to understand and adopt the material related to the basics of the SWI-Prolog.
The generation of comprehensible explanations is an essential feature of modern artificial intelligence systems. In this work, we consider probabilistic logic programming, an extension of logic programming which can b...
详细信息
Traditional logic programs are written in some formal languages easy to “unify” each other or symbol based ones such as in Prolog, and their “NOT” mechanisms are “negation by failure of proof” according to “CLO...
详细信息
ISBN:
(纸本)9781665480468
Traditional logic programs are written in some formal languages easy to “unify” each other or symbol based ones such as in Prolog, and their “NOT” mechanisms are “negation by failure of proof” according to “CLOSED world assumption” and are not assumed as “true negation”*** the other hand, we suppose that BigData for moral, ethics and values are written originally in various different natural languages over the *** order for both human and AI to easily understand and automatically operate such BigData, we hope that (1) human could logic-program the contents of such Big-Data, by semi-dead-copying the original-natural-language-texts as "logic-programs" without hard translation, formalization and/or normalization,(2) “NOT”s in the language text that mean some TABOOs in any culture shall be operated correctly as such (not as “negataion by failure of proof”s but as the TABOOs) even in case of concretizing objects from different cultures, as in OPEN world assumption, because any TABOO from any one culture shall be rigidly respected, even during meetings between people from different cultures including the one culture with the *** the above purpose, this document explains a method of natural-language-based-logic-programming where variables for knowledge abstraction and concretization are embedded into the natural language texts, and also explains the above strong "TABOO-NOT" implementation therefor.
In this paper we present an alternative approach to formalize the theory of logic programming. In this formalization we allow existential quantified variables and equations in queries. In opposite to standard approach...
详细信息
Building Information Modeling (BIM) produces three-dimensional object-oriented models of buildings combining the geometrical information with a wide range of properties about materials, products, safety, to name just ...
详细信息
A good choice of the programming paradigm can reduce the required development effort. Nevertheless, today almost all industrial systems are developed using imperative or object-oriented approaches. In order to use the...
详细信息
We formalized renvoi in private international law in JURIX 2019 in terms of modal logic fragment. In this demonstration paper, we show an implementation of the formalism by translating modal formula into a logic program.
ISBN:
(纸本)9781643681511;9781643681504
We formalized renvoi in private international law in JURIX 2019 in terms of modal logic fragment. In this demonstration paper, we show an implementation of the formalism by translating modal formula into a logic program.
The semantic foundations for logic programming are usually separated into two different approaches. The operational semantics, which uses SLD-resolution, the proof method that computes answers in logic programming, an...
详细信息
作者：
Vidal, GermanMiST
VRAIN Universitat Politècnica de València Valencia Spain
In this work, we say that a computation is reversible if one can find a procedure to undo the steps of a standard (or forward) computation in a deterministic way. While logic programs are often invertible (e.g., one c...
详细信息
ISBN:
(纸本)9783030524814;9783030524821
In this work, we say that a computation is reversible if one can find a procedure to undo the steps of a standard (or forward) computation in a deterministic way. While logic programs are often invertible (e.g., one can use the same predicate for adding and for subtracting natural numbers), computations are not reversible in the above sense. In this paper, we present a so-called Landauer embedding for SLD resolution, the operational principle of logic programs, so that it becomes reversible. A proof-of-concept implementation of a reversible debugger for Prolog that follows the ideas in this paper has been developed and is publicly available.
暂无评论