Search

Stream reasoning systems are designed for complex decision-making from possibly infinite, dynamic streams of data. Modern approaches to stream reasoning are usually performing their computations using stand-alone solvers, which incrementally update their internal state and return results as the new portions of data streams are pushed. However, the performance of such approaches degrades quickly as the rates of the input data and the complexity of decision problems are growing. This problem was already recognized in the area of stream processing, where systems became distributed in order to allocate vast computing resources provided by clouds. In this paper we propose a distributed approach to stream reasoning that can efficiently split computations among different solvers communicating their results over data streams. Moreover, in order to increase the throughput of the distributed system, we suggest an interval-based semantics for the LARS language, which enables significant reductions of network traffic. Performed evaluations indicate that the distributed stream reasoning significantly outperforms existing stand-alone LARS solvers when the complexity of decision problems and the rate of incoming data are increasing. [ABSTRACT FROM AUTHOR]

Little historical work examines the problems, practices and values of 'machine learning' as it was understood and justified within pattern recognition research communities prior to the 1980s. This omission has led to a failure to appreciate how the efficacy of machine learning was often justified by its perceived capacity for 'originality' rooted in machine (and human) subjectivity. This paper examines why and how early 1950s pattern recognition researchers came to see 'machine learning' as a technical and epistemological set of nominalist strategies for performing induction and abduction given incomplete, complex or contradictory information that might also spur 'creative' insight in such diverse activities as political judgement and scientific inquiry. I document local research problems, epistemological commitments, institutional contexts and the circulation of 'machine-learning' practices and values through three cases of early-career researchers imagining, building and programming digital computers to 'learn' from 1950 to 1953. This machine learning implemented in learning programs came to be seen by some researchers as more efficacious descriptions of the natural and social world because these descriptions were perspective-dependent, profoundly contingent and contextually non-exhaustive. Often indexed as colloquial appeals to greater 'generality', conceptions of machine learning's efficacy as the capacity to make meaning from contradictory information continues to inform contemporary debates regarding artificial intelligence, society and possibility. [ABSTRACT FROM AUTHOR]

There is a growing interest in leveraging functional programming languages in real-time and embedded contexts. Functional languages are appealing as many are strictly typed, amenable to formal methods, have limited mutation, and have simple but powerful concurrency control mechanisms. Although there have been many recent proposals for specialized domain-specific languages for embedded and real-time systems, there has been relatively little progress on adapting more general purpose functional languages for programming embedded and real-time systems. In this paper, we present our current work on leveraging Standard ML (SML) in the embedded and real-time domains. Specifically, we detail our experiences in modifying MLton, a whole-program optimizing compiler for SML, for use in such contexts. We focus primarily on the language runtime, reworking the threading subsystem, object model, and garbage collector. We provide preliminary results over a radar-based aircraft collision detector ported to SML. [ABSTRACT FROM AUTHOR]

Following the initiative in 2010 taken by the Association for Logic Programming and Cambridge University Press, the full papers accepted for the International Conference on Logic Programming again appear as a special issue of Theory and Practice of Logic Programming (TPLP)—the 27th International Conference on Logic Programming Special Issue. Papers describing original, previously unpublished research and not simultaneously submitted for publication elsewhere were solicited in all areas of logic programming including but not restricted to: Theory: Semantic Foundations, Formalisms, Non- monotonic Reasoning, Knowledge Representation. Implementation: Compilation, Memory Management, Virtual Machines, Parallelism. Environments: Program Analysis, Transformation, Validation, Verification, Debugging, Profiling, Testing. Language Issues: Concurrency, Objects, Coordination, Mobility, Higher Order, Types, Modes, Assertions, Programming Techniques. Related Paradigms: Abductive Logic Programming, Inductive Logic Programming, Constraint Logic Programming, Answer-Set Programming. Applications: Databases, Data Integration and Federation, Software Engineering, Natural Language Processing, Web and Semantic Web, Agents, Artificial Intelligence, Bioinformatics. [ABSTRACT FROM AUTHOR]

Loyalty cards programs have been used by retailers to increase customer retention. Loyality cards provide means to identify a particular customer and to collect customer-specific data, thus enabling individualized marketing; however, operating a loyalty program is complicated for retailers since they require to manage balances, collections, and transfers of customers. This is exactly the same problem the retailers were facing before credit cards were readily available. A new problem is that customers now have too many cards, customers may forget, or even deliberately decide to carry only a selection of their cards. This paper proposes a loyalty program based on a blockchain that does not require a physical card for identifying customers as it associates customers to their phone numbers, since nowadays people always carry their phone. In this perspective, companies can reduce overhead costs associated to managing the loyalty program. This paper reviews the technology required and describes the implementation of a loyalty program based on blockchains. Finally, it also enumerates the reasons for choosing the blockchain technology for this application. [ABSTRACT FROM AUTHOR]

