Skip to main content

Über dieses Buch

This book constitutes the refereed proceedings of the 13th International Conference on Artificial Intelligence and Symbolic Computation, AISC 2018, held in Suzhou, China, in September 2018.

The 13 full papers presented together with 5 short and 2 invited papers were carefully reviewed and selected from 31 submissions. The AISC conference is an important forum when it comes to ensuring that ideas, theoretical insights, methods and results from traditional AI can be discussed and showcased, while fostering new links with other areas of AI such as probabilistic reasoning and deep learning.



Invited Presentations


Automated Reasoning in the Age of the Internet

The internet hosts a vast store of information that we cannot and should not ignore. It’s not enough just to retrieve facts. To make full use of the internet we must also infer new information from old. This is an exciting new opportunity for automated reasoning, but it also presents new kinds of research challenge.
  • There are a huge number of potential axioms from which to infer new theorems. Methods of choosing appropriate axioms are needed.
  • Information is stored on the Internet in diverse forms, e.g., graph and relational databases, JSON (JavaScript Object Notation), CSV (Comma-Separated Values) files, and many others. Some contain errors and others are incomplete: lacking vital contextual details such as time and units of measurements.
  • Information retrieved from the Internet must be automatically curated into a common format before we can apply inference to it. Such a representation must be flexible enough to represent a wide diversity of knowledge formats, as well as supporting the diverse kinds of inference we propose.
  • We can employ forms of inference that are novel in automated reasoning, such as using regression to form new functions from sets of number pairs, and then extrapolation to predict new pairs.
  • Information is of mixed quality and accuracy, so introduces uncertainty into the theorems inferred. Some inference operations, such as regression, also introduce uncertainty. Uncertainty estimates need to be inherited during inference and reported to users in an intelligible form.
We will report on the FRANK (Formally know as RIF: Rich Inference Framework. We changed the name as the RIF acronym is already in use, standing for Requirements Interchange Format.) system that explores this new research direction.
Alan Bundy, Kwabena Nuamah, Christopher Lucas

Methodologies of Symbolic Computation

The methodologies of computer algebra are about making algebra (in the broad sense) algorithmic, and efficient as well. There are ingenious algorithms, even in the obvious settings, and also mechanisms where problems are translated into other (generally smaller) settings, solved there, and translated back. Much of the efficiency of modern systems comes from these translations. One of the major challenges is sparsity, and the complexity of algorithms in the sparse setting is often unknown, as many problems are NP-hard, or much worse.
In view of this, it is argued that the traditional complexity-theoretic method of measuring progress has its limits, and computer algebra should look to the work of the SAT community, with its large families of benchmarks and serious contests, for lessons.
James Davenport

Artificial Intelligence, Theorem Proving and SAT Solving


A Formal Proof of the Computation of Hermite Normal Form in a General Setting

In this work, we present a formal proof of an algorithm to compute the Hermite normal form of a matrix based on our existing framework for the formalisation, execution, and refinement of linear algebra algorithms in Isabelle/HOL. The Hermite normal form is a well-known canonical matrix analogue of reduced echelon form of matrices over fields, but involving matrices over more general rings, such as Bézout domains. We prove the correctness of this algorithm and formalise the uniqueness of the Hermite normal form of a matrix. The succinctness and clarity of the formalisation validate the usability of the framework.
Jose Divasón, Jesús Aransay

Formalizing Some “Small” Finite Models of Projective Geometry in Coq

We study two different descriptions of incidence projective geometry: a synthetic, mathematics-oriented one and a more practical, computation-oriented one, based on the combinatorial concept of rank of a set of points. Using both axiom systems, we prove that some specific finite planes (resp. spaces) verify the axioms of projective plane (resp. space) geometry and Desargues’ property. It requires using repeated case analysis on all variables of some finite inductive data-types and leads to numerous (sub-)goals in the Coq proof assistant. We thus investigate to what extend Coq can deal with such a combinatorial explosion in the number of cases to handle. We propose some easy-to-implement but relevant proof optimizations which, combined together, lead to an efficient way to deal with such large proofs.
David Braun, Nicolas Magaud, Pascal Schreck

Into the Infinite - Theory Exploration for Coinduction

Theory exploration is a technique for automating the discovery of lemmas in formalizations of mathematical theories, using testing and automated proof techniques. Automated theory exploration has previously been successfully applied to discover lemmas for inductive theories, about recursive datatypes and functions. We present an extension of theory exploration to coinductive theories, allowing us to explore the dual notions of corecursive datatypes and functions. This required development of new methods for testing infinite values, and for proof automation. Our work has been implemented in the Hipster system, a theory exploration tool for the proof assistant Isabelle/HOL.
Sólrún Halla Einarsdóttir, Moa Johansson, Johannes Åman Pohjola

Machine Learning for Inductive Theorem Proving

Over the past few years, machine learning has been successfully combined with automated theorem provers to prove conjectures from proof assistants. However, such approaches do not usually focus on inductive proofs. In this work, we explore a combination of machine learning, a simple Boyer-Moore model and ATPs as a means of improving the automation of inductive proofs in the proof assistant HOL Light. We evaluate the framework using a number of inductive proof corpora. In each case, our approach achieves a higher success rate than running ATPs or the Boyer-Moore tool individually.
Yaqing Jiang, Petros Papapanagiotou, Jacques Fleuriot

FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets

In the past few years, much attention has been given to the problem of finding Minimal Unsatisfiable Subsets (MUSes), not only for its theoretical importance but also for its wide range of practical applications, including software testing, hardware verification and knowledge-based validation. In this paper, we propose an algorithm for extracting all MUSes for formulas in the field of propositional logic and the function-free and equality-free fragment of first-order logic. This algorithm extends earlier work, but some changes have been made and a number of optimization strategies have been proposed to improve its efficiency. Experimental results show that our algorithm performs well on many industrial and generated instances, and the strategies adopted can indeed improve the efficiency of our algorithm.
Shaofan Liu, Jie Luo

Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving

This paper presents a method of deciding extended modal formulas that arise, in particular, when reasoning about transformations of relational structures and graphs. The method proceeds by first unwinding a structure that is an over-approximation of potential models, and then selecting effective models with the aid of a SAT solver.
Martin Strecker

Symbolic and Numerical Computation


What Does Qualitative Spatial Knowledge Tell About Origami Geometric Folds?

Origami geometry is based on a set of 7 fundamental folding operations. By applying a well-chosen sequence of the operations, we are able to solve a variety of geometric problems including those impossible by using Euclidean tools. In this paper, we examine these operations from spatial qualitative point of view, i.e. a common-sense knowledge of the space and the relations between its objects. The qualitative spatial representation of the origami folds is suitable for human cognition when practicing origami by hand. We analyze the spatial relations between the parameters of the folding operations using some existing spatial calculus. We attempt to divide the set of possible values of the parameters into disjoint spatial configurations that correspond to a specific number of fold lines. Our analyses and proofs use the power of a computer algebra system and in particular the Gröbner basis algorithm.
Fadoua Ghourabi, Kazuko Takahashi

Discovering Geometry Theorems in Regular Polygons

By using a systematic, automated way, we discover a large amount of geometry statements on regular polygons. Given a regular n-gon, its diagonals are taken, two pairs of them may determine a pair of intersection points that define a segment. By considering all possible segments defined in this way, we can compute the lengths of them symbolically, and, depending on the simplicity of the symbolic result we classify the segment either as “interesting” or “not interesting”.
Among others, we prove that in a regular 11-gon with unit sides the only rational lengths appearing the way described above, are 1 and 2, and the only quadratic surd is \(\sqrt{3}\). The applied way of proving is exhaustion, by using the freely available software tool RegularNGons, programmed by the author. The combinatorial explosion, however, calls for future improvements involving methods in artificial intelligence.
The symbolic method being used is Wu’s algebraic geometry approach [1], combined with the discovery algorithm communicated by Recio and Vélez [2]. The heavy computations are performed by a recent version of the Giac computer algebra software, running in a web browser with the support of the recent technology WebAssembly. Visual communication of the obtained results is operated by the dynamic geometry software GeoGebra.
Zoltán Kovács

Revealing Bistability in Neurological Disorder Models By Solving Parametric Polynomial Systems Geometrically

Understanding the mechanisms of the brain is a common theme for both computational neuroscience and artificial intelligence. Machine learning technique, like artificial neural network, has been benefiting from a better understanding of the neuronal network in human brains. In the study of neurons, mathematical modeling plays a vital role. In this paper, we analyze the important phenomenon of bistability in neurological disorders modeled by ordinary differential equations in virtue of our recently developed method for solving bi-parametric polynomial systems. Unlike the algebraic symbolic approach, our numeric method solves parametric systems geometrically. With respect to the classical bifurcation analysis approach, our method naturally has good initial points thanks to the critical point technique in real algebraic geometry.
Special heuristic strategies are proposed for addressing the multiscale problem of parameters and variables occurring in biological models, as well as taking into account the fact that the variables representing concentrations are non-negative. Comparing with its symbolic algebraic counterparts, one merit of this geometrical method is that it may compute smaller boundaries.
Changbo Chen, Wenyuan Wu

Early Ending in Homotopy Path-Tracking for Real Roots

For computing only the isolated real solutions to a given polynomial system, a heuristic test is proposed to decide whether one homotopy path will converge to a real root, which is based on the asymptotic behavior of an angle defined by two points on the homotopy path. The data that the test requires is easily obtained from the points along the curve-following procedure in homotopy methods. The homotopy path-tracking may be sped up if we start the test before the endgames, since most divergent paths and paths heading to complex roots can be stopped tracking earlier and unnecessary endgames are avoided. Experiments show that the test works pretty well on tested examples.
Yu Wang, Wenyuan Wu, Bican Xia

Autocorrelation via Runs

A problem of interest in the realm of autocorrelation of (binary) finite sequences is to find sequences of length n with given (pre-defined) autocorrelation profiles. This amounts to solving a system of \(\lfloor n/2 \rfloor \) quadratic equations over the boolean cube \(\{-1,+1\}^n\). We establish and discuss a computational approach to this autocorrelation problems, using the concept of runs. An algorithm is given to solve this problem and its application is illustrated with non-trivial examples.
Ilias S. Kotsireas, Jing Yang

