Wyniki wyszukiwania - BazTech

1

Adding Metalogic Features to Knowledge Representation Languages

Costantini Stefania, Formisano Andrea

Fundamenta Informaticae

|

2021

|

Vol. 181, nr 1

71--98

EN

In this paper we present a methodology for introducing customizable metalogic features in logic-based knowledge representation and reasoning languages. The proposed approach is based on concepts of introspection and reflection previously introduced and discussed by various authors in relevant literature. This allows a knowledge engineer to specify enhanced reasoning engines by defining properties and meta-properties of relations as expressible for instance in OWL. We employ meta-level axiom schemata based upon a naming (reification) device. We propose general principles for extending the semantics of “host” formalisms accordingly. Consequently, suitable pre-defined libraries of properties can be made available, while user-defined new schemata are also allowed. We make the specific cases of Answer Set Programming (ASP) and Datalog±, where such features may be part of software engineering toolkits for these programming paradigms. On the one hand, concerning ASP, we extend the programming principles and practice to accommodate the proposed methodology, so as to perform meta-reasoning within the plain ASP semantics. The computational complexity of the resulting framework does not change. On the other hand, we show how metalogic features can significantly enrich Datalog± with minor changes to its operational semantics (provided in terms of “chase”) and, also in this case, no additional complexity burden.

2

Unsatisfiable Core Analysis and Aggregates for Optimum Stable Model Search

Alviano Mario, Dodaro Carmine

Fundamenta Informaticae

|

2020

|

Vol. 176, nr 3/4

271--297

EN

Many efficient algorithms for the computation of optimum stable models in the context of Answer Set Programming (ASP) are based on unsatisfiable core analysis. Among them, algorithm OLL was the first introduced in the context of ASP, whereas algorithms ONE and PMRES were first introduced for solving the Maximum Satisfiability problem (MaxSAT) and later on adapted to ASP. In this paper, we present the porting to ASP of another state-of-the-art algorithm introduced for MaxSAT, namely K, which generalizes ONE and PMRES. Moreover, we present a new algorithm called OLL-IN-ONE that compactly encodes all aggregates of OLL by taking advantage of shared aggregate sets propagators. The performance of the algorithms have been empirically compared on instances taken from the latest ASP Competition.

3

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.

4

A Unifying Approach for Nonmonotonic S4F, (Reflexive) Autoepistemic Logic, and Answer Set Programming

Su Ezgi Iraz

Fundamenta Informaticae

|

2020

|

Vol. 176, nr 3/4

205--234

EN

This paper presents a general strategy, bringing together some major types of nonmonotonic reasoning under a monotonic bimodal setting. Such formalisms are also of interest to the fields of knowledge representation and declarative programming. We exemplify the methodology, capturing minimal model reasoning that underlies nonmonotonicity over S4F first, but then we also show how to apply the technique to other nonmonotonic logics respectively based on the modal logics KD45 and SW5 . We naturally succeed it, by modifying only the axioms of the underlying modal logic and show that it successfully works. The last two formalisms are also known as autoepistemic logic (AEL) and its reflexive extension (RAEL) in the given order: AEL is an important form of nonmonotonic reasoning, introduced by Robert C. Moore in order to allow an agent to reason about his own knowledge. Equilibrium logic (EL) is a general-purpose nonmonotonic reasoning formalism, proposed more recently by David Pearce as a semantical framework for answer set programming (ASP). The latter is an efficient declarative problem solving approach with lots of applications to science and technology. Fariñas et al. have embedded EL (and so ASP) into a monotonic bimodal logic. We take this work as an initiative and successfully apply a similar methodology to closely aligned nonmonotonic modal logics. We finally discuss the potential capability to subsume the epistemic extensions of ASP within our unified paradigm.

5

Model Enumeration via Assumption Literals

Alviano Mario, Dodaro Carmine

Fundamenta Informaticae

|

2019

|

Vol. 167, nr 1-2

31--58

EN

