Wyniki wyszukiwania - BazTech

1

Selective Unification in (Constraint) Logic Programming

Mesnard Fred, Payet Étienne, Vidal Germán

Fundamenta Informaticae

|

2020

|

Vol. 177, nr 3/4

359--383

EN

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.

2

lpopt : A Rule Optimization Tool for Answer Set Programming

Bichler Manuel, Morak Michael, Woltran Stefan

Fundamenta Informaticae

|

2020

|

Vol. 177, nr 3/4

275--296

EN

State-of-the-art answer set programming (ASP) solvers rely on a program called a grounder to convert non-ground programs containing variables into variable-free, propositional programs. The size of this grounding depends heavily on the size of the non-ground rules, and thus, reducing the size of such rules is a promising approach to improve solving performance. To this end, in this paper we announce lpopt, a tool that decomposes large logic programming rules into smaller rules that are easier to handle for current solvers. The tool is specifically tailored to handle the standard syntax of the ASP language (ASP-Core) and makes it easier for users to write efficient and intuitive ASP programs, which would otherwise often require significant hand-tuning by expert ASP engineers. It is based on an idea proposed by Morak and Woltran (2012) that we extend significantly in order to handle the full ASP syntax, including complex constructs like aggregates, weak constraints, and arithmetic expressions. We present the algorithm, the theoretical foundations on how to treat these constructs, as well as an experimental evaluation showing the viability of our approach.

3

Justifications in Constraint Handling Rules for Logical Retraction in Dynamic Algorithms : Theory, Implementations, and Complexity

Frühwirth Thom

Fundamenta Informaticae

|

2020

|

Vol. 173, nr 4

253--283

EN

We present a concise source-to-source transformation that introduces justifications for user-defined constraints into the rule-based Constraint Handling Rules (CHR) programming language. There is no need to introduce a new semantics for justifications. This leads to a conservative extension of the language, as we can show the equivalence of rule applications. A scheme of two rules suffices to allow for logical retraction (deletion, removal) of CHR constraints during computation. Without the need to recompute from scratch, these rules remove the constraint and also undo all its consequences. We prove a confluence result concerning the rule scheme. We prove its correctness in general and tighten the results for confluent programs. We give an implementation, show its correctness, present two classical examples of dynamic algorithms, and improve the implementation. The computational overhead of introducing justifications and of performing logical retraction, i.e. the additional time and space needed, is proportional to the derivation length in the original program. This overhead may increase space complexity, but does not change the worst-case time complexity.

4

Reasoning on Datalog± Ontologies with Abductive Logic Programming

Gavanelli M., Lamma E., Riguzzi F., Bellodi E., Zese R., Cota G.

Fundamenta Informaticae

|

2018

|

Vol. 159, nr 1/2

65--93

EN

Ontologies form the basis of the Semantic Web. Description Logics (DLs) are often the languages of choice for modeling ontologies. Integration of DLs with rules and rule-based reasoning is crucial in the so-called Semantic Web stack vision - a complete stack of recommendations and languages each based on and/or exploiting the underlying layers - which adds new features to the standards used in the Web. The growing importance of the integration between DLs and rules is proved by the definition of the profile OWL 2 RL1 and the definition of languages such as RIF2 and SWRL3. Datalog± is an extension of Datalog which can be used for representing lightweight ontologies and expressing some languages of the DL-Lite family, with tractable query answering under certain language restrictions. In particular, it is able to express the DL-Lite version defined in OWL. In this work, we show that Abductive Logic Programming (ALP) can be used to represent Datalog± ontologies, supporting query answering through an abductive proof procedure, and smoothly achieving the integration of ontologies and rule-based reasoning. Often, reasoning with DLs means finding explanations for the truth of queries, that are useful when debugging ontologies and to understand answers given by the reasoning process. We show that reasoning under existential rules can be expressed by ALP languages and we present a solving system, which is experimentally proved to be competitive with DL reasoning systems. In particular, we consider an ALP framework named SCIFF derived from the IFF abductive framework. Forward and backward reasoning is naturally supported in this ALP framework. The SCIFF language smoothly supports the integration of rules, expressed in a Logic Programming language, with Datalog± ontologies, mapped into SCIFF (forward) integrity constraints. The main advantage is that this integration is achieved within a single language, grounded on abduction in computational logic, and able to model existential rules.

