Agent-Based HOL Reasoning [pdf slides]
Alexander Steen (Freie Universität Berlin,
Institute of Computer Science),
Max Wisniewski (Freie Universität Berlin,
Institute of Computer Science),
Christoph Benzmüller (Stanford University, CSLI/Freie Universität Berlin, Institute of Computer Science)
Abstract:
We present the automated theorem prover Leo-III and its associated system platform.
In the DFG funded project a novel agent-based deduction system for classical higher-order logic (HOL) is developed
which aims at exploiting massive parallelism at various levels in the reasoning process.
The system allows ad-hoc inclusion of independent specialist agents that add advanced functionality
to the proof search such as consistency checks of the input axiomatization using model finders
or augmented deduction rules for non-classical logics.
The latter, very powerful, capability is enabled by semantical embedding of the desired goal
logic in HOL. Several of such embeddings will be included in Leo-III,
yielding an out-of-the-box automation tool for a great number of (quantified) non-classical logics
relevant in mathematics (e.g. inclusive/free logic as used in projective geometry), philosophy
(e.g. modal logics) and computer science (e.g many-valued logics, paraconsistent logics).
In its current state, Leo-III is based on an ordered paramodulation calculus
for typed lambda-terms, augmented with special means of extensionality treatment.
The employment of agents allows parallelism on the search level by introducing and/or splits
of the search space. The scheduling of the agents' actions is realized as optimization
procedure using combinatorical auction games.
-
Christoph Benzmüller (Stanford University/Freie Universität Berlin)
Dana Scott (Visiting Scholar, University of California, Berkeley)
Abstract:
Terms in classical logic denote, without exceptions, entities in a
non-empty domain of (existing) objects D, and it are these objects of
D the universal and existential quantifiers do range over.
Unfortunately, however, these conditions may render classical logic
unsuited for handling mathematically relevant issues such as
undefinedness and partiality. For example in category theory
composition of maps is not always defined.
Free logic (and inclusive logic) has been proposed as an alternative
to remedy these shortcomings. It distinguishes between a raw domain of
possibly non-existing objects D and a particular subdomain E of D,
containing only the "existing" entities. Free variables range over D
and quantified variables only over E. Each term denotes in D but not
necessarily in E. Unfortunately, as far as we know no theorem provers
have been developed so far for free logic.
In this talk we will present a semantic embedding of free logic in
classical higher-order logic (HOL). This embedding enables
state-of-art theorem provers and model finders for HOL, such as the
first author's Leo provers, the proof assistant Isabelle/HOL and the
model finder Nitpick, to reason within and about free logic in
practical applications.
To illustrate the approach we report on first experiments in which we
have analysed axioms systems in category theory. In our experiments
theorem provers were able to detect a (presumably unknown) redundancy
in the foundational axiom system of the category theory textbook by
Freyd and Scedrov.
Interactive Proving, Higher-Order Rewriting, and Theory Analysis in Theorema 2.0
Alexander Maletzky (RISC, JKU Linz)
Abstract:
In this talk we will report on three useful tools recently implemented in the frame of
the Theorema project: a graphical user interface for interactive proof development, a
higher-order rewriting mechanism, and a tool for automatically analyzing the logical
dependencies of formulas and theories. Each of these three tools already proved
extremely helpful in the extensive formal exploration of a non-trivial mathematical
theory, namely the theory of Gröbner bases in reduction rings, in Theorema.
Interactive proving proceeds in a dialog-oriented manner, where in each step a dialog
window pops up, displaying the current proof situation (characterized by the current
proof goal and list of assumptions) and containing buttons and menus for enabling the
user to specify how to continue, e. g. which inference rule to apply next.
The higher-order rewriting mechanism is capable of first turning Theorema formulas
into rewrite-rules, and then translating these (possibly higher-order)
rewrite-rules into Mathematica transformation rules that can be used for rewriting
expressions efficiently.
Analyzing Theorema theories, finally, works by first constructing a “dependency graph”
reflecting the logical structure of the formulas part of the theory and then employing
well-known functions from graph theory, e. g. to search for cycles, collect all
successors of a node, and many more.
An automated deduction and its implementation for solving problem of sequence at university entrance examination
Yumi Wada (University of Tsukuba, Japan)
Takuya Matsuzaki (Nagoya University, Japan)
Akira Terui (University of Tsukuba, Japan)
Noriko H. Arai (National Institute of Informatics, Japan)
Abstract:
"Todai Robot Project" is a project of artificial intelligence launched by National Institute of Informatics for re-unifying the artificial intelligence field subdivided in 1980’s and afterwards. We focus towards attaining a high score in National Center Test for University Admissions, and use Quantifier Elimination (QE) over the real closed fields as a main tool for solving problems in mathematics. However, it is not applicable for several kinds of problems such as one with sequence.
In this talk, we propose an algorithm for solving problems of sequence at the National Center Test for University Admissions. For solving the most problems of sequence in National Center Test, we need to solve recurrence relations and algebraic equations which are given as constraints for the sequence. Although functions for solving recurrence relations and algebraic equations are available in popular computer algebra systems, it is not easy to find an answer because we need to use these functions back and forth for solving the given recurrence relations and equations in appropriate order.
We have tackled this problem by implementing the algorithm on programing language Haskell and computer algebra system Maple, and present evaluation results for past and mock examinations, including a successful result in an open mock examination in 2015.
Automated Deduction in Ring Theory
Ranganathan Padmanabhan (Department of Mathematics, The University of Manitoba, Canada)
Yang Zhang (Department of Mathematics, The University of Manitoba, Canada)
Abstract:
It is well-known that automated reasoning tools have been widely used in many areas such as lattice theory, loop algebra, group theory and ring theory, which provide powerful methods to check or simplify the proofs,
prove or construct counter-examples for conjectures, and discover the new theorems, see, for example, McCune and Padmanabhan (Lecture Notes in Artificial Intelligence 1095, Springer), and Phillips and Stanovsky (ESARM 2008).
Pover9/Mace4 or its predecessor Otter is one of powerful automated theorem provers for the first-order logic with equality. Since 1990's, this kind of questions attracted more and more people's attentions in automated reasoning area.
The purpose of this paper is to explore various possibilities of using Prover9 in ring theory and semiring theory, in particular, associative rings, rings with involutions, semirings with cancellation laws and Near-rings. We code the corresponding axioms in Prover9, check some well-known theorems, for example, Jacobson and Herstein's commutativity theorems, give some new proofs, and also discuss some new applications.
Automated discovery of elementary geometry theorems: First steps
Miguel A. Abánades (Rey Juan Carlos University, Spain)
Francisco Botana (Vigo University, Spain)
Zoltán Kovács (Private University College of Education of the Diocese of Linz, Austria)
Tomas Recio (Cantabria University, Spain)
Csilla Sólyom-Gecse (Babeş-Bolyai University, Romania)
Abstract:
Considerable attention and efforts have been given to the implementation of automated reasoning tools in interactive geometric environments. Nevertheless, the main goal in such works focused on theorem proving, cf. Java Geometry Expert or GeoGebra. A related issue, automatic discovery, remains almost unexplored in the field of dynamic geometry software.
The talk describes our initial results towards the incorporation into GeoGebra, a worldwide spread software with tenths of millions of users, of automated discovery abilities. As a first result, currently available in the official version, we report on a new command allowing the automatic discovery of loci of points in diagrams. Besides the standard mover-tracer locus finding, the approach also deals with loci constrained by implicit conditions. Hence, our proposal successfully automates a kind of bound dragging in dynamic geometry, the 'dummy locus dragging'. In this way, the cycle of conjecturing-checking-proving will be accessible for general learners in elementary geometry.
Certifying efficient polynomial implementations using the FoCaLize system
Catherine Dubois (Ecole
Nationale Superieure d’Informatique pour l’Industrie et l’Entreprise, Laboratoire SAMOVAR)
Therese Hardin (Universite Pierre et Marie Curie)
Francois Pessaux (ENSTA Paristech)
Renaud Rioboo (Ecole
Nationale Superieure d’Informatique pour l’Industrie et l’Entreprise, Laboratoire SAMOVAR)
Abstract:
Polynomials are of major concern in mathematical software since they form the
base of any system. A computer algebra system is mainly a polynomial manipulator thus correctness and efficiency of their implementation is important for
any system manipulating mathematical values. In related publications, we presented a framework for a polynomial library implementation, which was structured in an object
oriented way and was both efficient and certifiable. This work started the FoCaL
project which is now FoCaLize, a general framework for program certification but polynomials remain a challenging subject for program certification.
Parameter space analysis for algebraic Python programs in SageMath
Matthias Köppe (Department of Mathematics, University of California, Davis)
Yuan Zhou (Department of Mathematics, University of California, Davis)
Abstract:
A metaprogramming trick transforms algebraic programs for testing a
property for a given input parameter into programs that compute
simplified semialgebraic descriptions of the input parameters for
which the property holds. Our implementation of this trick is for
Python programs (within the Python-based computer algebra system
SageMath and using Mathematica for semialgebraic computations). We
illustrate it with an application in the theory of integer linear
optimization, the automatic discovery and proof of certain cutting
plane theorems in integer programming.
Efficient knot discrimination via quandle colouring with SAT and #-SAT
Andrew Fish (University of Brighton)
Alexei Lisitsa (University of Liverpool)
David Stanovsky (Charles University, Prague)
Sarah Swartwood (University of Brighton)
Abstract:
We apply SAT and #-SAT to problems of computational
topology: knot detection and recognition. Quandle coloring can be viewed
as associations of elements of algebraic structures, called quandles, to
arcs of knot diagrams such that certain algebraic relations hold at each
crossing. The existence of a coloring (called colorability) and the number
of colorings of a knot by a quandle are knot invariants that can be used
to distinguish knots. We realise coloring instances as SAT and #-SAT
instances, and produce experimental data demonstrating that a SAT-based
approach to colorability is a practically efficient method for knot
detection and #-SAT can be utilised for knot recognition.
We find a
minimal set of 15 simple quandles (drawn from the set of all 354 simple
quandles of size at most 47) that distinguish all prime knots (up to
reverse and mirror image) of up to 10 crossings. We present a minimal
set of 17 quandles (of size up to 182) that distinguish all prime knots
(up to reverse and mirror image) of up to 12 crossings and compare the
efficiency of computing all colorings with that of the set of 26 previously
discovered distinguishing quandles from Clark et al (of size up to 182),
both using #-SAT.