Authors:Z. Kovács; T. Recio; C. Sólyom-Gecse Pages: 73 - 87 Abstract: We present an algorithm to help converting expressions having non-negative quantities (like distances) in Euclidean geometry theorems to be usable in a complex algebraic geometry prover. The algorithm helps in refining the output of an existing prover, therefore it supports immediate deployment in high level prover systems. We prove that the algorithm may take doubly exponential time to produce the output in polynomial form, but in many cases it is still computable and useful. PubDate: 2019-04-01 DOI: 10.1007/s10472-018-9590-1 Issue No:Vol. 85, No. 2-4 (2019)

Authors:Sana Stojanović-Ðurđević Pages: 89 - 117 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: 2019-04-01 DOI: 10.1007/s10472-018-9597-7 Issue No:Vol. 85, No. 2-4 (2019)

Authors:Mladen Nikolić; Vesna Marinković; Zoltán Kovács; Predrag Janičić Pages: 119 - 146 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: 2019-04-01 DOI: 10.1007/s10472-018-9598-6 Issue No:Vol. 85, No. 2-4 (2019)

Authors:Jean-Philippe Pernot; Dominique Michelucci; Marc Daniel; Sebti Foufou Pages: 147 - 173 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: 2019-04-01 DOI: 10.1007/s10472-018-9599-5 Issue No:Vol. 85, No. 2-4 (2019)

Authors:Ariel Kellison; Mark Bickford; Robert Constable Pages: 175 - 192 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: 2019-04-01 DOI: 10.1007/s10472-018-9603-0 Issue No:Vol. 85, No. 2-4 (2019)

Abstract: This paper explores the nature of competition between hypotheses and the effect of failing to model this relationship correctly when performing abductive inference. In terms of the nature of competition, the importance of the interplay between direct and indirect pathways, where the latter depends on the evidence under consideration, is investigated. Experimental results show that models which treat hypotheses as mutually exclusive or independent perform well in an abduction problem that requires identifying the most probable hypothesis, provided there is at least some positive degree of competition between the hypotheses. However, even in such cases a significant limitation of these models is their inability to identify a second hypothesis that may well also be true. PubDate: 2019-05-06

Abstract: This is a survey of some recent results relating Dung-style semantics for different types of logical argumentation frameworks and several forms of reasoning with maximally consistent sets (MCS) of premises. The related formalsims are also examined with respect to some rationality postulates and are carried on to corresponding proof systems for non-monotonic reasoning. PubDate: 2019-04-27

Abstract: In the frame of Digital Forensic (DF) and Digital Investigations (DI), the “Evidence Analysis” phase has the aim to provide objective data, and to perform suitable elaboration of these data so as to help in the formation of possible hypotheses, which could later be presented as elements of proof in court. The aim of our research is to explore the applicability of Artificial Intelligence (AI) along with computational logic tools – and in particular the Answer Set Programming (ASP) approach — to the automation of evidence analysis. We will show how significant complex investigations, hardly solvable for human experts, can be expressed as optimization problems belonging in many cases to the \(\mathbb {P}\) or \(\mathbb {N}\mathbb {P}\) complexity classes. All these problems can be expressed in ASP. As a proof of concept, in this paper we present the formalization of realistic investigative cases via simple ASP programs, and show how such a methodology can lead to the formulation of tangible investigative hypotheses. We also sketch a design for a feasible Decision Support System (DSS) especially meant for investigators, based on artificial intelligence tools. PubDate: 2019-04-24

Abstract: As the practical use of answer set programming (ASP) has grown with the development of efficient solvers, we expect a growing interest in extensions of ASP as their semantics stabilize and solvers supporting them mature. Epistemic Specifications, which adds modal operators K and M to the language of ASP, is one such extension. We call a program in this language an epistemic logic program (ELP). Solvers have thus far been practical for only the simplest ELPs due to exponential growth of the search space. We describe a solver that, at the time of its development (mid-2016), was able to solve harder problems better (e.g., without exponentially-growing memory needs w.r.t. K and M occurrences) and faster than any other known ELP solver. PubDate: 2019-04-23

Abstract: In this work, we approach the issue of privacy in distributed constraint reasoning by studying how agents compromise solution quality for preserving privacy, using utility and game theory. We propose a utilitarian definition of privacy in the context of distributed constraint reasoning, detail its different implications, and present a model and solvers, as well as their properties. We then show how important steps in a distributed constraint optimization with privacy requirements can be modeled as a planning problem, and more specifically as a stochastic game. We present experiments validating the interest of our approach, according to several criteria. PubDate: 2019-04-11

Abstract: Discoplan is a durable and efficient system for inferring state constraints (invariants) in planning domains, specified in the PDDL language. It is exceptional in the range of constraint types it can discover and verify, and it directly allows for conditional effects in action operators. However, although various aspects of Discoplan have been previously described and its utility in planning demonstrated, the underlying methodology, the algorithms for the discovery and inductive verification of constraints, and the proofs of correctness of the algorithms and their complexity analysis have never been laid out in adequate detail. The purpose of this paper is to remedy these lacunae. PubDate: 2019-04-08