Modern, efficient Answer Set Programming solvers implement answer set search via non-chronological backtracking algorithms. The extension of these algorithms to answer set enumeration is nontrivial. In fact, adding blocking constraints to discard already computed answer sets is inadequate because the introduced constraints may not fit in memory or deteriorate the efficiency of the solver. On the other hand, the algorithm implemented by CLASP, which can run in polynomial space, requires to modify the answer set search procedure. The algorithm is revised in this paper so as to make it almost independent from the underlying answer set search procedure, provided that the procedure accepts as input a logic program and a list of assumption literals, and returns an answer set (and associated branching literals). In fact, thanks to an alternative view in terms of transition systems, the revised algorithm is suitable to easily accommodate the enumerate of models of other Boolean languages, among them classical models of propositional theories. On a pragmatic level, the paper presents two implementations of the enumeration algorithm, in WASP for answer set enumeration, and in GLUCOSE for classical models enumeration. The implemented systems are compared empirically to the state of the art solver CLASP.

6

ASP Based Generation of Information Terms for Constructive EL

Bozzato L.

Fundamenta Informaticae

|

2018

|

Vol. 161, nr 1/2

29--51

EN

Constructive description logics define interpretations of description logics under different constructive semantics. These logics have been mostly studied from the point of view of their formal properties: limited practical approaches have been shown for their use in knowledge representation and Semantic Web languages and tools (which, on the other hand, constitute the distinctive applications of description logics). In this paper we demonstrate a solution to address this aspect: from the theoretical point of view, we first introduce an information terms semantics for the minimal description logic EL and we establish formal results linking this constructive semantics to answer set semantics. Using these results, on the practical side, we then present a prototype managing one aspect of such semantics (the generation of information terms of a knowledge base) using OWL-EL ontologies and "off the shelf” tools.

7

Representing Argumentation Frameworks in Answer Set Programming

Sakama C., Rienstra T.

Fundamenta Informaticae

|

2017

|

Vol. 155, nr 3

261--292

EN

This paper studies representation of argumentation frameworks (AFs) in answer set programming (ASP). Four different transformations from AFs to logic programs are provided under the complete semantics, stable semantics, grounded semantics and preferred semantics. The proposed transformations encode labelling-based argumentation semantics in a simple manner, and different semantics of AFs are uniformly characterized by stable models of transformed programs. We apply transformed programs to solving AF problems such as query-answering, enforcement of arguments, agreement or equivalence of different AFs. Logic programming encodings of AFs are also used for representing assumption-based argumentation (ABA) in ASP. The results of this paper exploit new connections between argumentation theory and logic programming, and enable one to perform various argumentation tasks using existing answer set solvers.

8

Modeling Variations of First-Order Horn Abduction in Answer Set Programming

Schüller P.

Fundamenta Informaticae

|

2016

|

Vol. 149, nr 1/2

159--207

EN

We study abduction in First Order Horn logic theories where all atoms can be abduced and we are looking for preferred solutions with respect to three objective functions: cardinality minimality, coherence, and weighted abduction. We represent this reasoning problem in Answer Set Programming (ASP), in order to obtain a flexible framework for experimenting with global constraints and objective functions, and to test the boundaries of what is possible with ASP. Realizing this problem in ASP is challenging as it requires value invention and equivalence between certain constants, because the Unique Names Assumption does not hold in general. To permit reasoning in cyclic theories, we formally describe fine-grained variations of limiting Skolemization. We identify term equivalence as a main instantiation bottleneck, and improve the efficiency of our approach with on-demand constraints that were used to eliminate the same bottleneck in state-of-the-art solvers. We evaluate our approach experimentally on the ACCEL benchmark for plan recognition in Natural Language Understanding. Our encodings are publicly available, modular, and our approach is more efficient than state-of-the-art solvers on the ACCEL benchmark.

9

Evaluating Answer Set Programming with Non-Convex Recursive Aggregates

Alviano M.

Fundamenta Informaticae

|

2016

|

Vol. 149, nr 1/2

1--34

EN

Aggregation functions are widely used in answer set programming (ASP) for representing and reasoning on knowledge involving sets of objects collectively. These sets may also depend recursively on the results of the aggregation functions, even if so far the support for such recursive aggregations was quite limited in ASP systems. In fact, recursion over aggregates was restricted to convex aggregates, i.e., aggregates that may have only one transition from false to true, and one from true to false, in this specific order. Recently, such a restriction has been overcome, so that the user can finally use non-convex recursive aggregates in ASP programs. An evaluation of ASP programs with non-convex recursive aggregates is reported in this paper, also testing a recently proposed extension of the concept of the positive extension graph to the case of programs with aggregates. Moreover, as an additional contribution, new rewritings for EVEN and ODD are presented: EVEN maps to true aggregation sets containing an even number of true literals, and ODD maps to true aggregation sets containing an odd number of true literals. Both aggregates are non-convex, and previously replaced by a conjunction of non-convex sums, whose size is quadratic with respect to the number of literals in the aggregation set. A different rewriting is presented in this paper, whose size is linear with respect to the number of literals in the aggregation set.

