作者：
Schulz, KatrinILLC
Department of Philosophy University of Amsterdam Netherlands
This article aims to propagate logic programming as a formal tool to deal with non-monotonic reasoning. In philosophy and linguistics non-monotonic reasoning is modelled using Minimal Models as standard, i.e., by impo...
详细信息
This study aimed to investigate the learning concepts of logic programming for high-school students introducing the arduino tool as a pedagogical strategy. therefore, the methodology applied initially consisted in pre...
详细信息
ISBN:
(纸本)9781479961115
This study aimed to investigate the learning concepts of logic programming for high-school students introducing the arduino tool as a pedagogical strategy. therefore, the methodology applied initially consisted in presencial classes, as well as the subsequent interaction with the tool and assessment activities. initial results indicate that this strategy was adequate for materialization of abstract concepts that are taught in logic programming, but it also allows one to identify formalization dificulties of mathematical concepts for solving activities that were proposed
A long-standing problem in logic programming is how to cleanly separate logic and control. While solutions exist, they fall short in one of two ways: some are too intrusive, because they require significant changes to...
详细信息
ISBN:
(纸本)9781450329477
A long-standing problem in logic programming is how to cleanly separate logic and control. While solutions exist, they fall short in one of two ways: some are too intrusive, because they require significant changes to Prolog's underlying implementation;others are lacking a clean semantic grounding. We resolve both of these issues in this paper. We derive a solution that is both lightweight and principled. We do so by starting from a functional specification of Prolog based on monads, and extend this with the effect handlers approach to capture the dynamic search tree as syntax. Effect handlers then express heuristics in terms of tree transformations. Moreover, we can declaratively express many heuristics as trees themselves that are combined with search problems using a generic entwining handler. Our solution is not restricted to a functional model: we show how to implement this technique as a library in Prolog by means of delimited continuations.
Caenorhabditis elegans vulval development is a paradigm system for understanding cell differentiation in the process of organogenesis. Through temporal and spatial controls, the fate pattern of six cells is determined...
详细信息
Caenorhabditis elegans vulval development is a paradigm system for understanding cell differentiation in the process of organogenesis. Through temporal and spatial controls, the fate pattern of six cells is determined by the competition of the LET-23 and the Notch signalling pathways. Modelling cell fate determination in vulval development using state-based models, coupled with formal analysis techniques, has been established as a powerful approach in predicting the outcome of combinations of mutations. However, computing the outcomes of complex and highly concurrent models can become prohibitive. Here, we show how logic programs derived from state machines describing the differentiation of C. elegans vulval precursor cells can increase the speed of prediction by four orders of magnitude relative to previous approaches. Moreover, this increase in speed allows us to infer, or 'retrodict', compatible genomes from cell fate patterns. We exploit this technique to predict highly variable cell fate patterns resulting from dig-1 reduced-function mutations and let-23 mosaics. In addition to the new insights offered, we propose our technique as a platform for aiding the design and analysis of experimental data.
Extensional higher-order logic programming has been recently proposed as an interesting extension of classical logic programming An important characteristic of the new paradigm is that it preserves all the well-known ...
详细信息
Extensional higher-order logic programming has been recently proposed as an interesting extension of classical logic programming An important characteristic of the new paradigm is that it preserves all the well-known properties of traditional logic programming In this paper we enhance extensional higher-order logic programming with constructive negation. We argue that the main ideas underlying constructive negation are quite close to the existing proof procedure for extensional higher-order logic programming and for this reason the two notions amalgamate quite conveniently. We demonstrate the soundness of the resulting proof procedure and describe an actual implementation of a language that embodies the above ideas. In this way we obtain the first (to our knowledge) higher-order logic programming language supporting constructive negation and offering a new style of programming that genuinely extends that of traditional logic programming.
We develop a model of abduction in abstract argumentation, where changes to an argumentation framework act as hypotheses to explain the support of an observation. We present dialogical proof theories for the main deci...
详细信息
ISBN:
(纸本)9781614994190;9781614994183
We develop a model of abduction in abstract argumentation, where changes to an argumentation framework act as hypotheses to explain the support of an observation. We present dialogical proof theories for the main decision problems (i.e., finding hypotheses that explain skeptical/credulous support) and we show that our model can be instantiated on the basis of abductive logic programs.
Stable models of logic programs have been studied and characterized in relation with other formalisms by many researchers. As already argued in previous papers, such characterizations are interesting for diverse reaso...
详细信息
Stable models of logic programs have been studied and characterized in relation with other formalisms by many researchers. As already argued in previous papers, such characterizations are interesting for diverse reasons, including theoretical investigations and the possibility of leading to new algorithms for computing stable models of logic programs. At the theoretical level, complexity and expressiveness comparisons have brought about fundamental insights. Beyond that, practical implementations of the developed reductions enable the use of existing solvers for other logical formalisms to compute stable models. In this paper, we first provide a simple characterization of stable models that can be viewed as a proof-theoretic counterpart of the standard model- theoretic definition. We further show how it can be naturally encoded in difference logic. Such an encoding, compared to the existing reductions to classical logics, does not require Boolean variables. Then, we implement our novel translation to a Satisfiability Modulo Theories (SMT) formula. We finally compare our approach, employing the SMT solver YICES, to the translation- based ASP solver LP2DIEE and to CLIvGo on domains from the "Basic Decision" track of the 2017 Answer Set programming competition. The results show that our approach is competitive to and often better than LP2DIEE, and that it can also be faster than CLIvGo on non-tight domains.
In recent years, the complexity of software systems has increased drastically. But methods for assuring their security by testing failed to keep up with this increased complexity. As a result, currently security testi...
详细信息
ISBN:
(纸本)9783319070766;9783319070759
In recent years, the complexity of software systems has increased drastically. But methods for assuring their security by testing failed to keep up with this increased complexity. As a result, currently security testing at the most is done by penetration testing, which lacks an underlying structured method. Thus, in this paper we propose an automated risk analysis by logic programming, whose results are valuable in doing structured security testing by additionally focusing on nonfunctional requirements, a main source for security bugs.
In ontology-based data access (OBDA), the classical database is enhanced with an ontology in the form of logical assertions generating new intensional knowledge. A powerful form of such logical assertions is the tuple...
详细信息
In ontology-based data access (OBDA), the classical database is enhanced with an ontology in the form of logical assertions generating new intensional knowledge. A powerful form of such logical assertions is the tuple-generating dependencies (TGDs), also called existential rules, where Horn rules are extended by allowing existential quantifiers to appear in the rule heads. In this paper, we introduce a new language called loop restricted (LR) TGDs (existential rules), which are TGDs with certain restrictions on the loops embedded in the underlying rule set. We study the complexity of this new language. We show that the conjunctive query answering (CQA) under the LR TGDs is decidable. In particular, we prove that this language satisfies the so-called bounded derivation-depth property (BDDP), which implies that the CQA is first-order rewritable, and its data complexity is in AC0. We also prove that the combined complexity of the CQA is 2-EXPTIME complete, while the language membership is PSPACE complete. Then we extend the LR TGDs language to the generalized loop restricted (GLR) TGDs language and prove that this class of TGDs still remains to be first-order rewritable and properly contains most of other first-order rewritable TGDs classes discovered in the literature so far.
Answer set programming (ASP) is a popular declarative programming language for solving hard combinatorial problems. Although ASP has gained widespread acceptance in academic and industrial contexts, there are certain ...
详细信息
Answer set programming (ASP) is a popular declarative programming language for solving hard combinatorial problems. Although ASP has gained widespread acceptance in academic and industrial contexts, there are certain user groups who may find it more advantageous to employ a higher-level language that closely resembles natural language when specifying ASP programs. In this paper, we propose a novel tool, called CNL2ASP, for translating English sentences expressed in a controlled natural language (CNL) form into ASP. In particular, we first provide a definition of the type of sentences allowed by our CNL and their translation as ASP rules and then exemplify the usage of the CNL for the specification of both synthetic and real-world combinatorial problems. Finally, we report the results of an experimental analysis conducted on the real-world problems to compare the performance of automatically generated encodings with the ones written by ASP practitioners, showing that our tool can obtain satisfactory performance on these benchmarks.
暂无评论