5

From Constructivism to Logic Programming : an Homage to Mario Ornaghi

Ferrari M., Fiorentini C., Momigliano A.

Fundamenta Informaticae

|

2018

|

Vol. 161, nr 1/2

1--7

EN

In this brief note, we outline Mario Ornaghi’s contributions to the field of computational logic to celebrate his 70th birthday.

6

Extending Logic Programming with Labelled Variables : Model and Semantics

Calegari R., Denti E., Dovier A., Omicini A.

Fundamenta Informaticae

|

2018

|

Vol. 161, nr 1/2

53--74

EN

In order to enable logic programming to deal with the diversity of pervasive systems, where many heterogeneous, domain-specific computational models could benefit from the power of symbolic computation, we explore the expressive power of labelled systems. To this end, we define a new notion of truth for logic programs extended with labelled variables interpreted in non-Herbrand domains-where, however, terms maintain their usual Herbrand interpretations. First, a model for labelled variables in logic programming is defined. Then, the fixpoint and the operational semantics are presented and their equivalence is formally proved. A meta-interpreter implementing the operational semantics is also introduced, followed by some case studies aimed at showing the effectiveness of our approach in selected scenarios.

7

Towards Deriving Conclusions from Cause-effect Relations

Fandinno J.

Fundamenta Informaticae

|

2016

|

Vol. 147, nr 1

93--131

EN

In this work we propose an extension of logic programming, under the stable model semantics, and the action language BC where rule bodies and causal laws may contain a new kind of literal, that we call causal literal, that allows us to inspect the causal justifications of standard atoms. To this aim, we extend a recently proposed semantics where each atom belonging to a stable model is associated with a justification in the form of an algebraic expression (which corresponds to a logical proof built with rule labels). In particular, we use causal literals for evaluating and deriving new conclusions from statements like "A has been sufficient to cause B." We also use the proposed semantics to extend the action language BC with causal literals and, by some examples, show how this action language is useful for expressing a high level representation of some typical Knowledge Representation examples involving causal knowledge.

8

Shift Design with Answer Set Programming

Abseher M., Musliu N., Woltran S., Gebser M., Schaub T.

Fundamenta Informaticae

|

2016

|

Vol. 147, nr 1

1--25

EN

Answer Set Programming (ASP) is a powerful declarative programming paradigm that has been successfully applied to many different domains. Recently, ASP has also proved successful for hard optimization problems like course timetabling and travel allotment. In this paper, we approach another important task, namely, the shift design problem, aiming at an alignment of a minimum number of shifts in order to meet required numbers of employees (which typically vary for different time periods) in such a way that over- and understaffing is minimized. We provide an ASP encoding of the shift design problem, which, to the best of our knowledge, has not been addressed by ASP yet. Our experimental results demonstrate that ASP is capable of improving the best known solutions to some benchmark problems. Other instances remain challenging and make the shift design problem an interesting benchmark for ASP-based optimization methods.

9

Logic Programming with Graded Introspection

Zhang Z., Wang B., Zhang S.

Fundamenta Informaticae

|

2016

|

Vol. 147, nr 1

133--158

EN

This paper develops a logic programming language, GI-log, that extends answer set programming language with a new graded modality Kω where ω is an interval satisfying ω ⊆ [0; 1]. The modality is used to precede a literal in rules bodies, and thus allows for the representation of graded introspections in the presence of multiple belief sets: KωF intuitively means: it is known that the proportion of the belief sets where F is true is in the interval ω. We define the semantics of GI-log, study the relation to the languages of strong introspections, give an algorithm for computing solutions of GI-log programs, and investigate the use of GI-log for formalizing contextual reasoning, conformant planning with threshold, and modeling a graph problem.

10

Answer Set Programming Modulo Acyclicity

Bomanson J., Janhunen T., Schaub T., Gebser M., Kaufmann B.

Fundamenta Informaticae

|

2016

|

Vol. 147, nr 1

63--91

EN