10

D-FLAT^2 : Subset Minimization in Dynamic Programming on Tree Decompositions Made Easy

Bliem B., Charwat G., Hecher M., Woltran S.

Fundamenta Informaticae

|

2016

|

Vol. 147, nr 1

27--61

EN

Many problems from the area of AI have been shown tractable for bounded treewidth. In order to put such results into practice, quite involved dynamic programming (DP) algorithms on tree decompositions have to be designed and implemented. These algorithms typically show recurring patterns that call for tasks like subset minimization. In this paper we present a novel approach to obtain such DP algorithms from simpler principles, where the DP formalization of subset minimization is performed automatically. We first give a theoretical account of our novel method, and then present D-FLAT^2, a system that allows one to specify the core DP algorithm via answer set programming (ASP). We illustrate the approach at work by providing several DP algorithms that are more space-efficient than existing solutions, while featuring improved readability, reuse and therefore maintainability of ASP code. Experiments show that our approach also yields a significant improvement in runtime performance.

11

Negation as a Resource: a Novel View on Answer Set Semantics

Costantini S., Formisano A.

Fundamenta Informaticae

|

2015

|

Vol. 140, nr 3/4

279--305

EN

In recent work, we provided a formulation of ASP programs in terms of linear logic theories. Answer sets were characterized in terms of maximal tensor conjunctions provable from such theories. In this paper, we propose a full comparison between Answer Set Semantics and its variation obtained by interpreting literals (including negative literals) as resources, which leads to a different interpretation of negation. We argue that this novel view can be of both theoretical and practical interest, and we propose a modified Answer Set Semantics that we call Resource-based Answer Set Semantics. An advantage is that of avoiding inconsistencies, as every program has a (possibly empty) resource-based answer set. This implies however the introduction of a different way of representing constraints. We provide a characterization of the new semantics as a variation of the answer set semantics, and also in terms of Autoepistemic Logic. The latter characterization leads to a way of computing resource-based answer set via answer set solvers.

12

Synthesizing Concurrent Programs Using Answer Set Programming

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

Fundamenta Informaticae

|

2012

|

Vol. 120, nr 3/4

205-229

EN

We address the problem of the automatic synthesis of concurrent programs within a framework based on Answer Set Programming (ASP). Every concurrent program to be synthesized is specified by providing both the behavioural and the structural properties it should satisfy. Behavioural properties, such as safety and liveness properties, are specified by using formulas of the Computation Tree Logic, which are encoded as a logic program. Structural properties, such as the symmetry of processes, are also encoded as a logic program. Then, the program which is the union of these two encoding programs, is given as input to an ASP system which returns as output a set of answer sets. Finally, each answer set is decoded into a synthesized program that, by construction, satisfies the desired behavioural and structural properties.

13

Nested Preferences in Answer Set Programming

Confalonieri R., Nieves J.C.

Fundamenta Informaticae

|

2011

|

Vol. 113, nr 1

19-39

EN

In this paper, we define a class of nested logic programs, called Nested Logic Programs with Ordered Disjunction (LPODs+), which makes it possible to specify conditional (qualitative) preferences by means of nested preference statements. To this end, we augment the syntax of Logic Programs with Ordered Disjunction (LPODs) to capture more general expressions. We define the LPODs+ semantics in a simple way and we extend most of the results of LPODs showing how our approach generalizes the LPODs framework in a proper way. We also show how the LPODs+ semantics can be computed in terms of a translation procedure that maps a nested ordered disjunction program (OD+-program) into a disjunctive logic program.

14

Look-back Techniques for ASP Programs with Aggregates

Faber W., Leone N., Maratea M., Ricca F.

Fundamenta Informaticae

|

2011

|

Vol. 107, nr 4

379-413

EN