This paper corresponds to an invited oral contribution to the session 5A organised by the IAU inter-commission B2-B5 working group (WG) "Laboratory Astrophysics Data Compilation, Validation and Standardization: from the Laboratory to FAIR usage in the Astronomical Community" at the IAU 2022 General Assembly (GA) Rengel (2022). This WG provides a platform where to discuss the Findability, Accessibility,Interoperability, Reuse (FAIR) usage of laboratory Atomic and Molecular (A&M) data in astronomy and astrophysics. A&M data play a key role in the understanding of the physics and chemistry of processes in several research topics, including planetary science and interdisciplinary research in particular the atmospheres of planets and planetary explorations, etc. Databases, compilation of spectroscopic parameters, and facility tools are used by computer codes to interpret spectroscopic observations and simulate them. In this talk I presented existing A&M databases of interest to the planetary community focusing on access, organisation, infrastructures, limitations and issues, etc. [ABSTRACT FROM AUTHOR]

In live coding, the code can be considered as an archetypal form of score that notates formal processes. We aimed at investigating the possibility of using graphic visuals as a complementary form of descriptive score by visualising sound events using different time representations. To this end, we devised two visualisation systems (Time_X and Time_Z). Time_X represents time along the x -axis, while in Time_Z the objects overlap along an imaginary z -axis. Based on our previous personal experience with the system, such forms of visual scores can help to develop new musicking strategies while live coding. In this article, we wanted to broaden such reflections, and we used them as probes in a study with three live coders. After tailoring the two systems to the usual practice of the three participants, we asked them to use the systems for three weeks and keep a diary. At the end, we interviewed them. Based on their comments, we present some reflections on the use of graphic forms of visualisation in live coding, on how they can support musicking process, and to what extent such visuals can be considered scores. [ABSTRACT FROM AUTHOR]

This article presents several scenarios in which a live coding environment called Paragraph was utilised to telematically play networked and geographically distributed hyperorgans. Situated within the framework of the Global Hyperorgan project, the TCP/Indeterminate Place Quartet have explored the affordances of the organ network through the concept of Tele-Copresence. By outsourcing certain dimensions of the parameter space of the Paragraph language to other members of the quartet, a shared instrumentality is enabled, where the organs are collaboratively controlled by means of this system. Rooted in a personal composer-performer practice and studied from the perspective of the live coder, the Paragraph system, adapted to the TCP/Indeterminate Place environment, can be understood as a modular system of human and non-human agents, into which the other musicians are patched. The distributed parameter space utilised, thus resembles a shared cantus firmus , a foundational, but dynamically changing, ecology for the live coder to play within. [ABSTRACT FROM AUTHOR]

This article describes agent-based music live coding, an approach for music performance and composition based on programming a set of agents in a 2D plane. This style of programming draws from the tradition of agent-based models and facilitates interactive algorithmic control of data-driven sound synthesis methods such as wave terrain synthesis or corpus-based concatenative synthesis. The main elements are a 'terrain', which may be used to access different types of data, a set of agents and their trajectories, and a set of synthesis functions associated to agents. An implementation using the SuperCollider language is demonstrated. [ABSTRACT FROM AUTHOR]

This article reports on a study to identify the new sonic challenges and opportunities for live coders, computer musicians and sonic artists using MIRLCa, a live-coding environment powered by an artificial intelligence (AI) system. MIRLCa works as a customisable worldwide sampler, with sounds retrieved from the collective online Creative Commons (CC) database Freesound. The live-coding environment was developed in SuperCollider by the author in conversation with the live-coding community through a series of workshops and by observing its use by 16 live coders, including the author, in work-in-progress sessions, impromptu performances and concerts. This article presents a qualitative analysis of the workshops, work-in-progress sessions and performances. The findings identify (1) the advantages and disadvantages, and (2) the different compositional strategies that result from manipulating a digital sampler of online CC sounds in live coding. A prominent advantage of using sound samples in live coding is its low-entry access suitable for music improvisation. The article concludes by highlighting future directions relevant to performance, composition, musicology and education. [ABSTRACT FROM AUTHOR]

Pellet injection is used for fuelling and controlling discharges in tokamaks, and it is foreseen in ITER. During pellet injection, a movement of the ablated material towards the low-field side (or outward major radius direction) occurs because of the inhomogeneity of the magnetic field. Due to the complexity of the theoretical models, computer codes developed to simulate the cross-field drift are computationally expensive. Here, we present a one-dimensional semi-analytical model for the radial displacement of ablated material after pellet injection, taking into account both the Alfvén and ohmic currents which shortcircuit the charge separation creating the drift. The model is suitable for rapid calculation of the radial drift displacement, and can be useful for e.g. modelling of disruption mitigation via pellet injection. [ABSTRACT FROM AUTHOR]

