ABSTRACT. Formal systems such as interactive theorem provers and computer algebra systems come with their own libraries or ontologies of mathematical concepts they operate on. These libraries are largely unconnected and (when considered collectively) contain huge duplications of content.

While the TPTP language already provides a standard for formal logics, making the test problems in its library available to various formal systems, a similar language and associated ontology for higher mathematical knowledge is needed to effectively transfer more advanced mathematical knowledge.

We present the Math-in-the-Middle library, a semi-formal archive of formal mathematics in MMT, intended to serve as a collection of interface theories for mathematical concepts.

Its abstract representation in OMDoc/MMT makes it easily parsable and hence available to any formal system, allowing it to serve as a common ontology to exchange knowledge across systems and logical foundations. Its capability to handle content on various levels of formality makes it conveniently extensible even with highly complicated definitions and theorems not easily expressible in terms of simple logical expressions.

The Math-in-the-Middle library is currently seeded with ~200 theories from algebra, arithmetics, calculus, topology, geometry, graph theory, probability theory, functional analysis and measure theory, as well as various theory morphisms between them.

It is already used to facilitate knowledge exchange between computer algebra systems, databases of mathematical objects and modelling software in the OpenDreamKit and MaMoRed projects.

ABSTRACT. In previous work, we translated the mathematical library of the IMPS system (at danger of being lost due to the system no longer actively developed) to OMDoc and partially verify the result within the MMT system against an implementation of the underlying logic of IMPS.

However, so far we only include proof scripts as informal (not machine-checkable) information in our translation. Hence, our goal now is to extend our implementation of the translation to also include as much formal information as possible about the IMPS proof commands, user-defined macetes and their combination language, with the hope of being able to also formally verify (parts of) the translated proofs via MMT.

ABSTRACT. see paper

ABSTRACT. We study possibilities of using symbol elimination in program verification and synthesis. We consider programs in which some instructions or subprograms are not fully specified; the task is to derive conditions on the parameters (or subprograms) which imply inductivity of certain properties. We then propose a method for property-directed invariant generation and analyze its properties. We indicate how to use similar ideas for proving properties of recursively defined functions.

ABSTRACT. Many problems humans face in their everyday life cannot be solved by solely relying on explicitly given facts but so-called commonsense knowledge. These facts are often not formalized in knowledge bases, but can be derived indirectly, e.g., from text passages. However this results in incomplete and inconsistent knowledge. In recent research, many scientists address commonsense reasoning tasks using primarily information retrieval, machine learning or neural network techniques. While this works rather well on several benchmarks, this procedure remains a black box, unable to explain how the correct answer is derived. In our research we address this shortcoming and develop a explainable and responsible artificial intelligence by integrating a theorem prover into the reasoning process. This theorem prover will give a fundamental basis to the derivation process, as well as making it possible to properly explain it and ultimately making an attempt to explain human reasoning.

For this purpose, a reasoning chain was developed at the university in Koblenz which aims to solve commonsense reasoning problems, e.g., from the COPA benchmark set (Choice of Plausible Alternatives), each consisting of a problem and two possible answers. The chain converts the input into a logical representation using Knews and adds information from WordNet, ConceptNet and other Ontologies. This information is passed to the theorem prover Hyper, which conducts a logical model out of it. In the end, this model and the gathered information is fed into a machine learning algorithm, which determines the probabilities of the answer candidates for being the right answer. Primarily we will use recurrent neural networks, as they already proved their superiority at this tasks. More precisely we want to employ predictive neural networks, as they enable us to re-engineer the derivation process.

Our research goal within the CoRg project (Cognitive Reasoning), conducted together with the university in Koblenz, is to evaluate whether a theorem prover can improve this reasoning tasks in the developed chain. Furthermore we will evaluate different ontologies, theorem provers and machine learning algorithms. To address the incomplete and inconsistent knowledge we will also consider the combination of defeasible and normative reasoning. In the end, we will analyze which inputs were most influential to derive the results, e.g., with a principal component analysis on a predictive neural network. This will give us significant hints on how human reasoning might take place.

