Authors:Tobias Ahlbrecht; Jürgen Dix; Niklas Fiekas Pages: 1 - 16 Abstract: We present the twelfth edition of the Multi-Agent Programming Contest (https://multiagentcontest.org), an annual, community-serving competition that attracts groups from all over the world. Our contest facilitates comparison of multi-agent systems and provides a concrete problem that is interesting in itself and well-suited to be tackled in educational environments. This time, seven teams competed using strictly agent-based as well as traditional programming approaches. PubDate: 2018-10-01 DOI: 10.1007/s10472-018-9594-x Issue No:Vol. 84, No. 1-2 (2018)

Authors:Jonathan Pieper Pages: 17 - 33 Abstract: This paper describes the team BusyBeaver, that participated in and won the Multi-Agent Programming Contest 2017. Its strategy is based on dividing agents into three static groups modeling the work chain of buying, assembling and delivering items. The team is coordinated by a centralized agent doing most of the high-level planning, usually using greedy algorithms and specialized heuristics. There is a heavy focus on proactively buying and assembling some items, in order to quickly complete upcoming jobs. PubDate: 2018-10-01 DOI: 10.1007/s10472-018-9589-7 Issue No:Vol. 84, No. 1-2 (2018)

Authors:Evangelos I. Sarmas Pages: 35 - 56 Abstract: This paper presents the workings of the Flisvos-2017 multi-agent system that participated in the Multi-Agent Programming Contest MAPC 2017 of Clausthal TU. PubDate: 2018-10-01 DOI: 10.1007/s10472-018-9587-9 Issue No:Vol. 84, No. 1-2 (2018)

Authors:Jørgen Villadsen; Oliver Fleckenstein; Helge Hatteland; John Bruntse Larsen Pages: 57 - 74 Abstract: This paper presents the overall strategy utilized by Jason-DTU to achieve a shared second place in the annual Multi-Agent Programming Contest. It provides an overview of the implementation details considering perception, task handling, agent logic and more. The paper analyzes the team’s results in each match, and is summarized by evaluating strengths and weaknesses of the proposed multi-agent system. PubDate: 2018-10-01 DOI: 10.1007/s10472-018-9588-8 Issue No:Vol. 84, No. 1-2 (2018)

Authors:Rafael C. Cardoso; Tabajara Krausburg; Túlio Baségio; Débora C. Engelmann; Jomi F. Hübner; Rafael H. Bordini Pages: 75 - 93 Abstract: The Multi-Agent Programming Contest in 2017 expanded upon the Agents in the City scenario used in the 2016 edition of the contest. In the Agents in the City contest, two teams compete to accomplish logistic tasks in simulations using realistic city maps from OpenStreetMap. The new version of the scenario shifted emphasis to include jobs that require assembled items, new types of facilities, and larger teams, resulting in a significantly more complex scenario than before. In this paper, we describe the strategies used by our team, highlighting our adaptations and any new additions from our participation in the previous year. One such new addition, is that now we have fully explored the use of all three programming dimensions (agent, environment, and organization) found in JaCaMo, the multi-agent system development platform that we used to implement our team. We also provide some discussion and analysis on what we believe were some of our most influential matches. PubDate: 2018-10-01 DOI: 10.1007/s10472-018-9584-z Issue No:Vol. 84, No. 1-2 (2018)

Authors:Philipp Czerner; Jonathan Pieper Pages: 95 - 115 Abstract: In this paper we describe our participation in the 2017 edition of the Multi-Agent Programming Contest as team ‘lampe’. Our strategy was implemented in C++; it uses a centralised organisation of agents and evaluates different strategies based on an internal simulation of the future game state. Strategies are generated using handwritten heuristics in a randomised fashion, also relying on the internal simulation. PubDate: 2018-10-01 DOI: 10.1007/s10472-018-9581-2 Issue No:Vol. 84, No. 1-2 (2018)

Authors:Christopher-Eyk Hrabia; Patrick Marvin Lehmann; Nabil Battjbuer; Axel Hessler; Sahin Albayrak Pages: 117 - 138 Abstract: In the Multi-Agent Programming Contest 2017 the TUBDAI team of the Technische Universität Berlin is using the complex multi-agent scenario to evaluate the application of two frameworks from the field (multi-)robot systems. In particular the task-level decision-making and planning framework ROS Hybrid Behaviour Planner (RHBP) is used to implement the execution and decision-making for single agents. The RHBP framework builds on top of the framework Robot Operating System (ROS) that is used to implement the communication and scenario specific coordination strategy of the agents. The united team for the official contest is formed by volunteering students from a project course and their supervisors. PubDate: 2018-10-01 DOI: 10.1007/s10472-018-9586-x Issue No:Vol. 84, No. 1-2 (2018)

Authors:Luís Cruz-Filipe; Graça Gaspar; Isabel Nunes; Peter Schneider-Kamp Pages: 213 - 246 Abstract: In the database world, integrity constraints are essential to guarantee database integrity. The related problem of database repair deals with finding the best way to change a database so that it satisfies its integrity constraints. These two topics have been studied intensively since the 1980s. The formalism of active integrity constraints, proposed in 2004, aims at addressing them jointly, by providing a syntax whereby a particular subclass of integrity constraints can be specified together with preferred ways to repair inconsistency. In the last decade, several authors have proposed adaptations of the notion of integrity constraints to other reasoning frameworks than relational databases. In this article, we extend this line of work in two ways. First, we target multi-context systems, a general-purpose framework for combining heterogeneous reasoning systems, able to model most other reasoning frameworks, as we demonstrate. Second, we extend the notions of active integrity constraints and grounded repairs to this generalized setting. This way of including repair suggestions inside integrity constraints, subject to a validity check, enables us to define simple iterative algorithms to find all possible grounded repairs for an inconsistent multi-context system, avoiding the need to solve complex or undecidable problems. PubDate: 2018-08-01 DOI: 10.1007/s10472-018-9577-y Issue No:Vol. 83, No. 3-4 (2018)

Authors:Christoph Beierle; Christian Eichhorn; Gabriele Kern-Isberner; Steven Kutsch Pages: 247 - 275 Abstract: While the axiomatic system P is an important standard for plausible, nonmonotonic inferences from conditional knowledge bases, it is known to be too weak to solve benchmark problems like Irrelevance or Subclass Inheritance. Ordinal conditional functions provide a semantic base for system P and have often been used to design stronger inference relations, like Pearl’s system Z, or c-representations. While each c-representation shows excellent inference properties and handles particularly Irrelevance and Subclass Inheritance properly, it is still an open problem which c-representation is the best. In this paper, we consider the skeptical inference relation, called c-inference, that is obtained by taking all c-representations of a given knowledge base into account. We study properties of c-inference and show in particular that it preserves the properties of solving Irrelevance and Subclass Inheritance. Based on a characterization of c-representations as solutions of a Constraint Satisfaction Problem (CSP), we also model skeptical c-inference as a CSP and prove soundness and completeness of the modelling, ensuring that constraint solvers can be used for implementing c-inference. PubDate: 2018-08-01 DOI: 10.1007/s10472-017-9571-9 Issue No:Vol. 83, No. 3-4 (2018)

Authors:Bernhard Bliem; Stefan Woltran Pages: 277 - 295 Abstract: Answer Set Programming has become an increasingly popular formalism for declarative problem solving. Among the huge body of theoretical results, investigations of different equivalence notions between logic programs play a fundamental role for understanding modularity and optimization. While strong equivalence between two programs holds if they can be faithfully replaced by each other in any context (facts and rules), uniform equivalence amounts to equivalent behavior of programs under any set of facts. Both notions (as well as several variants thereof) have been extensively studied. However, the somewhat reverse notion of equivalence which holds if two programs are equivalent under the addition of any set of proper rules (i.e., all rules except facts) has not been investigated yet. In this paper, we close this gap and give a thorough study of this notion, which we call rule equivalence , and its parameterized version where we allow facts over a given restricted alphabet to appear in the context. This notion of equivalence is thus a relationship between two programs whose input is (partially) fixed but where additional proper rules might still be added. Such a notion might be helpful in debugging of programs. We give full characterization results and a complexity analysis for the propositional case of rule equivalence and its relativized versions. Moreover, we address the problem of program simplification under rule equivalence. Finally, we show that rule equivalence is decidable in the non-ground case. PubDate: 2018-08-01 DOI: 10.1007/s10472-017-9567-5 Issue No:Vol. 83, No. 3-4 (2018)

Authors:Arnaud Durand; Miika Hannula; Juha Kontinen; Arne Meier; Jonni Virtema Pages: 297 - 320 Abstract: We define a variant of team semantics called multiteam semantics based on multisets and study the properties of various logics in this framework. In particular, we define natural probabilistic versions of inclusion and independence atoms and certain approximation operators motivated by approximate dependence atoms of Väänänen. PubDate: 2018-08-01 DOI: 10.1007/s10472-017-9568-4 Issue No:Vol. 83, No. 3-4 (2018)

Authors:Flavio Ferrarotti; Klaus-Dieter Schewe; Loredana Tec; Qing Wang Pages: 321 - 349 Abstract: We develop a logic which enables reasoning about single steps of non-deterministic and parallel State Machines (ASMs). Our logic builds upon the unifying logic introduced by Nanchen and Stärk for reasoning about hierarchical (parallel) ASMs. Our main contribution is the handling of non-determinism within the logical formalism. We do this without sacrificing the completeness of the logic for statements about single steps of non-deterministic and parallel ASMs, such as invariants of rules, consistency conditions for rules, or step-by-step equivalence of rules. Moreover, we show that the proposed one-step logic can be easily extended to a multiple-step logic which enables reasoning about concurrent ASMs. PubDate: 2018-08-01 DOI: 10.1007/s10472-017-9569-3 Issue No:Vol. 83, No. 3-4 (2018)

Authors:Ioannis Kokkinis Pages: 351 - 382 Abstract: Let L be some extension of classical propositional logic. The non-iterated probabilistic logic over L is the logic PL that is defined by adding non-nested probabilistic operators in the language of L. For example, in PL we can express a statement like “the probability of truthfulness of A is at least 0.3” where A is a formula of L. The iterated probabilistic logic over L is the logic PPL, where the probabilistic operators may be iterated (nested). For example, in PPL we can express a statement like “this coin is counterfeit with probability 0.6”. In this paper we investigate the influence of probabilistic operators in the complexity of satisfiability in PL and PPL. We obtain complexity bounds, for the aforementioned satisfiability problem, which are parameterized in the complexity of satisfiability of conjunctions of positive and negative formulas that have neither a probabilistic nor a classical operator as a top-connective. As an application of our results we obtain tight complexity bounds for the satisfiability problem in PL and PPL when L is classical propositional logic or justification logic. PubDate: 2018-08-01 DOI: 10.1007/s10472-018-9593-y Issue No:Vol. 83, No. 3-4 (2018)

Authors:Min Kong; Xinbao Liu; Jun Pei; Hao Cheng; Panos M. Pardalos Abstract: This paper introduces a parallel-batching scheduling problem with deterioration and learning effects on parallel machines, where the actual processing time of a job is subject to the phenomena of deterioration and learning. All jobs are first divided into different parallel batches, and the processing time of the batches is equal to the largest processing time of their belonged jobs. Then, the generated batches are assigned to parallel machines to be processed. Motivated by the characteristics of machine maintenance activities in a semiconductor manufacturing process, we take the machine preventive maintenance into account, i.e., the machine should be maintained after a fixed number of batches have been completed. In order to solve the problem, we analyze several structural properties with respect to the batch formation and sequencing. Based on these properties, a hybrid BRKGA-DE algorithm combining biased random-key genetic algorithm (BRKGA) and Differential Evolution (DE) is proposed to solve the parallel-batching scheduling problem. A series of computational experiments is conducted to demonstrate the effectiveness and efficiency of the proposed algorithm. PubDate: 2018-09-27 DOI: 10.1007/s10472-018-9602-1

Authors:Ariel Kellison; Mark Bickford; Robert Constable Abstract: Constructions are central to the methodology of geometry presented in the Elements. This theory therefore poses a unique challenge to those concerned with the practice of constructive mathematics: can the Elements be faithfully captured in a modern constructive framework' In this paper, we outline our implementation of Euclidean geometry based on straightedge and compass constructions in the intuitionistic type theory of the Nuprl proof assistant. A result of our intuitionistic treatment of Euclidean geometry is a proof of the second proposition from Book I of the Elements in its full generality; a result that differs from other formally constructive accounts of Euclidean geometry. Our formalization of the straightedge and compass utilizes a predicate for orientation, which enables a concise and intuitive expression of Euclid’s constructions. PubDate: 2018-09-26 DOI: 10.1007/s10472-018-9603-0

Authors:Jean-Philippe Pernot; Dominique Michelucci; Marc Daniel; Sebti Foufou Abstract: This paper presents a new way of interaction between modelers and solvers to support the Product Development Process (PDP). The proposed approach extends the functionalities and the power of the solvers by taking into account procedural constraints. A procedural constraint requires calling a procedure or a function of the modeler. This procedure performs a series of actions and geometric computations in a certain order. The modeler calls the solver for solving a main problem, the solver calls the modeler’s procedures, and similarly procedures of the modeler can call the solver for solving sub-problems. The features, specificities, advantages and drawbacks of the proposed approach are presented and discussed. Several examples are also provided to illustrate this approach. PubDate: 2018-09-18 DOI: 10.1007/s10472-018-9599-5

Authors:Dolores Barrios Rolanía; Guillermo Delgado Martínez; Daniel Manrique Abstract: This article presents an evolutionary algorithm to autonomously construct full-connected multilayered feedforward neural architectures. This algorithm employs grammar-guided genetic programming with a context-free grammar that has been specifically designed to satisfy three important restrictions. First, the sentences that belong to the language produced by the grammar only encode all valid neural architectures. Second, full-connected feedforward neural architectures of any size can be generated. Third, smaller-sized neural architectures are favored to avoid overfitting. The proposed evolutionary neural architectures construction system is applied to compute the terms of the two sequences that define the three-term recurrence relation associated with a sequence of orthogonal polynomials. This application imposes an important constraint: training datasets are always very small. Therefore, an adequate sized neural architecture has to be evolved to achieve satisfactory results, which are presented in terms of accuracy and size of the evolved neural architectures, and convergence speed of the evolutionary process. PubDate: 2018-09-18 DOI: 10.1007/s10472-018-9601-2

Authors:Mladen Nikolić; Vesna Marinković; Zoltán Kovács; Predrag Janičić Abstract: In recent years, portfolio problem solving found many applications in automated reasoning, primarily in SAT solving and in automated and interactive theorem proving. Portfolio problem solving is an approach in which for an individual instance of a specific problem, one particular, hopefully most appropriate, solving technique is automatically selected among several available ones and used. The selection usually employs machine learning methods. To our knowledge, this approach has not been used in automated theorem proving in geometry so far and it poses a number of new challenges. In this paper we propose a set of features which characterize a specific geometric theorem, so that machine learning techniques can be used in geometry. Relying on these features and using different machine learning techniques, we constructed several portfolios for theorem proving in geometry and also runtime prediction models for provers involved. The evaluation was performed on two corpora of geometric theorems: one coming from geometric construction problems and one from a benchmark set of the GeoGebra tool. The obtained results show that machine learning techniques can be useful in automated theorem proving in geometry, while there is still room for further progress. PubDate: 2018-09-06 DOI: 10.1007/s10472-018-9598-6

Authors:Sana Stojanović-Ðurđević Abstract: In this paper, we propose a new approach for automated verification of informal proofs in Euclidean geometry using a fragment of first-order logic called coherent logic and a corresponding proof representation. We use a TPTP inspired language to write a semi-formal proof of a theorem, that fairly accurately depicts a proof that can be found in mathematical textbooks. The semi-formal proof is verified by generating more detailed proof objects expressed in the coherent logic vernacular. Those proof objects can be easily transformed to Isabelle and Coq proof objects, and also in natural language proofs written in English and Serbian. This approach is tested on two sets of theorem proofs using classical axiomatic system for Euclidean geometry created by David Hilbert, and a modern axiomatic system E created by Jeremy Avigad, Edward Dean, and John Mumma. PubDate: 2018-08-29 DOI: 10.1007/s10472-018-9597-7