Calculi with disjoint intersection types support a symmetric merge operator with subtyping. The merge operator generalizes record concatenation to any type, enabling expressive forms of object composition, and simple solutions to hard modularity problems. Unfortunately, recent calculi with disjoint intersection types and the merge operator lack a (direct) operational semantics with expected properties such as determinism and subject reduction, and only account for terminating programs. This paper proposes a type-directed operational semantics (TDOS) for calculi with intersection types and a merge operator. We study two variants of calculi in the literature. The first calculus, called λi, is a variant of a calculus presented by Oliveira et al. (2016) and closely related to another calculus by Dunfield (2014). Although Dunfield proposes a direct small-step semantics for her calculus, her semantics lacks both determinism and subject reduction. Using our TDOS, we obtain a direct semantics for λi that has both properties. The second calculus, called λi+, employs the well-known subtyping relation of Barendregt, Coppo and Dezani-Ciancaglini (BCD). Therefore, λi+ extends the more basic subtyping relation of λi, and also adds support for record types and nested composition (which enables recursive composition of merged components). To fully obtain determinism, both λi and λi+ employ a disjointness restriction proposed in the original λi calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike previous calculi with disjoint intersection types where recursion is problematic. We relate the static and dynamic semantics of λi to the original version of the calculus and the calculus by Dunfield. Furthermore, for λi+, we show a novel formulation of BCD subtyping, which is algorithmic, has a very simple proof of transitivity and allows for the modular addition of distributivity rules (i.e. without affecting other rules of subtyping). All results have been fully formalized in the Coq theorem prover. [ABSTRACT FROM AUTHOR]

The article discusses various reports published within the issue which include "Automated Termination Analysis for Logic Programs with Cut," by Peter Schneider-Kamp, Thomas Stroeder, and Alexander Serebrenik; "Transformations of Logic Programs on Infinite Lists," by Alberto Pettorossi, Maurizio Proietti, Valerio Senni;, and "Threads and or-Parallelism Unified," by Vítor Santos Costa and Ricardo Rocha.

We present a declarative language, ${\cal PP}$, for the high-level specification of preferences between possible solutions (or trajectories) of a planning problem. This novel language allows users to elegantly express non-trivial, multi-dimensional preferences and priorities over such preferences. The semantics of ${\cal PP}$ allows the identification of most preferred trajectories for a given goal. We also provide an answer set programming implementation of planning problems with ${\cal PP}$ preferences. [ABSTRACT FROM AUTHOR]

Program slicing has been mainly studied in the context of imperative languages, where it has been applied to a wide variety of software engineering tasks, like program understanding, maintenance, debugging, testing, code reuse, etc. This work introduces the first forward slicing technique for declarative multi-paradigm programs which integrate features from functional and logic programming. Basically, given a program and a slicing criterion (a function call in our setting), the computed forward slice contains those parts of the original program which are reachable from the slicing criterion. Our approach to program slicing is based on an extension of (online) partial evaluation. Therefore, it provides a simple way to develop program slicing tools from existing partial evaluators and helps to clarify the relation between both methodologies. A slicing tool for the multi-paradigm language Curry, which demonstrates the usefulness of our approach, has been implemented in Curry itself. [ABSTRACT FROM AUTHOR]

SUMMARY: This paper proposes a new path-planning algorithm which is close to the family of bug algorithms. Path planning is one of the challenging problems in the area of service robotics. In practical applications, traditional methods have some limitations with respect to cost, efficiency, security, flexibility, portability, etc. Our proposed algorithm offers a computationally inexpensive goal-oriented strategy by following a smooth and short trajectory. The paper also presents comparisons with other algorithms. In addition, the paper also presents a test bed which is created to test the algorithm. We have used a two-wheeled differential drive robot for the navigation and only a single camera is used as a feedback sensor. Using an extended Kalman filter, we localize the robot efficiently in the map. Furthermore, we compare the actual path, predicted path and planned path to check the effectiveness of the control system. [ABSTRACT FROM AUTHOR]

The aim of this paper is to investigate the challenges associated with the industrial implementation of generative design systems. Though many studies have been aimed at validating either the technical feasibility or the usefulness of generative design systems, there is, however, a lack of research on the practical implementation and adaptation in industry. To that end, this paper presents two case studies conducted while developing design systems for industrial uses. The first case study focuses on an engineering design application and the other on an industrial design application. In both cases, the focus is on detail-oriented performance-driven generative design systems based on currently available computer-assisted design tools. The development time and communications with the companies were analyzed to identify challenges in the two projects. Overall, the results show that the challenges are not related to whether the design tools are intended for artistic or technical problems, but rather in how to make the design process systematic. The challenges include aspects such as how to fully utilize the potential of generative design tools in a traditional product development process, how to enable designers not familiar with programming to provide design generation logic, and what should be automated and what is better left as a manual task. The paper suggests several strategies for dealing with the identified challenges. [ABSTRACT FROM PUBLISHER]

