In recent years, formalised large theories in form of ontologies, system speci cations or mathematical libraries with thousands of sentences have become more and more common. Automatically proving properties in such theories is an important task in research as well as in industry, for instance, as part of system speci cations. However, automated theorem provers struggle nding proofs when there are too many axioms available. This paper presents and investigates two approaches to reduce the load on automated theorem provers by preselecting axioms: 1) a generalisation of the SInE selection heuristics to arbitrary rst-order provers, and 2) frequent item set mining. These selection methods are implemented in the web application Ontohub. One of the implementations' usefulness is validated while others' is refuted by an evaluation on well-known benchmarks for automated theorem proving.
the AI method of frequent item set mining (which we will employ for axiom selection). Section 3 presents the axiom selection algorithms whose implementation is described brie y in section 4 and evaluated in section 5. Afterwards, section 6 gives an overview of related work while section 7 concludes this paper. 2 2.1
Ontohub [
Ontohub has several distinctive features. The following list gives a short overview of them.
Di erent repositories organise logical theories. For each repository, access rights and ownership can be managed on a per-user or per-team basis.
Logical theories (and all other les) are versioned. The underlying git1 [
Ontohub features an integrated editor for logic theories, which however may also be edited outside of Ontohub: les can either be uploaded via the web front end or via git with SSH.
Ontohub is fully linked-data compliant. One and the same URL can be used for referencing a logical theory, downloading its de ning le or examining it in a user-friendly presentation in the browser. The representation served by Ontohub depends on the requested MIME-type.
Logical theories can be modular and distributed, which means they can be structured into many simpler theories depending on each other.
As in BioPortal [
Diverse structuring languages are supported, including DOL2 [
As a novel contribution of this work, logical theories may contain conjectures which Ontohub recognises.
There is an interface for proving these with di erent parametrisations. 2.2
Ontohub itself does only little analysis of logical theories. Instead, we use the Heterogeneous Tool Set (Hets)3 [
Currently, Hets has an interface to several rst-order automated provers (ATPs) as, for example, SPASS [
Hets also features user interfaces other than the web API, for example, a graphical user interface, a stateless command line interface or an interactive command prompt, but we do not use them in the context of Ontohub.
1Git is a popular decentralised version control system, usually utilised in software development. Many open source software projects use git in combination with Github: https://github.com (last checked: 13 June 2016).
2Details on DOL and its background can be found on http://dol-omg.org (last checked: 13 June 2016). 3Details on HETS can be found on http://hets.eu (last checked: 13 June 2016).
Before starting this work, Ontohub was not able to recognise conjectures in a logical theory. Hets, however, already provided proving functionality and thus, its analysis of the theory already discovered conjectures. However, Hets's proving interface has not been suitable for the use with Ontohub yet. For the preparation of the axiom selection, adjustments of Hets's interface and the creation of an infrastructure for proving conjectures in Ontohub were required.
By this work, Ontohub nds conjectures (called theorems for simplicity) and allows the user to run proof
attempts with each of Hets's ATP that are suitable for the logic translation's target logic. For each nished
proof attempt, Ontohub provides an overview of its details like the time it took, the axioms that were used and
the prover's output. It is even possible to run multiple proof attempts in parallel with di erent ATP which yields
a higher success rate [
Frequent item set mining [
De nition 2.1 Let B = fi1; : : : ; img be a set of items. B is called the item base. A subset I B of the item base is called an item set. A multiset4 T = ft1; : : : ; tng with 8m 2 f1; : : : ; kg : tm B is called a transaction database over B. An element tm of T is called a transaction over B.
Items are these entities whose occurrence together with other entities is analysed, for example, shopping products. A transaction database can be, for example, a collection of purchases in a shop over a given period of time. Note that the same transaction can occur multiple times in a transaction database because it is de ned as a multiset. In practice, the item base is often given implicitly as the union of all the item sets in the transaction database.
De nition 2.2 Let T = ft1; : : : ; tng be a transaction database, I t 2 T covers I i I t. We de ne the multiset KT (I) ..= ft 2 T j I
tg with the characteristic 8t 2 KT (I) : multiplicityKT (I)(t) = multiplicityT (t) meaning that each element of KT (I) occurs as many times in KT (I) as it occurs in T . KT (I) is called the cover of I with respect to T .
The cover is the multiset of transactions that cover the given item set. It is a tool for de ning two of the central notions of this topic: the absolute and the relative support.
De nition 2.3 sT (I) ..= j KT (I) j is the absolute support
T (I) ..= n1 j KT (I) j is the relative support of I with respect to T . of
I with respect to
T .
The support is the number or fraction of transactions in the transaction database that cover an item set. It is also called the absolute or relative frequency.
De nition 2.4 Given the size of the transaction base n 2 N
an item base B = fi1; : : : ; img a transaction database T = ft1; : : : ; tng and the minimum support of either smin 2 f0; : : : ; ng or R min 2 [0; 1]
N 4A multiset (also called a bag) M is an unordered collection of elements. It can contain the same elements multiple times. How many times an element is included is given by the function multiplicityM : M ! N. frequent item set mining is about nding the set of frequent item sets:
There are algorithms which compute the set of frequent item sets e ciently. In the worst case, the time
complexity is exponential in the number of items. However, algorithms used in practice, like FP-Growth [
The basic idea of many selection methods is to nd sentences that share a symbol with the already selected sentences. Standing out, SInE concentrates on the characteristics of de nitions: They describe more special terms by using more general terms. It assumes that the more general terms occur more often in a theory.
An entirely di erent observation we made when manually solving mathematics-textbook exercises is that sentences are probably relevant if they share many symbols with the conjecture or the already selected sentences. This section covers axiom selection ideas based on this observation which are novel contributions of this work.
In the sequel, let symbols(') denote the set of non-logical symbols of a rst-order sentence '. 3.1
SInE operates heuristically on the syntax of rst-order sentences and was rst implemented in the Vampire
Prover. It was rst developed in Hoder's masters thesis `Automated Reasoning in Large Knowledge Bases'. It
entered the public as an implementation in Python with the Vampire V9 and E 0.999 as a back end at
CASCJ45 [
be sentences. Furthermore, let be the conjecture. Let De nition 3.1 Let k 2 N, s be a symbol, ', trigger Sym Sen be an arbitrary relation.
1. s is 0-step triggered i s 2 symbols( ).
3. s is k-step triggered i there is a k-step triggered ' and s 2 symbols('). This recursive de nition can be illustrated as follows: 3 s0 trigger '1 3 s1 trigger '2 3 : : : We now de ne a trigger relation as needed for Def. 3.1.
De nition 3.3 Let s be a symbol, ' be an axiom, 1 t 2 R the tolerance parameter, 1 g 2 N the generality threshold parameter. Let furthermore slcs 2 symbols(') with for all s 2 symbols(') : occ(slcs) occ(s) be the least common symbol of '. The trigger relation of SInE is de ned as: trigger(s; ') i s 2 symbols(') and (either occ(s) g or occ(s) t occ(slcs)).
This means that either a sentence is triggered because it contains very uncommon symbols (due to the generality threshold; occ(s) g) or it is triggered by its least common symbol (or as close to it as the tolerance allows; occ(s) t occ(slcs)).
SInE then selects all axioms that are at most d-step triggered given a d 2 N[f1g as the depth limit parameter. 5The used SInE version and more information about it is available at http://www.cs.man.ac.uk/~hoderk/sine/. Last checked: 13 June 2016. 3.2
Finding sentences that share many symbols with the conjecture is similar to nding frequent item sets: Frequent item set mining answers the question which items occur often in combination.
De nition 3.4 Let smin 2 N and min 2 [0; 1] R be a minimum absolute respectively relative support. Let T = (A; C) be a theory consisting of a set of axioms A and a set of conjectures C. Let the multiset be a transaction database and let the set
T = fsymbols(') j ' 2 A [ Cg
Frequent symbol set mining helps nding the symbols that occur together in a sentence and that occur in the conjecture or the already selected sentences as well. One can then select the sentences that have all the symbols of the frequent symbol sets. This would, however, ignore the short sentences which have less symbols than the absolute minimum support. To consider them as well, one can select all the short sentences that share a symbol with the already selected sentences.
De nition 3.5 Let F be a set of frequent symbol sets for the corresponding theory (A; C) with a de ned minimum support. Let s be a symbol and ' 2 A be an axiom while 2 C is the conjecture. Let 2 n 2 N be a minimal symbol set size, t 2 N be a short axiom tolerance, d 2 N [ f1g be a depth limit.
1. ' is 0-step selected i j symbols(') j < n + t. 2. s is 0-step selected i s 2 symbols( ). 3. S 2 F is selection-enabled i n
j S j.
there is some S 2 F with: S is selection-enabled and S s. symbols(') and s 2 S for a k-step selected symbol 5. s is k-step selected i ' is k-step selected and s 2 symbols('), for k 1.
This de nition describes a simple axiom selection idea that was implemented in Ontohub in this work. The recursive de nition can be illustrated as follows:
F
F 2
2 3 s0 2 S0 symbols('1) 3 s1 2 S1 symbols('2) 3 : : : 3.3
Another idea to circumvent the problem of short sentences is to combine frequent item set mining with SInE. The k-step-trigger relation from Def. 3.1 is modi ed. Apart from this de nition, the SInE algorithm is used as is.
De nition 3.6 Let k 2 N, s; s0 be symbols, ', be sentences. Furthermore, let be the conjecture, trigger Sym Sen be a relation and F be the set of frequent symbol sets for the corresponding theory with a de ned minimum support. Let 1 2 R be a tolerance value. 1. s is 0-step triggered i s 2 symbols( ). 2. s is k-step-trigger-enabled i there is an S 2 F : fsk; sg with sk being k-step triggered and for all s0 2 S : occ(s0) occ(smcs) where smcs 2 S is the most common symbol of S.
4. s is k-step triggered i ' is k-step triggered and s 2 symbols(').
F
S F This recursive de nition can be illustrated as follows (note that the condition involving smcs is not illustrated): 3
2 s00 2 S0 3 s0
This de nition says that not the symbols that occur in a triggered sentence are allowed to trigger further axioms. Instead, those symbols are allowed that occur in a frequent symbol set in combination with a symbol from a triggered sentence. Additionally, only the most common symbols (with a tolerance) of such a frequent symbol set may trigger an axiom. Specifying a high tolerance value allows any symbol from such a set to trigger. The evaluation of SInE showed that there were still many axioms selected and the idea was to reduce the selection even further. 4
The described axiom selection methods were implemented in Ontohub which is based on the web framework Ruby on Rails. One of Ontohub's basic features is the analysis of logical theories which recognises sentences and symbols inside the sentences. These are stored in a relational database and queried when an axiom selection heuristic is invoked.
In our implementation, association objects are stored in the database such that SInE's commonness values and the frequent symbol sets don't need to be re-computed. Furthermore, the minimal tolerance parameter of SInE for each axiom/symbol combination for the symbol to trigger the axiom is saved. This way, the axiom selection of consecutive proof attempts with di erent parametrisations of our selection methods or for di erent conjectures in the same logical theory is very e cient.
The axiom selections that are using frequent symbol set mining are based on the mining algorithm FP-Growth.
The FP-Growth application itself is implemented in C by Borgelt6 [
The axiom selection was evaluated on rst-order logic with the MPTP20787 [
Each problem of the MPTP2078 benchmark comes in a `bushy' and a `chainy' version. The `bushy' version contains only the axioms that are used in a human-made proof while the `chainy' version contains all axioms that were introduced in the MML before the conjecture. Proof attempts were started for each problem in both versions without any axiom selection. Their results are used as a baseline: The problems that could not be solved in the bushy category are considered too hard for the used ATP with the given resources because the bushy ones only contain axioms which contribute to a known human-made proof. The other ones are the ones whose corresponding chainy version might be solved with an appropriate axiom selection. For evaluating the axiom selection methods, only the chainy versions were used. The problems that could be solved in the chainy category without an axiom selection are supposed to be also provable with an axiom selection. An axiom selection is 6The FP-Growth implementations sources or binaries for various systems can be downloaded from http://borgelt.net/fpgrowth. html (last checked: 13 June 2016).
7Information about the MPTP2078 benchmark is available on http://wiki.mizar.org/twiki/bin/view/Mizar/MpTP2078 (last checked: 13 June 2016). parameter generality threshold g depth limit d tolerance value t symbol set tolerance min. absolute support smin short axiom tolerance t minimal symbol set size n
SInE considered not e ective if fewer conjectures can be proven using it than without using it in the chainy category. It is possible that a selection hides axioms that are relevant for a proof and, hence, leads to no conclusion. However, a well performing selection should enable proving more conjectures by selecting all the relevant axioms and hiding only irrelevant ones.
The experiments were conducted on an instance of Ontohub speci cally set up for this work. This instance runs on a machine with two Intel R Xeon R E5-2667 v2 processors with HyperThreading (resulting in 32 logical processor cores) typically clocked at 3.3 GHz along with 256 GB of RAM.
For analysis and proving, 30 Hets instances were used in parallel. This puts heavy load on 30 of the cores. The asynchronous (to the web interface) processing of Hets responses is done by another 30 Ruby processes. Their workload alternates with that of the Hets processes, such that no additional cores are used extensively at the same time. The web user interface's workload is very low. During the evaluation, it is only called by Hets to fetch the theory les and it does not put heavy use to another core. In total 30 cores were used completely and one additional core was used with little load. This leaves one spare processor core for other tasks. During the experiments, processor utilisation of around 70% was observed.
For the benchmark, SPASS v3.7 and the E Theorem Prover 1.8 were used. These are among the best-rated rst-order provers. Since E features an own implementation of SInE, this was not activated by only using the parameters -xAuto -tAuto among (soft) CPU time and memory limiting as well as input and output parameters.
The parameters for the axiom selections are shown in Table 1. Proof attempts were made with each combination of these parameters. Each of the provers was given a timeout of 10 seconds.
During the run with the rst SInE with Frequent Symbol Set Mining con guration, a very slow runtime behaviour was observed for some examples. The selection for these examples was cancelled after about eight hours of selection runtime. As a consequence, a timeout for the axiom selection was implemented: If the axiom selection itself took longer than two minutes, the proof attempt was cancelled. The choice of two minutes is arbitrary. The selection timeout must be chosen considerably large to make sure that much CPU time is consumed because it was measured using wall clock time. The controlled environment ensured that no other CPU-hungry processes were running other than the axiom selection and proving (which are limited to less than one process per core). Hence, it is unlikely that other processes used much CPU time that should have been given to the selection for a perfect timing evaluation (as it would have happened by measuring CPU time instead of wall clock time). The selection timeout has to be much longer than the chosen proving timeout, though, because we want to analyse the selection run time as well. An axiom selection that consequently takes this much longer than proving a conjecture is not an acceptable method because the goal is not only to enable proofs but also shorten the overall proving time which includes the axiom selection. 5.2
In the MPTP2078 benchmark, only 2044 problems are non-trivial. The other 34 conjectures are equal to an axiom and could be proved by Hets during static analysis using re exivity of an entailment relation without invoking an external prover. Only the 2044 non-trivial problems were used for the axiom selection method evaluation.
The rst gures in this section show stacked column charts of the performance: Figure 1 shows how many problems could be solved using SInE. The same goes for Figure 2 using SInE with Frequent Symbol Set Mining. Finally, Figure 3 shows the performance of the Simple Axiom Selection using Frequent Item Set Mining.
Top-rated rst-order provers return a status of the proof attempt telling the result in a single word. These
statuses are de ned in the SZS ontology [
Of these statuses, `THM' and `CSA' indicate a successful prover run, while `TMO' shows that the prover did not nish successfully. There are more such values indicating failures which are actually used by software, but ATP only use the two values `THM' and `CSA' in case of success. We extended this ontology8 by a status speci cally for proving with reduced axiom sets: (iv) CSAS (CounterSatis ableWithSubset): Some models of the selected axioms are models of the conjecture's negation.
If a refutation of the conjecture is found using a strict subset of the axioms (which means that the prover returns with `CSA'), we do not know whether the conjecture is really false or we have excluded an axiom that is crucial to a potentially existing proof. If the prover returns with `THM', we know by monotonicity of entailment relations that the found proof is also a proof with the full axiom set.
When a prover returns with a proof (marked in the diagrams as `THM') or a refutation (marked as `CSA'), a problem is considered solved. When it returns with a refutation while only a true subset of the axioms was used (marked as `CSAS'), or with a proving timeout (marked as `TMO (Prover)') or when the axiom selection takes more than two minutes (marked as `TMO (Selection)'), the problem is considered still unsolved.
8Our modi ed SZS ontology can be found on http://ontohub.org/meta/proof_statuses. 2000 y h s u B .,,.()10110 .,,.()10120 .,,.()01210 .,,.()01220 .,,.()02110 .,,.()20120 .,,.()20210 Axiom Selection Parameters ( , smin, t) ) 0 . 2 , 2 ., 0 2 ( (a) E Theorem Prover (b) SPASS
To interpret the results properly, we need to know the size of the benchmarks. For implementation reasons, there is no very easy way to count the symbols including duplicates. So, only the distinct symbols are taken into account. This is regarded as a su cient approximation for interpreting the results.
The MPTP2078 benchmark in the bushy version has between 2 and 232 axioms per problem. Its average is 31:5 axioms with a standard deviation of 23:4. It has between 2 and 93 distinct symbols per problem with an average of 18:8 and a standard deviation of 12:1. Counting the distinct symbols per axiom, there are between 0 and 26 symbols, 2:9 on average with a standard deviation of 2:7.
The chainy version of the MPTP2078 has between 10 and 4563 axioms per problem. The average axiom count is 1876:4 with a standard deviation of 1288:6. The number of distinct symbols per problem ranges from 5 to 784 with an average of 266:7 and a standard deviation of 229:2. In the axioms, there are between 0 and 26 distinct symbols, 4:9 on average with a standard deviation of 3:1.
Inspecting Figure 1, one can see that the E Theorem Prover improves by about 50% for most of the parametrisations of SInE (45% on average) compared to the chainy versions without any selection. SPASS also performs much better with a selection than without one: Its manages to solve 64% more problems on average across the SInE parametrisations. As a side note, the E Theorem Prover performs better than SPASS, even when comparing the E Theorem Prover without preselecting axioms against the best result with the selection for SPASS. Considering all SInE parametrisations, 769 problems could be solved, 330 of them could not be solved without an axiom selection. Without axiom selection, 444 problems could be solved.
For both provers, the number of `CSA' and `CSAS' results is negligible. For the largest tolerance value without a depth limit, meaning (t; d) = (2:0; 1), the axiom selection takes more than two minutes for 294 examples. These examples have 2165:5 axioms on average with a standard deviation of 1680:1, ranging from 51 to 4563 and 332:5 distinct symbols on average with a standard deviation of 298:7, ranging from 12 to 784. This means that not only the largest problems take long during axiom selection but also some of the small problems. Having a timeout on some of the small problems may be a result of a high CPU load caused by other tasks performed on the hardware. It is imaginable that the timeout at the larger problems is due to the problem size, though. 2000 Axiom Selection Parameters (smin, t) (b) SPASS 2000 s m o ixA1500 d e t c lee1000 s f o r eb 500 m u N 0 yh ) )5 ) )5 ) )5 ) )5 iyn suB .,0 ,.01 ,.2 ,.21 ,.5 .,15 .,0 ,.0 ah
(1 ( (1 ( (1 ( (2 (2 C limit and a limit of 5 increases with a growing tolerance value. As expected, the number of selected axioms highly increases with a growing tolerance value.
Considering the evaluation results, of the three selection methods, SInE clearly is the only usable method for large theories. The methods based on frequent symbol set mining take too much time for large problems and sometimes even for small problems. Even if the selection itself nishes quickly, the selected axioms do not enable proving considerably more conjectures. SInE on the other hand, allows to prove signi cantly more conjectures. For this reason, only SInE will be kept in Ontohub. 6
Axiom selection was actively researched in the recent years. A simple algorithm called RedAx [
Because of saving intermediate information in a database, our implementation of SInE is very e cient for consecutive runs, although because of the implementation in Ruby and because of being bound to a relational database the rst run performs slower than an implementation with native/compiled code such as it exists directly in Vampire or E. One notable feature is the prover-independent operability of the axiom selection. This implementation is usable with any prover that interfaces with Hets. 7
An implementation of axiom selection heuristics was presented: the already existing SInE and two methods based on frequent item set mining. These are implemented in the combination of the web application Ontohub and Hets and run independently of the selected prover, which is a rst step towards an implementation of logicindependent axiom selections in Ontohub. Currently, this implementation is compatible to every Hets-interfaced rst-order prover. The evaluation of the selection methods showed once again the e ectiveness of the SInE algorithm but also revealed that frequent item set mining is not an appropriate tool for selecting axioms because of the slow computation of frequent item sets.
Future work in this eld should extend the feature of independence such that the axiom selections operate independently of the logic as well. A new evaluation could feature a comparison between SInE as it is implemented in provers to the SInE implementation of Ontohub, measuring the performance of consecutive axiom selections that are applied to the same theory (with di erent conjectures) such that the commonness values can be read from the database. Also learning methods could be incorporated into the selection, e.g. learning the best parameters for SInE or entirely learning-based methods similar to MaSh or MOR could be incorporated. This is very promising in the context of Ontohub because of its repository structure which stores information on every logical theory including proof attempts { both successful and failed.