Acyclicity constraints are prevalent in knowledge representation and applications where acyclic data structures such as DAGs and trees play a role. Recently, such constraints have been considered in the satisfiability modulo theories (SMT) framework, and in this paper we carry out an analogous extension to the answer set programming (ASP) paradigm. The resulting formalism, ASP modulo acyclicity, offers a rich set of primitives to express constraints related to recursive structures. In the technical results of the paper, we relate the new generalization with standard ASP by showing (i) how acyclicity extensions translate into normal rules, (ii) how weight constraint programs can be instrumented by acyclicity extensions to capture stability in analogy to unfounded set checking, and (iii) how the gap between supported and stable models is effectively closed in the presence of such an extension. Moreover, we present an efficient implementation of acyclicity constraints by incorporating a respective propagator into the stateof- the-art ASP solver CLASP. The implementation provides a unique combination of traditional unfounded set checking with acyclicity propagation. In the experimental part, we evaluate the interplay of these orthogonal checks by equipping logic programs with supplementary acyclicity constraints. The performance results show that native support for acyclicity constraints is a worthwhile addition, furnishing a complementary modeling construct in ASP itself as well as effective means for translation-based ASP solving.

11

A Theoretical Perspective of Coinductive Logic Programming

Ancona D., Dovier A.

Fundamenta Informaticae

|

2015

|

Vol. 140, nr 3/4

221--246

EN

In this paper we study the semantics of Coinductive Logic Programming and clarify its intrinsic computational limits, which prevent, in particular, the definition of a complete, computable, operational semantics. We propose a new operational semantics that allows a simple correctness result and the definition of a simple meta-interpreter. We compare, and prove the equivalence, with the operational semantics defined and used in other papers on this topic.

12

A Rule-based Verification Strategy for Array Manipulating Programs

De Angelis E., Fioravanti F., Pettorossi A., Proietti M.

Fundamenta Informaticae

|

2015

|

Vol. 140, nr 3/4

329--355

EN

We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {ϕ} prog {ψ} that defines a partial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect defined by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T . The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.

13

The CHR-based Implementation of the SCIFF Abductive System

Alberti M., Gavanelli M., Lamma E.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 4

365--381

EN

Abduction is a form of inference that supports hypothetical reasoning and has been applied to a number of domains, such as diagnosis, planning, protocol verification. Abductive Logic Programming (ALP) is the integration of abduction in logic programming. Usually, the operational semantics of an ALP language is defined as a proof procedure. The first implementations of ALP proof-procedures were based on the meta-interpretation technique, which is flexible but limits the use of the built-in predicates of logic programming systems. Another, more recent, approach exploits theoretical results on the similarity between abducibles and constraints. With this approach, which bears the advantage of an easy integration with built-in predicates and constraints, Constraint Handling Rules has been the language of choice for the implementation of abductive proof procedures. The first CHR-based implementation mapped integrity constraints directly to CHR rules, which is an efficient solution, but prevents defined predicates from being in the body of integrity constraints and does not allow a sound treatment of negation by default. In this paper, we describe the CHR-based implementation of the SCIFF abductive proof-procedure, which follows a different approach. The SCIFF implementation maps integrity constraints to CHR constraints, and the transitions of the proof-procedure to CHR rules, making it possible to treat default negation, while retaining the other advantages of CHR-based implementations of ALP proof-procedures.

14

Logic programming tools for formal software specification

Przymusińska H.

Zeszyty Naukowe Warszawskiej Wyższej Szkoły Informatyki

|

2011

|

nr 6

67--73

EN

Two of the most important problems in software engineering are the problem of elaborating and refining software requirements into accurate specifications, and the problem of transforming specifications of complicated problems into executable code. Proving that software products produced agree with the specifications (verifiability) is the main reason for pursuing the study of formal specifications.

PL

Jednym z najistotniejszych problemów w inżynierii oprogramowania jest opracowanie i zawężenie wymagań dotyczących oprogramowania w celu określenia dokładnych specyfikacji, a także kwestia przekształcenia specyfikacji dotyczących złożonych problemów w wykonywalne kody. Głównym powodem podjęcia się badania formalnych specyfikacji jest udowodnienie, że oprogramowanie produkowane jest z nimi zgodne (chodzi o weryfikowalność). Artykuł ukazuje, iż programowanie logiczne połączone z rachunkiem sytuacyjnym można z powodzeniem stosować jako formalną specyfikację oprogramowania.