A natural approach to software quality assurance consists in writing unit tests securing programmer-declared code invariants. Throughout the literature, a great body of work has been devoted to tools and techniques automating this labour-intensive process. A prominent example is the successful use of randomness, in particular, random typable λ-terms, in testing functional programming compilers such as the Glasgow Haskell Compiler. Unfortunately, due to the intrinsically difficult combinatorial structure of typable λ-terms, no effective uniform sampling method is known, setting it as a fundamental open problem in the random software testing approach. In this paper, we combine the framework of Boltzmann samplers, a powerful technique of random combinatorial structure generation, with today's Prolog systems offering a synergy between logic variables, unification with occurs check and efficient backtracking. This allows us to develop a novel sampling mechanism able to construct uniformly random closed simply typed λ-terms of up size 120. We apply our techniques to the generation of uniformly random closed simply typed normal forms and design a parallel execution mechanism pushing forward the achievable term size to 140. [ABSTRACT FROM PUBLISHER]

This paper presents an example of formal reasoning about the semantics of a Prolog program of practical importance (the SAT solver of Howe and King). The program is treated as a definite clause logic program with added control. The logic program is constructed by means of stepwise refinement, hand in hand with its correctness and completeness proofs. The proofs are declarative – they do not refer to any operational semantics. Each step of the logic program construction follows a systematic approach to constructing programs which are provably correct and complete. We also prove that correctness and completeness of the logic program is preserved in the final Prolog program. Additionally, we prove termination, occur-check freedom and non-floundering.Our example shows how dealing with “logic” and with “control” can be separated. Most of the proofs can be done at the “logic” level, abstracting from any operational semantics.The example employs approximate specifications; they are crucial in simplifying reasoning about logic programs. It also shows that the paradigm of semantics-preserving program transformations may be not sufficient. We suggest considering transformations which preserve correctness and completeness with respect to an approximate specification. [ABSTRACT FROM PUBLISHER]

This paper deals with runtime enforcement of untimed and timed properties with uncontrollable events. Runtime enforcement consists in defining and using mechanisms that modify the executions of a running system to ensure their correctness with respect to a desired property. We introduce a framework that takes as input any regular (timed) property described by a deterministic automaton over an alphabet of events, with some of these events being uncontrollable. An uncontrollable event cannot be delayed nor intercepted by an enforcement mechanism. Enforcement mechanisms should satisfy important properties, namely soundness, compliance and optimality – meaning that enforcement mechanisms should output as soon as possible correct executions that are as close as possible to the input execution. We define the conditions for a property to be enforceable with uncontrollable events. Moreover, we synthesise sound, compliant and optimal descriptions of runtime enforcement mechanisms at two levels of abstraction to facilitate their design and implementation. [ABSTRACT FROM AUTHOR]

By increasing the amount of data in computer networks, searching and finding suitable information will be harder for users. One of the most widespread forms of information on such networks are textual documents. So exploring these documents to get information about their content is difficult and sometimes impossible. Multi-document text summarization systems are an aid to producing a summary with a fixed and predefined length, while covering the maximum content of the input documents. This paper presents a novel method for multi-document extractive summarization based on textual entailment relations and sentence compression via formulating the problem as a knapsack problem. In this approach, sentences of documents are ranked according to the extended Tf-Idf method, then entailment scores of selected sentences are computed. Through these scores, the final score of each sentence is calculated. Finally, by decreasing the lengths of sentences via sentence compression, the problem has been solved by greedy and dynamic Programming approaches to the knapsack problem. Experiments on standard summarization datasets and evaluating the results based on the Rouge system show that the suggested method, according to the best of our knowledge, has increased F-measure of query-based summarization systems by two per cent and F-measure of general summarization systems by five per cent. [ABSTRACT FROM AUTHOR]