ABSTRACT. Most modern first-order theorem provers rely on methods like Superposition [1] and Resolution [5], where implications of a clause set are computed to eventually generate the empty clause. The chronological order of computing inferences is a key aspect of proof search and is crucial for the system’s performance. It is typically controlled by a clause selection heuristic. For the task of clause selection, we present a novel heuristic based on artificial neural networks. Deep Learning has demonstrated significant success in several domains [3, 4]. In our approach, clauses are first embedded by a vocabulary that is learned during training and shares features among similar symbols. Compression of clauses to a fixed size is implemented by combining the concepts of dilated convolutions [8] and a dense block [2] to ensure a broad context. The features of a clause to be evaluated are combined with features of the negated conjecture and of the original axiom set, and are processed by a small classifier network. The training is optimized by extensive negative mining and a novel loss function. The heuristic is integrated and tested in the state of the art theorem prover E [6, 7]. In experiments, the network correctly classifies over 90% of all clauses in the test data set with respect to the question if they are useful for the proof or not. However, despite hardware acceleration, the Deep Learning based evaluation currently is several orders of magnitude slower than conventional heuristics, and hence only one from a sample of 25 new proof problems can be solved with the developed technique, highlighting the challenge for future work.

References [1] Leo Bachmair and Harald Ganzinger. Rewrite-Based Equational Theorem Proving with Selection and Simplification. Journal of Logic and Computation, 3(4):217–247, 1994. [2] Gao Huang, Zhuang Liu, Kilian Q Weinberger, and Laurens van der Maaten. Densely connected convolutional networks. In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 2261–2269, 2017. [3] Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. Deep learning. Nature, 521(7553):436–444, 2015. [4] Sarah Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep Network Guided Proof Search. In Thomas Eiter and David Sands, editors, Proc. 21st LPAR, Maun, Botswana, volume 46 of EPiC Series in Computing, pages 85–105, 2017. [5] J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1):23–41, 1965. [6] Stephan Schulz. E – A Brainiac Theorem Prover. Journal of AI Communications, 15(2/3):111–126, 2002. [7] Stephan Schulz. System Description: E 1.8. In Ken McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Proc. of the 19th LPAR, Stellenbosch, volume 8312 of LNCS, pages 735–743. Springer, 2013. [8] Fisher Yu and Vladlen Koltun. Multi-scale context aggregation by dilated convolutions. Computing Research Repository (CoRR), abs/1511.07122, 2015.

ABSTRACT. We describe a light-weight integration of the propositional SAT solver PicoSAT and the saturation-based superposition prover E. The proof search is driven by the saturation prover. Periodically, the saturation is interrupted, and all first-order clauses are grounded. The resulting ground problem is converted to a propositional format and handed to the SAT solver. If the SAT solver reports unsatisfiability, the proof is extracted and reported on the first-order level. First experiments demonstrate the viability of the approach and suggest future extensions. They also yield interesting information about the structure of the search space.

ABSTRACT. The most expressive layer of the Semantic Web is based on Description Logic (DL) [1]. This fact naturally brought about a larger interest in this family of formalisms and their languages. The Semantic Web choice for DL was surely based in two main pros from these formalisms: its rich expressiveness and its inherent reasoning possibilities. Concerning this last aspect, DL reasoners were developed with cutting-edge performance, implementing plenty of specific optimization techniques over tableaux based methods, which took over the field for years. On the other hand, promising methods may have been neglected in such a scenario, in which the tough competition is often focused on gains through optimizations. Therefore, perhaps there is still room available for “basic research” on DL reasoning, in the sense that other efficient calculi need to be adapted to DL, tuned and tested. The purpose of this work is to stimulate research on trying out DL calculi (other than tableaux) by making a careful, detailed comparison between tableaux and other inference methods in a systematic way: first starting with simpler languages (like ALC) without any optimizations. Then gradually including optimizations and comparing them; and continuing these interactive steps: enhancing language expressivity, including optimizations, and testing until reaching the last advances on optimizations and the most expressive DL fragments such as SROIQ. The comparison can also be done by in terms of two other additional aspects: memory usage and algorithm asymptotic analysis, with worst and average cases, etc. The rationale is identifying whether there are fragments which are more suitable to certain inference methods, as well as which aspects or constructs (e.g., the costliest combinations, which usually involve inverses, nominals, equalities, etc) are sensitive to which calculus. Concretely, the idea is to start out with our DL connection calculi [2,3] and reasoner, the RACCOON (ReAsoner based on the Connection Calculus Over ONtologies) [4], which for now takes on ALC, the basic DL fragment, and displayed a surprisingly effective performance in comparison with other well-established reasoners, such as Hermit, FaCT++ and Konclude.