15

Modeling fuzzy intervals with constraint logic programming

Kobylański P.

Prace Naukowe Politechniki Warszawskiej. Elektronika

|

2008

|

z. 165

9-22

EN

In this paper the method of modeling fuzzy intervals in fuzzy decision-making is presented. Described method makes use of constraint logic programming and it is based on the concept of descriptors. This approach is very general and it is consistent with Zadeh's extension principle and Bellman-Zadeh concept of fuzzy decision making. It fulfills Klir's requisite constraint and deals effectively with a drowning effect too. The idea of descriptors of fuzzy intervals and fuzzy constraints is illustrated with computational example of flexible scheduling problem in which robust for drowning effect schedule is found.

16

Programowanie w logice ograniczeniami do zarządzania w środowisku wieloprojektowym

Skołud B., Zientek A.

Zeszyty Naukowe. Mechanika / Politechnika Śląska

|

2005

|

z. 152

173-158

PL

W pracy podejmuje się próbę zdefiniowania ograniczeń zawężających liczbę projektów możliwych do współbieżnej realizacji. Przedstawiona została alternatywna metoda zapisu zajętości zasobów. Kolejność analizowania ograniczeń limitujących liczbę projektów przeprowadzona jest na podstawie Teorii Ograniczeń, według której wskaźnik priorytetu definiuje kolejność realizacji czynności zarówno na zasobie krytycznym określonym mianem bębna, jak i na pozostałych zasobach.

EN

The paper deals with the problem of defining constraints limiting the number of projects that can be curried out concurrently. An alternative method of describing occupancy of resources was presented. Sequence of analysing constraints limiting the number of running project is based on Theory of Constrains. According to this philosophy the priority rule defined the order of project execution both on the critical resource called drum resource, and on other resources.

17

A graphical tabular model for rule-based logic programming and verification

Nalepa G. J., Ligęza A.

Systems Science

|

2005

|

Vol. 31, no 2

89-95

EN

New trends in the development of databases and expert systems seem to underline the role of graphical specification tools, visual information modeling and formal verification procedures. This paper incorporates these new ideas and, moreover, tries to present putting them in engineering practice. The main goal is to move the design procedure to a more abstract, logical level, where knowledge specification is based on use of abstract rule representation, called eXtended Tabular Trees. The main idea behind XTTis to build a hierarchy of Object-Attribute-Value Tables (OAV table). The basic component for knowledge specification is an OAV table. It is analogous to a relational database table; however, it contains conditional part and decision columns. Moreover, the attribute values can be non-atomic ones. Each row provides specification of a single rule. The OAV tables can be connected with one another through appropriate links specifying the control flow in the system. The design specification is automatically translated into Prolog code, so the designer can focus on logical specification of safety and reliability. On the other hand, formal aspects such as completeness, determinism, etc., are automatically verified on-line during the design, so that its verifiable characteristics are preserved. From practical point of view, the design process is performed with an intelligent tool named Mirella.

18

Infinite Unfolding and Transformations of Nondeterministic Programs

Lisper B.

Fundamenta Informaticae

|

2005

|

Vol. 66, nr 4

415--439

EN

We prove some new results about the correctness of transformations of nondeterministic programs. The reported work formalises the intuitive idea that two recursive programs ought to be equivalent, also in a nondeterministic setting, if they can be symbolically unfolded, through deterministic reductions, to the same, possibly infinite, term. In order to do this we develop two related semantics, based on computations modeled by reduction sequences, and argue that they are operationally meaningful. We then specialise to the case of Combinatory Reduction Systems, which provides a suitable rewrite setting for higher order functional programs with nondeterministic constructs, e.g., stream or process primitives. In this setting we prove a theorem about equivalence of programs based on possibly infinite, deterministic unfoldings of programs converging to the same term. We then use the theorem to show a correctness criterion for unfold/fold-transformations of nondeterministic recursive programs. This criterion is similar to the well-known Tamaki-Sato correctness criterion for unfold/fold-transformations of logic programs.

19

Rozwiązanie problemu m zadań - n maszyn metodą CLP oraz metodą genetyczną

Donocik S.

Automatyka / Akademia Górniczo-Hutnicza im. Stanisława Staszica w Krakowie