The family ${\mathcal{R}} X^*$ of regular subsets of the free monoid $X^*$ generated by a finite set X is the standard example of a ${}^*$ -continuous Kleene algebra. Likewise, the family ${\mathcal{C}} X^*$ of context-free subsets of $X^*$ is the standard example of a $\mu$ -continuous Chomsky algebra, i.e. an idempotent semiring that is closed under a well-behaved least fixed-point operator $\mu$. For arbitrary monoids M , ${\mathcal{C}} M$ is the closure of ${\mathcal{R}}M$ as a $\mu$ -continuous Chomsky algebra, more briefly, the fixed-point closure of ${\mathcal{R}} M$. We provide an algebraic representation of ${\mathcal{C}} M$ in a suitable product of ${\mathcal{R}} M$ with $C_2'$ , a quotient of the regular sets over an alphabet $\Delta_2$ of two pairs of bracket symbols. Namely, ${\mathcal{C}}M$ is isomorphic to the centralizer of $C_2'$ in the product of ${\mathcal{R}} M$ with $C_2'$ , i.e. the set of those elements that commute with all elements of $C_2'$. This generalizes a well-known result of Chomsky and Schützenberger (1963, Computer Programming and Formal Systems , 118–161) and admits us to denote all context-free languages over finite sets $X\subseteq M$ by regular expressions over $X\cup\Delta_2$ interpreted in the product of ${\mathcal{R}} M$ and $C_2'$. More generally, for any ${}^*$ -continuous Kleene algebra K the fixed-point closure of K can be represented algebraically as the centralizer of $C_2'$ in the product of K with $C_2'$. [ABSTRACT FROM AUTHOR]

A recent trend in object-oriented programming languages is the use of access permissions (APs) as an abstraction for controlling concurrent executions of programs. The use of AP source code annotations defines a protocol specifying how object references can access the mutable state of objects. Although the use of APs simplifies the task of writing concurrent code, an unsystematic use of them can lead to subtle problems. This paper presents a declarative interpretation of APs as linear concurrent constraint programs (lcc). We represent APs as constraints (i.e., formulas in logic) in an underlying constraint system whose entailment relation models the transformation rules of APs. Moreover, we use processes in lcc to model the dependencies imposed by APs, thus allowing the faithful representation of their flow in the program. We verify relevant properties about AP programs by taking advantage of the interpretation of lcc processes as formulas in Girard's intuitionistic linear logic (ILL). Properties include deadlock detection, program correctness (whether programs adhere to their AP specifications or not), and the ability of methods to run concurrently. By relying on a focusing discipline for ILL, we provide a complexity measure for proofs of the above-mentioned properties. The effectiveness of our verification techniques is demonstrated by implementing the Alcove tool that includes an animator and a verifier. The former executes the lcc model, observing the flow of APs, and quickly finding inconsistencies of the APs vis-à-vis the implementation. The latter is an automatic theorem prover based on ILL. [ABSTRACT FROM AUTHOR]

An important issue towards a broader acceptance of answer-set programming (ASP) is the deployment of tools which support the programmer during the coding phase. In particular, methods for debugging an answer-set program are recognised as a crucial step in this regard. Initial work on debugging in ASP mainly focused on propositional programs, yet practical debuggers need to handle programs with variables as well. In this paper, we discuss a debugging technique that is directly geared towards non-ground programs. Following previous work, we address the central debugging question why some interpretation is not an answer set. The explanations provided by our method are computed by means of a meta-programming technique, using a uniform encoding of a debugging request in terms of ASP itself. Our method also permits programs containing comparison predicates and integer arithmetics, thus covering a relevant language class commonly supported by all state-of-the-art ASP solvers. [ABSTRACT FROM AUTHOR]

Aggregation functions are widely used in answer set programming for representing and reasoning on knowledge involving sets of objects collectively. Current implementations simplify the structure of programs in order to optimize the overall performance. In particular, aggregates are rewritten into simpler forms known as monotone aggregates. Since the evaluation of normal programs with monotone aggregates is in general on a lower complexity level than the evaluation of normal programs with arbitrary aggregates, any faithful translation function must introduce disjunction in rule heads in some cases. However, no function of this kind is known. The paper closes this gap by introducing a polynomial, faithful, and modular translation for rewriting common aggregation functions into the simpler form accepted by current solvers. A prototype system allows for experimenting with arbitrary recursive aggregates, which are also supported in the recent version 4.5 of the grounder gringo, using the methods presented in this paper. [ABSTRACT FROM AUTHOR]

Gelfond and Zhang recently proposed a new stable model semantics based on Vicious Circle Principle in order to improve the interpretation of logic programs with aggregates. The paper focuses on this proposal, and analyzes the complexity of both coherence testing and cautious reasoning under the new semantics. Some surprising results highlight similarities and differences versus mainstream stable model semantics for aggregates. Moreover, the paper reports on the design of compilation techniques for implementing the new semantics on top of existing ASP solvers, which eventually lead to realize a prototype system that allows for experimenting with Gelfond-Zhang's aggregates. [ABSTRACT FROM AUTHOR]