Abstract: We consider the geometric version of the well-known Generalized Traveling Salesman Problem introduced in 2015 by Bhattacharya et al. that is called the Euclidean Generalized Traveling Salesman Problem in Grid Clusters (EGTSP-GC). They proved the intractability of the problem and proposed first polynomial time algorithms with fixed approximation factors. The extension of these results in the field of constructing the polynomial time approximation schemes (PTAS) and the description of non-trivial polynomial time solvable subclasses for the EGTSP-GC appear to be relevant in the light of the classic C. Papadimitriou result on the intractability of the Euclidean TSP and recent inapproximability results for the Traveling Salesman Problem with Neighborhoods (TSPN) in the case of discrete neighborhoods. In this paper, we propose Efficient Polynomial Time Approximation Schemes (EPTAS) for two special cases of the EGTSP-GC, when the number of clusters \(k=O(\log n)\) and \(k=n-O(\log n)\) . Also, we show that any time, when one of the grid dimensions (height or width) is fixed, the EGTSP-GC can be solved to optimality in polynomial time. As a consequence, we specify a novel non-trivial polynomially solvable subclass of the Euclidean TSP in the plane. PubDate: 2019-03-28

Abstract: This paper analyses the graph mining problem, and the frequent pattern mining task associated with it. In general, frequent pattern mining looks for a graph which occurs frequently within a network or, in the transactional setting, within a dataset of graphs. We discuss this task in the transactional setting, which is a problem of interest in many fields such as bioinformatics, chemoinformatics and social networks. We look at the graph mining problem from a Knowledge Representation point of view, hoping to learn something about support for higher-order logics in declarative languages and solvers. Graph mining is studied as a prototypical problem; it is easily expressible mathematically and exists in many variations. As such, it appears to be a prime candidate for a declarative approach; one would expect this allows for a clear, structured, statement of the problem combined with easy adaptation to changing requirements and variations. Current state-of-the-art KR languages such as IDP and ASP aspire to be practical solvers for such problems (Bruynooghe, Theory Practice Logic Program. (TPLP) 15(6), 783–817 2015). Nevertheless, expressing the graph mining problem in these languages requires unexpectedly complicated and unintuitive encoding techniques. These techniques are in contrast to the ease with which one can transform the mathematical definition of graph mining to a higher-order logic specification, and distract from the problem essentials, complicating possible future adaptation. In this paper, we argue that efforts should be made towards supporting higher-order logic specifications in modern specification languages, without unintuitive and complicated encoding techniques. We argue that this not only makes representation clearer and more susceptible to future adaptation, but might also allow for faster, more competitive solver techniques to be implemented. PubDate: 2019-03-28

Abstract: In this article, we provide the epistemic-entrenchment and partial-meet characterizations of a new, important class of concrete revision operators (all of which satisfy the AGM postulates for revision), called Parametrized Difference revision operators (PD operators, for short). PD operators are natural generalizations of Dalal’s revision operator, with a much greater range of applicability, hence, the epistemic-entrenchment and partial-meet characterizations of the latter are also provided, as a by-product. Lastly, we prove that PD operators satisfy the strong version of Parikh’s relevance-sensitive axiom for belief revision, showing that they are fully compatible with the notion of relevance. PubDate: 2019-03-26

Abstract: The following two strongly NP-hard problems are considered. In the first problem, we need to find in the given finite set of points in Euclidean space the subset of largest size. The sum of squared distances between the elements of this subset and its unknown centroid (geometrical center) must not exceed a given value. This value is defined as percentage of the sum of squared distances between the elements of the input set and its centroid. In the second problem, the input is a sequence (not a set) and we have some additional constraints on the indices of the elements of the chosen subsequence. The restriction on the sum of squared distances is the same as in the first problem. Both problems can be treated as data editing problems aimed to find similar elements and removal of extraneous (dissimilar) elements. We propose exact algorithms for the cases of both problems in which the input points have integer-valued coordinates. If the space dimension is bounded by some constant, our algorithms run in a pseudopolynomial time. Some results of numerical experiments illustrating the performance of the algorithms are presented. PubDate: 2019-03-21

Authors:Michael Beeson; Julien Narboux; Freek Wiedijk Abstract: We used computer proof-checking methods to verify the correctness of our proofs of the propositions in Euclid Book I. We used axioms as close as possible to those of Euclid, in a language closely related to that used in Tarski’s formal geometry. We used proofs as close as possible to those given by Euclid, but filling Euclid’s gaps and correcting errors. Euclid Book I has 48 propositions; we proved 235 theorems. The extras were partly “Book Zero”, preliminaries of a very fundamental nature, partly propositions that Euclid omitted but were used implicitly, partly advanced theorems that we found necessary to fill Euclid’s gaps, and partly just variants of Euclid’s propositions. We wrote these proofs in a simple fragment of first-order logic corresponding to Euclid’s logic, debugged them using a custom software tool, and then checked them in the well-known and trusted proof checkers HOL Light and Coq. PubDate: 2019-01-10 DOI: 10.1007/s10472-018-9606-x

Authors:Johann A. Makowsky Abstract: We survey the status of decidability of the first order consequences in various axiomatizations of Hilbert-style Euclidean geometry. We draw attention to a widely overlooked result by Martin Ziegler from 1980, which proves Tarski’s conjecture on the undecidability of finitely axiomatizable theories of fields. We elaborate on how to use Ziegler’s theorem to show that the consequence relations for the first order theory of the Hilbert plane and the Euclidean plane are undecidable. As new results we add: (A) The first order consequence relations for Wu’s orthogonal and metric geometries (Wen-Tsün Wu, 1984), and for the axiomatization of Origami geometry (J. Justin 1986, H. Huzita 1991) are undecidable. It was already known that the universal theory of Hilbert planes and Wu’s orthogonal geometry is decidable. We show here using elementary model theoretic tools that (B) the universal first order consequences of any geometric theory T of Pappian planes which is consistent with the analytic geometry of the reals is decidable. The techniques used were all known to experts in mathematical logic and geometry in the past but no detailed proofs are easily accessible for practitioners of symbolic computation or automated theorem proving. PubDate: 2018-12-12 DOI: 10.1007/s10472-018-9610-1

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