|

2001

|

T. 5, z. 1/2

141-152

PL

Zostały zaprezentowane dwie różne metody rozwiązywania klasycznego problemu m zadań n maszyn. Pierwsza bazuje na programowaniu w logice z ograniczeniami (Constraint Logic Programming) i została zaimplementowana w językach CHIP v.5.2 i CHIP 4. Druga metoda, bazująca na dostosowanym do zagadnienia algorytmie genetycznym, została napisana w języku C++. Obydwie metody były testowane za pomocą sławnego benchmarku MT10 napisanego przez Mutha i Thompsona. W celu zwiększenia efektywności algorytmu w języku CHIP zostało zastosowanych wiele heurystyk. Najważniejsze polegały na zmianie metody ukonkretniania zmiennych, zmianie metody wyboru wartości z domeny i na losowaniu kolejności ukonkretniania zmiennych. Pierwsze dwie heurystyki przyczyniły się do przyspieszenia obliczeń, jednak uzyskiwane wyniki były jeszcze dalekie od rozwiązania optymalnego. Trzecia heurystyka, losująca kolejność zmiennych, poprawiła wynik, jedna po znacznie dłuższych obliczeniach. Po wprowadzeniu dodatkowej heurystyki, bazującej na wcześniejszych wynikach, udało się osiągnąć wynik 938 w zadawalającym czasie, 937 po dłuższych obliczeniach. Optymalny wynik to 930. Zmodyfikowany algorytm genetyczny zbudowany jest w oparciu o chromosom w postaci permutacji z powtórzeniami, a nie w postaci binarnej. Chromosom taki opisany został w artykule Genetic algorithms in engineering systems, którego autorami są A.M.S. Zalzala and P. J. Fleming. W algorytmie tym chromosom jest pozostawiony przy życiu, jeśli należy do ograniczonej grupy najlepszych chromosomów. Mutacja nie jest wywoływana losowo, lecz w sytuacji, gdy występują dwa lub więcej chromosomy z takim samym wynikiem. Operacja krzyżowania jest wykonywana dla każdej pary różnych chromosomów. Program taki pozwolił na uzyskanie wyniku 934.

EN

Two different approaches to the solution of the classical m jobs n machines problem have been presented. The first is based on Constraint Logic Programming and implemented using CHIP v.5.2. and CHIP 4. The second is based on a custom-tailored Genetic Algorithm and implemented using C++. Both approaches have been tested against the famous MT10 benchmark written by Muth and Thompson. To make the CHIP v. 5.2 solution efficient, a number of heuristics has been used. The most important are switching between various labeling routines (first-fail, etc), switching between various domain search methods and randomly changing the order in which variables are instantiated. The first two heuristics contributed towards accelerating the search in the initial stages and achieving a solution near the optimum but had problems with getting farther. The third heuristic produced a better solution but at the expense of decidedly longer computations. An additional heuristic that changed the ordering of variables in the program according to the best ordering obtained so far produced a slightly better solution and shorter computations (938). The best result obtained for MT10 was 937, the optimum being 930. The custom-tailored Genetic Algorithm is based upon a chromosome structure that is not binary but integer, permutation-wit-repetition based, which is known under the name "Genetic algorithms in engineering systems" and was first presented by A.M.S. Zalzala and P. J. Fleming. The algorithm keeps chromosomes alive provided they belong to a limited set of good chromosomes. Mutation is not initiated randomly, but by the existence of 2 or more than 2 equal results in chromosomes. Crossover operations are always performed for all pairs of different chromosomes. The best result obtained for MT10 was 934.

20

Declarativity in modelling and problem solving

Niederliński A.

Control and Cybernetics

|

2000

|

Vol. 29, no 1

325-339

EN

The paper discusses a new trend in the modelling software for combinatorial and mixed combinatorial-continuous decision problems. The trend, aiming at solving those problems by the simple activity of properly describing them, is best exemplified by a constantly inereasing spectrum of Constraint Logic Programming (CLP) languages. The first such language was Prolog. After a short historical survey concentrating mainly on Prolog, main characteristics of a modern, commercially successful CLP language - CHIP - are presented, discussed and illustrated. The CLP approach to problem solving is compared with traditional Operation Research approaches.