This special issue comprises selected papers which were presented at the workshop on dependently typed programming (DTP 10) in Edinburgh in July 2010 – affiliated with Federated Logic conferences (FLOC 10). Earlier workshops on dependently typed programming took place in Nottingham in 2008 (DTP 2008) and there also has been a Dagstuhl seminar (04381) on this subject in 2004. After DTP 2010, in 2011 a workshop on dependently typed programming (DTP 11) took place in Nijmegen affiliated with Interactive Theorem Proving 2011 (ITP 11). In September 2011 there also was a DTP workshop in Shonan, Japan. [ABSTRACT FROM PUBLISHER]

In this paper we exploit Answer Set Programming (ASP) for reasoning in a rational extension SROEL (⊓,×)RT of the low complexity description logic SROEL(⊓, ×), which underlies the OWL EL ontology language. In the extended language, a typicality operator T is allowed to define concepts T(C) (typical C's) under a rational semantics. It has been proven that instance checking under rational entailment has a polynomial complexity. To strengthen rational entailment, in this paper we consider a minimal model semantics. We show that, for arbitrary SROEL(⊓,×)RT knowledge bases, instance checking under minimal entailment is ΠP2-complete. Relying on a Small Model result, where models correspond to answer sets of a suitable ASP encoding, we exploit Answer Set Preferences (and, in particular, the asprin framework) for reasoning under minimal entailment. [ABSTRACT FROM AUTHOR]

Answer set programming is a declarative programming paradigm oriented towards difficult combinatorial search problems. A fundamental task in answer set programming is to compute stable models, i.e., solutions of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has a stable model is ΣP2-complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely dlv, gnt, cmodels, clasp and wasp. In this paper, we show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for disjunctive answer set solvers. Transition systems give a unifying perspective and bring clarity in the description and comparison of solvers. They can be effectively used for analyzing, comparing and proving correctness of search algorithms as well as inspiring new ideas in the design of disjunctive answer set solvers. In this light, we introduce a general template, which accounts for major techniques implemented in disjunctive solvers. We then illustrate how this general template captures solvers dlv, gnt, and cmodels. We also show how this framework provides a convenient tool for designing new solving algorithms by means of combinations of techniques employed in different solvers. [ABSTRACT FROM PUBLISHER]

In previous work, we proposed a logic-based framework in which computation is the execution of actions in an attempt to make reactive rules of the form if antecedent then consequent true in a canonical model of a logic program determined by an initial state, sequence of events, and the resulting sequence of subsequent states. In this model-theoretic semantics, reactive rules are the driving force, and logic programs play only a supporting role. In the canonical model, states, actions, and other events are represented with timestamps. But in the operational semantics (OS), for the sake of efficiency, timestamps are omitted and only the current state is maintained. State transitions are performed reactively by executing actions to make the consequents of rules true whenever the antecedents become true. This OS is sound, but incomplete. It cannot make reactive rules true by preventing their antecedents from becoming true, or by proactively making their consequents true before their antecedents become true. In this paper, we characterize the notion of reactive model, and prove that the OS can generate all and only such models. In order to focus on the main issues, we omit the logic programming component of the framework. [ABSTRACT FROM PUBLISHER]

Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively defined datatypes such as finite lists, finite trees and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes. [ABSTRACT FROM AUTHOR]

With the significant advances in the area of autonomous agents and multi-agent systems in the last decade, promising technologies for the development and engineering of multi-agent systems have emerged. The result is a variety of agent-oriented programming languages, development frameworks, execution platforms, and tools that facilitate building and engineering of multi-agent systems. This paper provides an overview of the multi-agent programming research field and explains the aim and characteristics of various multi-agent programming languages and development frameworks. This overview is complemented with a discussion on the current trends and challenges in this research community. [ABSTRACT FROM AUTHOR]

A data integration system provides transparent access to different data sources by suitably combining their data, and providing the user with a unified view of them, called global schema. However, source data are generally not under the control of the data integration process; thus, integrated data may violate global integrity constraints even in the presence of locally consistent data sources. In this scenario, it may be anyway interesting to retrieve as much consistent information as possible. The process of answering user queries under global constraint violations is called consistent query answering (CQA). Several notions of CQA have been proposed, e.g., depending on whether integrated information is assumed to be sound, complete, exact, or a variant of them. This paper provides a contribution in this setting: it uniforms solutions coming from different perspectives under a common Answer-Set Programming (ASP)-based core, and provides query-driven optimizations designed for isolating and eliminating inefficiencies of the general approach for computing consistent answers. Moreover, the paper introduces some new theoretical results enriching existing knowledge on the decidability and complexity of the considered problems. The effectiveness of the approach is evidenced by experimental results. [ABSTRACT FROM AUTHOR]

Coding standards and good practices are fundamental to a disciplined approach to software projects irrespective of programing languages being employed. Prolog programing can benefit from such an approach, perhaps more than programing in other languages. Despite this, no widely accepted standards and practices seem to have emerged till now. The present paper is a first step toward filling this void: It provides immediate guidelines for code layout, naming conventions, documentation, proper use of Prolog features, program development, debugging, and testing. Presented with each guideline is its rationale and, where sensible options exist, illustrations of the relative pros and cons for each alternative. A coding standard should always be selected on a per-project basis, based on a host of issues pertinent to any given programing project; for this reason the paper goes beyond the mere provision of normative guidelines by discussing key factors and important criteria that should be taken into account when deciding on a full-fledged coding standard for the project. [ABSTRACT FROM AUTHOR]

Our broader goal is to automatically translate English sentences into formulas in appropriate knowledge representation languages as a step towards understanding and thus answering questions with respect to English text. Our focus in this paper is on the language of Answer Set Programming (ASP). Our approach to translate sentences to ASP rules is inspired by Montague's use of lambda calculus formulas as meaning of words and phrases. With ASP as the target language the meaning of words and phrases are ASP-lambda formulas. In an earlier work we illustrated our approach by manually developing a dictionary of words and their ASP-lambda formulas. However such an approach is not scalable. In this paper our focus is on two algorithms that allow one to construct ASP-lambda formulas in an inverse manner. In particular the two algorithms take as input two lambda-calculus expressions G and H and compute a lambda-calculus expression F such that F with input as G, denoted by F@G, is equal to H; and similarly G@F = H. We present correctness and complexity results about these algorithms. To do that we develop the notion of typed ASP-lambda calculus theories and their orders and use it in developing the completeness results. [ABSTRACT FROM AUTHOR]

Description Logic Programs (dl-programs) proposed by Eiter et al. constitute an elegant yet powerful formalism for the integration of answer set programming with description logics, for the Semantic Web. In this paper, we generalize the notions of completion and loop formulas of logic programs to description logic programs and show that the answer sets of a dl-program can be precisely captured by the models of its completion and loop formulas. Furthermore, we propose a new, alternative semantics for dl-programs, called the canonical answer set semantics, which is defined by the models of completion that satisfy what are called canonical loop formulas. A desirable property of canonical answer sets is that they are free of circular justifications. Some properties of canonical answer sets are also explored. [ABSTRACT FROM AUTHOR]

AbstractConceptual innovation in mechanical engineering design has been extremely challenging compared to the wide applications of automated design systems in digital circuits. This paper presents an automated methodology for open-ended synthesis of mechanical vibration absorbers based on genetic programming and bond graphs. It is shown that our automated design system can automatically evolve passive vibration absorbers that have performance equal to or better than the standard passive vibration absorbers invented in 1911. A variety of other vibration absorbers with competitive performance are also evolved automatically using a desktop PC in less than 10?h. [ABSTRACT FROM AUTHOR]

AbstractThis paper describes how genetic programming has been used as an invention machine to automatically synthesize complete designs for four optical lens systems that duplicated the functionality of previously patented lens systems. The automatic synthesis of the complete design is done ab initio, that is, without starting from a preexisting good design and without prespecifying the number of lenses, the topological arrangement of the lenses, or the numerical or nonnumerical parameters associated with any lens. One of the genetically evolved lens systems infringed a previously issued patent, whereas the others were noninfringing novel designs that duplicated (or improved upon) the performance specifications contained in the patents. One of the patents was issued in the 21st century. The designs were created in a substantially similar and routine way, suggesting that the approach described in the paper can be readily applied to other similar problems in the field of optical design. The genetically evolved designs are instances of human-competitive results produced by genetic programming in the field of optical design. [ABSTRACT FROM AUTHOR]

AbstractThe refinement calculus for logic programs is a framework for deriving logic programs from specifications. It is based on a wide-spectrum language that can express both specifications and code, and a refinement relation that models the notion of correct implementation. In this paper we extend and generalise earlier work on contextual refinement. Contextual refinement simplifies the refinement process by abstractly capturing the context of a subcomponent of a program, which typically includes information about the values of the free variables. This paper also extends and generalises module refinement. A moduleis a collection of procedures that operate on a common data type; module refinement between a specification module Aand an implementation module Callows calls to the procedures of Ato be systematically replaced with calls to the corresponding procedures of C. Based on the conditions for module refinement, we present a method for calculatingan implementation module from a specification module. Both contextual and module refinement within the refinement calculus have been generalised from earlier work and the results are presented in a unified framework. [ABSTRACT FROM AUTHOR]

The research field of Agent-Oriented Software Engineering (AOSE) aims to find abstractions, languages, methodologies and toolkits for modeling, verifying, validating and prototyping complex applications conceptualized as Multiagent Systems (MASs). A very lively research sub-field studies how formal methods can be used for AOSE. This paper presents a detailed survey of six logic-based executable agent specification languages that have been chosen for their potential to be integrated in our ARPEGGIO project, an open framework for specifying and prototyping a MAS. The six languages are ConGolog, AGENT-0, the IMPACT agent programming language, DyLOG, Concurrent METATEM and Ehhf. For each executable language, the logic foundations are described and an example of use is shown. A comparison of the six languages and a survey of similar approaches complete the paper, together with considerations of the advantages of using logic-based languages in MAS modeling and prototyping. [ABSTRACT FROM AUTHOR]

Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: We can finally write correct-by-construction software. However, this extreme accuracy is also a curse: A datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data. In this paper, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: The users can ask the definition of addition to be lifted to lists and they will only be asked the details necessary to carry on adding lists rather than numbers. Our presentation is formalised in the type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory. [ABSTRACT FROM AUTHOR]

Modular logic programs provide a way of viewing logic programs as consisting of many independent, meaningful modules. This paper introduces first-order modular logic programs, which can capture the meaning of many answer set programs. We also introduce conservative extensions of such programs. This concept helps to identify strong relationships between modular programs as well as between traditional programs. We show how the notion of a conservative extension can be used to justify the common projection rewriting. [ABSTRACT FROM AUTHOR]

In this paper, we study an extension of the stable model semantics for disjunctive logic programs where each true atom in a model is associated with an algebraic expression (in terms of rule labels) that represents its justifications. As in our previous work for non-disjunctive programs, these justifications are obtained in a purely semantic way, by algebraic operations (product, addition and application) on a lattice of causal values. Our new definition extends the concept of causal stable model to disjunctive logic programs and satisfies that each (standard) stable model corresponds to a disjoint class of causal stable models sharing the same truth assignments, but possibly varying the obtained explanations. We provide a pair of illustrative examples showing the behaviour of the new semantics and discuss the need of introducing a new type of rule, which we call causal-choice. This type of rule intuitively captures the idea of “A may cause B” and, when causal information is disregarded, amounts to a usual choice rule under the standard stable model semantics. [ABSTRACT FROM AUTHOR]

This paper presents CoreALMlib, an $\mathscr{ALM}$ library of commonsense knowledge about dynamic domains. The library was obtained by translating part of the Component Library (CLib) into the modular action language $\mathscr{ALM}$. CLib consists of general reusable and composable commonsense concepts, selected based on a thorough study of ontological and lexical resources. Our translation targets CLibstates (i.e., fluents) and actions. The resulting $\mathscr{ALM}$ library contains the descriptions of 123 action classes grouped into 43 reusable modules that are organized into a hierarchy. It is made available online and of interest to researchers in the action language, answer-set programming, and natural language understanding communities. We believe that our translation has two main advantages over its CLib counterpart: (i) it specifies axioms about actions in a more elaboration tolerant and readable way, and (ii) it can be seamlessly integrated with ASP reasoning algorithms (e.g., for planning and postdiction). In contrast, axioms are described in CLib using STRIPS-like operators, and CLib's inference engine cannot handle planning nor postdiction. [ABSTRACT FROM AUTHOR]

In recent years, several frameworks and systems have been proposed that extend Inductive Logic Programming (ILP) to the Answer Set Programming (ASP) paradigm. In ILP, examples must all be explained by a hypothesis together with a given background knowledge. In existing systems, the background knowledge is the same for all examples; however, examples may be context-dependent. This means that some examples should be explained in the context of some information, whereas others should be explained in different contexts. In this paper, we capture this notion and present a context-dependent extension of the Learning from Ordered Answer Sets framework. In this extension, contexts can be used to further structure the background knowledge. We then propose a new iterative algorithm, ILASP2i, which exploits this feature to scale up the existing ILASP2 system to learning tasks with large numbers of examples. We demonstrate the gain in scalability by applying both algorithms to various learning tasks. Our results show that, compared to ILASP2, the newly proposed ILASP2i system can be two orders of magnitude faster and use two orders of magnitude less memory, whilst preserving the same average accuracy. [ABSTRACT FROM AUTHOR]

This paper presents a method that allows mobile devices to be globally self-localised in indoor localisation systems by transmitting to them data from position reference anchors. The objective is to establish a reliable one-way down-link communication through signals used in the localisation process in a typically strong fading and multipath channel environment. This is accomplished by using signal processing techniques, including coding and forward error correction, to transmit data using a specific transmission control protocol. Experimental results, using audio as the signal between anchors and the mobile device, demonstrate successful data transmission in realistic scenarios like a common noisy and reverberant room. Spread spectrum noise-like masked signals 4·9 dB below background noise were sufficient to attain correct data reception at four metres distance between a loudspeaker anchor and a mobile device's microphone. [ABSTRACT FROM AUTHOR]