Intelligent Documents and Collective Intelligence


: A Linear Algebra Textbook System

Mathematical textbooks play a key role in disseminating systematized mathematical knowledge of study. Most textbooks are published in printed or online electronic format without machine-understandable semantics. In this paper we present an intelligent system for managing linear algebra knowledge in the form of textbook with open access to users. Fine-grained data schemas are designed to represent structural semantics of knowledge contents and implemented by using a graph database with an interface of authoring and browsing knowledge contents and structures. A vector-based retrieving method is implemented to rank knowledge objects with respect to query. We report the results of our investigations on semantic representation of mathematical knowledge with experimental implementations for the development of such textbooks.
Xiaoyu Chen, Haotian Shuai, Dongming Wang, Jing Yang

Towards an Automated Geometer

We report on preliminary work towards the automated finding of theorems in elementary geometry. The resulting system is being currently implemented on top of GeoGebra, a dynamic geometry system with millions of users at high schools and universities. Our system exploits GeoGebra’s recently added new functionalities concerning automated reasoning tools in geometry. We emphasize that the method for finding geometric properties that are present on a user-provided construction is purely symbolic, thus giving such properties rigorous mathematical certainty. We describe some generalities about the system we are developing, which are illustrated through an example.
Francisco Botana, Zoltán Kovács, Tomás Recio

Automatic Deduction in an AI Geometry Book

The pursuit of an AI Geometry Book should involve the study of how currently developing methodologies and technologies of geometry knowledge representation, management, deduction and discovery can be incorporated effectively into a computational application, a “book” of the future.
In the geometry book of the future statements and proofs should be en-lighted by dynamic geometry sketches and diagrams, and the correctness of the proofs should be ensured by computer checking. The book will be intelligent, the reader should be able to ask closed or open questions, and can also ask for proof hints. The book should also provide interactive exercises with automatic correction.
To fulfil such a goal the development of an open library of geometry automated theorem provers with a carefully design application interface protocol, must be considered. This would allow to link computer platforms for geometry with theorem provers, providing the automatic deduction capabilities for the AI Geometry Book.
Pedro Quaresma

A Chinese New Word Detection Approach Based on Independence Testing

New word detection is of great significance for Chinese text information processing, which directly affects the capabilities of word segmentation, information retrieval and automatic translation. Focusing on the problem of Chinese new word detection, this paper proposes an independence-testing-based detection approach with no need of prior information. The paper analyzes statistical characteristics of new words in Chinese texts, uses statistical hypothesis testing to infer the correlations between adjacent semantic units, and proposes an iterative algorithm to detect new words gradually. Our algorithm is evaluated on both large-scale corpus and short news texts. Experimental results show that this approach can effectively detect new words from all kinds of news.
Dongchen Jiang, Xiaoyu Chen, Xin Yang

The Accessibility of Mathematical Formulas for the Visually Impaired in China

Accessing mathematical information, including inputting and reading mathematical formulas on computer, still has big difficulty and barrier for people who are blind or partially sighted. The paper introduces new progress of assistive technology of mathematical documents and Web pages for Chinese visually impaired people. In the paper, we give two conversion models from MathML to Chinese mathematics Braille and a verbalization method of mathematical formulas in Chinese. The work described in the paper is part of “China Digital Platform of Braille” Web site and can be found in http://​www.​braille.​org.​cn.
Wei Su, Chuan Cai, Jinzhao Wu

Specialty-Aware Task Assignment in Spatial Crowdsourcing

With the rapid development of mobile Internet, spatial crowdsourcing is gaining more and more attention from both academia and industry. In spatial crowdsourcing, spatial tasks are sent to workers based on their locations. A wide kind of tasks in spatial crowdsourcing are specialty-aware, which are complex and need to be completed by workers with different skills collaboratively. Existing studies on specialty-aware spatial crowdsourcing assume that each worker has a unified charge when performing different tasks, no matter how many skills of her/him are used to complete the task, which is not fair and practical. In this paper, we study the problem of specialty-aware task assignment in spatial crowdsourcing, where each worker has fine-grained charge for each of their skills, and the goal is to maximize the total utility of the completed tasks based on tasks’ budget and requirements on particular skills. The problem is proven to be NP-hard. Thus, we propose two efficient heuristics to solve the problem. Experiments on both synthetic and real datasets demonstrate the effectiveness and efficiency of our solutions.
Tianshu Song, Feng Zhu, Ke Xu

Game-Theoretic Analysis on the Number of Participants in the Software Crowdsourcing Contest

In this paper a game theoretic model of multiple players is established to relate the reward from the outsourcer and the number of participants in the software crowdsourcing contest in the winner-take-all mode via Nash equilibria of the game. We show how to construct the payoff function of each participant in this game by computing his expected probability of winning sequential pairwise challenges. Preliminary experimental results with our implementations are provided to illustrate the relationships between the reward and the number of participants for three typical participant compositions.
Pengcheng Peng, Chenqi Mou, Wei-Tek Tsai


Weitere Informationen

Premium Partner