ABSTRACT. We have formalized conflict-driven clause learning (CDCL) in Isabelle/HOL. Later we have refined the CDCL to include two crucial optimisation: two watched literals with blocking literals. We formalized the data structure and the invariants. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications.

ABSTRACT. In 1900, at the International Congress of Mathematicians in Paris and in a publication that shortly followed, David Hilbert presented the twenty-three most important problems for the coming century. The tenth problem concerns the solvability of Diophantine equations and was resolved in 1970 by Yuri Matiyasevich (DPRM theorem).

We conduct a formal verification of Matiyasevich's original proof using the proof assistant Isabelle. We formally state each lemma in Isabelle's formal language and prove each required step. The complete formalised proof includes even the simplest details such as commutativity of matrix addition and more abstract concepts like termination of register machines. At the time of writing, we have completely formalised the proof that exponentiation is Diophantine --- Matiyasevich's key breakthrough from 1970. We have also produced a model of a register machine and shown that given equations describing a certain register machine we can encode them as geometric sums (and hence, as exponential Diophantine equations). Additional work will produce proofs that simulate a register machine as equations. This will then result in a full formalisation of the DPRM theorem.

Fourteen of the original Hilbert problems have been resolved and none of the solutions have been formally verified yet. Our project will be the first complete such formal verification of a Hilbert problem. By formalising the DPRM theorem, we see our larger goal as bringing one of the most important mathematical results the twentieth century into the methods of the twenty-first.

ABSTRACT. We propose a system for large-scale theorem proving contests. We hope that such contests could spark interest in the research field, attract a new generation of theorem proving savants, and foster competition among proof assistants. For the proof assistant Isabelle, we construct and evaluate a prototype implementation of our proposed system architecture.

ABSTRACT. In this project, we want to explore the computer-supported application of formal logic (using automated theorem provers and model finders) to issues in philosophy concerned with: (i) the methodical evaluation and interpretation of arguments and, building upon this, we want to tackle (ii) the problem of formalization: how to search methodically for the most appropriate logical form(s) of a given natural-language argument, by casting its individual statements into expressions of some sufficiently expressive logic (classical or non-classical). Computational hermeneutics is a holistic, iterative, trial-and-error enterprise, where we evaluate the adequacy of some candidate formalization of a sentence by computing the logical validity of the whole argument. We start with formalizations of some simple statements (taking them as tentative) and use them as stepping stones on the way to the formalization of other argument's sentences, repeating the procedure until arriving at a state of reflective equilibrium: A state where our beliefs have the highest degree of coherence and acceptability.

ABSTRACT. Leibniz wrote down a proof for the existence of God accompanied by a note on impossible concepts in Latin (a reproduction of the manuscript is presented). A possibly true contradiction is quite unusual and not compatible with mainstream logic or his “Theodicy”. His example of such a contradiction about an impossible concept, the “square circle”, is still popular in contemporary metaphysics. Similar examples make the proposition of contradiction and possible truth controversial. An alternative formalization approach using a different kind of concept composition is proposed.

ABSTRACT. Wanda is a fully automatic tool to analyse termination of higher-order term rewriting systems in various styles. In this talk I will present Wanda and discuss the underlying methodology, which includes both a discussion of the theory involved and the strategies for automation.