The introduction of aggregates has been one of the most relevant language extensions to Answer Set Programming (ASP). Aggregates are very expressive, they allow to represent many problems in a more succinct and elegant way compared to aggregate-free programs. A significant amount of research work has been devoted to aggregates in the ASP community in the last years, and relevant research results on ASP with aggregates have been published, on both theoretical and practical sides. The high expressiveness of aggregates (eliminating aggregates often causes a quadratic blow-up in program size) requires suitable evaluation methods and optimization techniques for an efficient implementation. Nevertheless, in spite of the above-mentioned research developments, aggregates are treated in a quite straightforward way in most ASP systems. In this paper, we explore the exploitation of look-back techniques for an efficient implementation of aggregates. We define a reason calculus for backjumping in ASP programs with aggregates. Furthermore, we describe how these reasons can be used in order to guide look-back heuristics for programs with aggregates. We have implemented both the new reason calculus and the proposed heuristics in the DLV system, and have carried out an experimental analysis on publicly available benchmarks which shows significant performance benefits

15

Extending and Implementing RASP

Costantini S., Formisano A., Petturiti D.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 1/2

1-33

EN

In previous work we have proposed an extension to ASP (Answer Set Programming), called RASP, standing for ASP with Resources. RASP supports declarative reasoning on production and consumption of (amounts of) resources. The approach combines answer set semantics with quantitative reasoning and relies on an algebraic structure to support computations and comparisons of amounts. The RASP framework provides some form of preference reasoning on resources usage. In this paper, we go further in this direction by introducing expressive constructs for supporting complex preferences specification on aggregate resources. We present a refinement of the semantics of RASP so as to take into account the new constructs. For all the extensions, we provide an encoding into plain ASP.We prove that the complexity of establishing the existence of an answer set, in such an enriched framework, remains NP-complete as in ASP. Finally, we report on raspberry, a prototypical implementation of RASP. This tool consists of a compiler that, given a ground RASP program, produces a pure ASP encoding suitable to be processed by commonly available ASP-solvers.

16

Armin : Automatic Trance Music Composition using Answer Set Programming

Everardo Pérez F. O., Aguilera Ramirez F. A.

Fundamenta Informaticae

|

2011

|

Vol. 113, nr 1

79-96

EN

The Artificial Intelligence (AI) has taken a leading role in many activities which used to be made "by hand"; one of them is the musical composition. Such task now has another alternative implementation, through the support of software that can compose different musical genres to the point where a computer can compose pieces with some autonomy. This paper proposes Armin, a system dedicated to the electronic trance music composition. Armins aim is to provide a trance music composition to serve as a template or a base audio file, ready to add more instruments in a mastering (remastering) production Additionally, it seeks to enable greater collaboration between a machine and a human, both seen as musical composers.

17

A Logic-Based System for e-Tourism

Ricca F., Dimasi A., Grasso G., Ielpa S.M., Iiritano S., Manna M., Leone N.

Fundamenta Informaticae

|

2011

|

Vol. 105, nr 1/2

35-55

EN

In this paper we present a successful application of logic programming for e-tourism: the iTravel system. The system exploits two technologies that are based on the state-of-the-art computational logic system DLV: (i) a system for ontology representation and reasoning, called OntoDLV; and, (ii) HLX a semantic information-extraction tool. The core of iTravel is an ontology which models the domain of tourism offers. The ontology is automatically populated by extracting the information contained in the tourism leaflets produced byε tour operators. A set of specifically devised logic programs is used to reason on the information contained in the ontology for selecting the holiday packages that best fit the customer needs. An intuitive web-based user interface eases the task of interacting with the system for both the customers and the operators of a travel agency.

18

GASP: Answer Set Programming with Lazy Grounding

Dal Palu A., Dovier A., Pontelli E., Rossi G.

Fundamenta Informaticae

|

2009

|

Vol. 96, nr 3

297-322

EN

In recent years, Answer Set Programming has gained popularity as a viable paradigm for applications in knowledge representation and reasoning. This paper presents a novel methodology to compute answer sets of an answer set program. The proposed methodology maintains a bottom-up approach to the computation of answer sets (as in existing systems), but it makes use of a novel structuring of the computation, that originates from the non-ground version of the program. Grounding is lazily performed during the computation of the answer sets. The implementation has been realized using Constraint Logic Programming over finite domains.