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: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: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:Sreelekha S. Abstract: Most of the tasks which require intelligent behavior have some degree of uncertainty associated with them. The occurrence of uncertainty might be because of several reasons such as the incomplete domain knowledge, unreliable or ambiguous data due to measurement errors, inconsistent data representation. Most of the knowledge-based systems require the incorporation of some form of uncertainty management, in order to handle this kind of indeterminacy present in the system. In this paper, we present one such method to handle the uncertainty in neurules, a neuro-symbolic integration concept. Neuro-Computing is used within the symbolic frame work for improving the performance of symbolic rules. The uncertainty, the personal belief degree that an uncertain event may occur is managed by computing the composite belief values of incomplete or conflicting data. With the implementation of uncertainty management in neurules, the accuracy of the inference mechanism and the generalization performance can be improved. PubDate: 2018-11-01 DOI: 10.1007/s10472-018-9605-y

Authors:David Braun; Nicolas Magaud; Pascal Schreck Abstract: Incidence geometry is a well-established theory which captures the very basic properties of all geometries in terms of points belonging to lines, planes, etc. Moreover, projective incidence geometry leads to a simple framework where many properties can be studied. In this article, we consider two very different but complementary mathematical approaches formalizing this theory within the Coq proof assistant. The first one consists of the usual and synthetic geometric axiom system often encountered in the literature. The second one is more original and relies on combinatorial aspects through the notion of rank which is based on the matroid structure of incidence geometry. This paper mainly contributes to the field by proving the equivalence between these two approaches in both 2D and 3D. This result allows us to study the further automation of many proofs of projective geometry theorems. We give an overview of techniques that will be heavily used in the equivalence proof and are generic enough to be reused later in yet-to-be-written proofs. Finally, we discuss the possibilities of future automation that can be envisaged using the rank notion. PubDate: 2018-10-24 DOI: 10.1007/s10472-018-9604-z

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