When humans evaluate the validity of a logical conclusion, they typically consider the meaning of the conclusion, taking into account the context, leading to a naturally targeted approach that avoids irrelevant inferences. For example, if humans are asked to show that all hammocks are also beds, they will certainly not draw conclusions about vehicles or weapons. However, automated theorem provers do not usually take the context of the conclusion into account when selecting inference steps. Existing heuristics for selecting the clause for the next inference step usually do not take into account the meaning of symbol names, overlooking this valuable source of information about the context of a clause. Therefore, in the example above, clauses with symbol names such as weapon or vehicle could well be found in the processed clauses. However, since these clauses are not required for the actual proof, they are not helpful to the prover and tend to distract from the actual proof task. In this paper, we present an approach that uses natural language processing techniques to align the selection of the clause for the next inference step with the meaning of the current proof goal. By mapping symbol names to natural language words and representing them as vectors, we compute similarities between symbols and the proof goal, which inform the selection of the clause for the next inference. The approach has been implemented and evaluated. The experimental results show a significant reduction in the number of clauses processed during proof construction using the proposed method.
When humans evaluate the validity of a logical conclusion,
they naturally consider the context and meaning of the
conclusion and avoid irrelevant inferences. This intuitive
approach is in line with Daniel Kahneman’s model of human
cognition based on two systems [
For example, a human being asked to prove that all hammocks are also beds will intuitively avoid considering unrelated concepts such as vehicles or weapons. Conversely, automated theorem provers typically do not consider the contextual relevance of symbol names when selecting inference steps. Existing heuristics focus on syntactic properties without exploiting the semantic content embedded in symbol names, which can lead to the inclusion of irrelevant clauses and an ineficient proof process.
It is a key strength of human reasoning that we are able to combine both intuitive (system 1) and analytical (system 2) processes. It is therefore plausible that automated theorem proving could similarly benefit from integrating these two approaches, using the contextual understanding of system 1 alongside the logical strictness of system 2. Currently, however, the meaning of symbol names, and thus the contextual content of formulae, is not taken into account during proof construction in automated reasoning.
To address this gap, we propose an approach that integrates statistical methods from natural language processing into the reasoning process to improve the selection of the clause for the next inference step of a theorem prover. We do this by mapping symbol names to natural language words and representing them as vectors. This allows us to measure 10th Workshop on Formal and Cognitive Reasoning (FCR-2024) at the 47th German Conference on Artificial Intelligence (KI-2024, September 23 - 27), Würzburg, Germany $ c.schon@hochschule-trier.de (C. Schon) © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). the semantic similarity between symbols and the goal of the proof. We use these similarities to derive symbol weights, which guide the selection of the clause for the next inference step in a more goal-directed way.
Our approach has been implemented and evaluated using
the E theorem prover [
The main contributions of this paper are: • The introduction of a heuristic for determining symbol weights based on similarity to the proof goal. These weights can be used to guide the selection of the clause for the next inference step in automated theorem proving. • An evaluation of the approach, demonstrating a significant reduction in the number of clauses processed during proof construction for commonsense reasoning tasks.
The paper is structured as follows: after discussing related
work (Sect. 2) and preliminaries (Sect. 3), we describe how
to determine symbol weights based on the similarity of the
symbol name to the proof goal in Sect. 4. In Sect. 5 we
present experimental results of our approach. Finally, we
summarize and discuss ideas for future work in Sect. 6.
The selection of the clause for the next inference step has a
very large influence on the performance of theorem provers.
A perfect selection can make a search unnecessary, and a
proof can be found directly. Most heuristics for selecting
the clause for the next inference step are based on simple
counting of symbols and the like [
To make it possible to adjust symbol weights, the theorem
prover E [
In [
Another approach is to use machine learning to derive
new clause selection strategies from successful proofs [
The ENIGMA [
To the best of our knowledge, none of the currently used approaches to determining symbol weights take into account the meaning of symbol names.
The problem of premise selection, where relevant
formulae for a given proof task have to be selected from a
knowledge base, is related to the problem considered in
this paper. Especially in the area of large mathematical
libraries, there are many approaches to premise selection
that rely on machine learning methods [
The Semantic Web [
Regarding premise selection in commonsense knowledge
bases, there are a few approaches that consider the meaning
of symbol names. One such approach is Similarity SInE [
We are not aware of any approaches that use the meaning of symbols to select the clause to be used in the next reasoning step.
We consider the following first-order logic reasoning task in this paper: given of a set of formulae called the knowledge base (KB) and a goal . The task is to show that the KB implies which can be reduced to showing that the conjunction of KB and ¬ is unsatisfiable. To show the unsatisfiability, usually the conjunction of the KB and the negated goal are transformed into an equisatisfiable clause normal form and a contradiction is inferred from the clause set.
To achieve this contradiction, saturation-based provers organise the execution of their inferences using a given-clause algorithm as shown in Alg. 1. This algorithm maintains two sets of clauses: The set of processed clauses and the set of unprocessed clauses. Initially, all clauses are added to the set of unprocessed clauses, and the set of processed clauses is empty. In each step, the algorithm selects a so-called given clause from the set of unprocessed clauses, adds it to the set of processed clauses, and then performs all the inferences possible with the given clause and the set of processed clauses. The resulting new clauses are added to the set of unprocessed clauses. This process is repeated until either the empty clause is inferred, or the set of unprocessed clauses is empty (or a resource or time limit is reached).
Require: Initial set of clauses initial_clauses 1: processed_set ← {} 2: unprocessed_set ← initial_clauses 3: while True do 4: if empty_clause ∈ processed_set then 5: return “Proof Found” 6: end if 7: if unprocessed_set is empty then 8: return “No Proof Found” 9: end if 10: given_clause ← select_clause(unprocessed_set) 11: remove given_clause from unprocessed_set 12: add given_clause to processed_set 13: new_clauses ← generate_new_clauses(given_clause, processed_set) 14: simplified_clauses ← simplify_clauses(new_clauses) 15: for each clause in simplified_clauses do 16: if clause ∈/ unprocessed_set then 17: add clause to unprocessed_set 18: end if 19: end for 20: end while
The choice of the given clause (line 10 in Alg. 1) strongly influences whether and how fast a proof is found. An unskilful choice of given clause can quickly lead to a large number of irrelevant clauses in the set of unprocessed clauses, making it dificult to find a proof. On the other hand, a skilful choice of the given clause can lead to only those inferences being made that are relevant to the proof task, so that a proof can be found directly.
To select the given clause, heuristics are usually used that assign a weight to each clause. The clause with the lowest weight is then selected as the given clause. Common heuristics use the age of the clause (older clauses are favoured and receive a lower weight) or are based on a weighted symbol count. These heuristics are often used in combination. The ratio of clauses selected by age to clauses selected by symbol count is called the pick-given ratio. A well-known ratio is the pick-given ratio of 5, which means that the heuristic selects the clause with the lowest weighted symbol count ifve times and the oldest clause once. There are many other heuristics for selecting clauses. See Sect. 2 for some pointers in this regard.
In the following, the set of all predicate and function symbols in a formula is represented as sym(F ). In a slight abuse of notation, we use sym(KB ) to denote the set containing all predicate and function symbols occurring in a knowledge base KB . 3.1. Distributional Semantics Our approach uses the meaning of the names of the function and predicate symbols. To do this, we rely on the distributional semantics of natural language. This is best explained using Firth’s famous statement:
keeps. [
One approach in this area are word embeddings [
It is very interesting that words with similar meanings are mapped to similar vectors. Usually, the similarity of two word vectors is calculated with the help of the cosine similarity.
Definition 1 (Cosine similarity of two vectors). Let , ∈ R, both non-zero. The cosine similarity of and is defined as: cos_sim(, ) =
· |||| ||||
The cosine similarity of two vectors and takes values between -1 and 1. For exactly opposite vectors the value is -1, for orthogonal vectors the value is 0 and for equal vectors the value 1. The more similar two vectors are, the greater is their cosine similarity.
In our approach, we use a trained word embedding to determine similarities between the names of symbols in a knowledge base and the proof task. The next section describes how we do this. 19–27
KB extraction of symbol names set sym(KB) of symbol names in KB
Automated theorem provers usually calculate the weight of a clause from the weights of the symbols occurring in the clause. For example, the theorem prover E can be given values for weights for function and predicate symbols. These weights then determine which weights the clauses receive and therefore which clauses are preferred in the reasoning process.
We now present an approach to determine symbol weights, and thus clause weights, that uses the meaning of symbol names. As described above, we assume that there are multiple proof tasks to solve for a given knowledge base. In the following, when we talk about a knowledge base or a goal, we refer to the knowledge base or the goal in this scenario.
Our approach uses a word embedding. It is important
that the word embedding fits to the domain of the
knowledge base. For example if the knowlege base is Yago [
Fig. 1 shows the first step of our approach, which
determines a vector representation for all function and predicate
symbols occurring in the knowledge base under
consideration. To achieve this, in a first step, all function and predicate
symbols are extracted from the knowledge base resulting in
the set sym(KB ). Next, during the vector transformation,
all extracted symbols ∈ sym(KB ) are mapped to the
vocabulary of a word embedding. This mapping step is
typically not trivial and highly depends on the knowledge
base in use. It builds upon an existing WordNet mapping
for the knowledge base, if available, which is then
semiautomatically extended. We do not go into detail here and
refer the reader to [
Since we assume that for a large number of goals it has to be proven that they are entailed from the same knowledge base, the efort of this preprocessing step is relativized.
Fig. 2 provides an overview of the process of proving a goal using the symbol-name heuristic. First, a vector representation of the goal is computed for a given goal . To do this, all function and predicate symbols are extracted from the goal leading to the set sym(G ) and mapped to words in the vocabulary of the word embedding used. For this, the above mentioned function map is used. It is important to use the same word embedding that was chosen for the knowledge base in the pre-processing step. The next step is to compute the vector representation for the goal: For each symbol ∈ sym(G ) in the goal, the vector of the word map(s) is looked up in the word embedding. The vectors of all symbols in sym(G ) are summed and divided by the number of symbols in the goal resulting in vector : (1) = ∑︁
∈sym(G) |sym(G )| In other words, the vector representation of a goal corresponds to the average of the vector representations of all the symbols in the goal.
In the next step, weights for symbols in the knowledge base are computed based on the vector representations of the function and predicate symbols in the knowledge base and the vector representation of the goal. To compute the weight of a symbol ∈ sym(KB ), we first compute the similarity of its vector representation and the vector representation of the goal . Cosine similarity is used for this. The values of cosine similarity are between -1 and 1. The higher the similarity of the two vectors, the higher the value. On the other hand, symbol with a low value are preferred by provers. Therefore, we convert the cosine similarities into weights as follows:
We assume a default weight of 1000. From this we subtract 1000 times the cosine similarity. This allows us to account for three decimal places in the cosine similarity. This results in the weight of a symbol as weight (, ) = 1000 − cos_sim(, ) (2)
The weights of the symbols calculated in this way are now passed to the theorem prover together with the proof task. The prover calculates the weights for the clauses from the weights for the symbols and uses them to control the proof process.
A first approach would be to pass all calculated weights for symbols to the theorem prover. Experiments have shown that this does not necessarily lead to the best results. Our experiments have shown that it is most advantageous to pass only the weights of the 10 highest scoring symbols and leave all other symbol weights at the default value of 1000.
To evaluate the approach, we need a knowledge base with
function and predicate symbols that are, or can be, mapped
to natural language words. We also need a large number
of proof tasks for this knowledge base. Adimen SUMO
[
The proof tasks considered in the experiments were
created to test the application of the closed world assumption
(CWA) to first-order logic ontologies [
These Adimen SUMO problems are challenging even for highly optimised theorem provers. Usually theorem provers use selection techniques for this kind of problems, which try to select the formulas relevant for a given proof task from the knowledge base.
In all our experiments, we use the theorem prover E with a timeout of 10 seconds. We call it with diferent parameters combinations2: formulas.
Fig. 3 shows the number of proofs found for the diferent E configurations we considered. We see that the configuration with no parameters finds the highest number of proofs with 129 proofs, which is not surprising because of the way the problems were chosen. Furthermore, we see that the number of proofs found using the configuration with the auto parameter (121 proofs), as well as the configurations using the similarity-based weights, results in slightly fewer proofs being found (122 for all configurations of E using similarity-based symbol weights without auto parameter).
Since our approach aims at influencing the selection of the clause for the next inference step in such a way that the selected clause fits the thematic context of the goal, the number of processed clauses is of particular interest for the evaluation. This number is usually much larger than the number of clauses in the actual proof. The smaller the number of processed clauses, the more targeted the proof. Ideally, the number of processed clauses is equal to the number of clauses in the proof, and no unnecessary conclusions have been drawn.
Fig. 4 shows the average number of clauses processed by the diferent E configurations we considered. We can see that E with the auto parameter processes the most clauses. The number of clauses processed for E without any parameter and E using the similarity-based weight for only the symbol most similar to the goal are comparable. Again, this is not surprising as one would not expect a single symbol weight to have much influence. The configurations of E using similarity-based symbol weights for the 5 to 25 symbols most similar to the goal are comparable in terms of the number of clauses processed. The best configuration seems to be the one with 10 symbol weights. Compared to the conifguration using E without parameters, the configurations using symbol weights for 5 to 25 symbols process only about half the number of clauses. This shows the usefulness of the presented approach. We have also investigated whether the combination of the auto parameter and the symbol weights for the 10 symbols most similar to the goal has advantages. However, we observe that the number of clauses processed by this configuration is comparable to the use of the auto parameter alone.
Fig. 5 shows a direct comparison of the number of processed clauses for the E configuration without using any parameters and the E configuration using the similarity based weights for the 10 symbols most similar to the proof goal. We observe that the majority of the points in Fig. 5 are above the first bisector. Thus, we see that for most problems the number of clauses processed could be reduced by using the similarity-based symbol weights.
Fig. 6 shows a direct comparison of the number of clauses processed for the E configuration using the auto parameter and the E configuration using the similarity-based weights for the 10 symbols most similar to the proof goal. The vast majority of the points in Fig. 6 are above the first bisector. Many are also at a large distance from it. For example, we see a cluster of problems for which E with auto-parameter processed around 17500 clauses, but for which the configuration with symbol weights processed only about 7500 clauses. This illustrates that the use of similarity-based symbol weights was able to drastically reduce the number of clauses processed in many cases.
Since we observe large diferences in the number of clauses processed, the question arises whether the sizes of the proofs found also difer. In Fig. 7 we see the direct comparison of the sizes of proofs constructed with E using the auto parameter with the sizes of proofs constructed with E and the similarity-based symbol weights of the 10 symbols most similar to the goal. We observe that the proofs are often smaller when E was using similarity-based symbol weights. In future work, we plan to analyze the diferent proofs in more detail to determine how they difer and whether the shorter proofs are easier to understand.
Fig 8 shows the corresponding comparison, where we compared the proof size for proofs constructed with E without any parameters with the proof sizes of proofs constructed with E and the similarity-based symbol weights of the 10 symbols most similar to the goal. Here we observe that the size of some proofs is smaller using the configuration of E with symbol weights. However, the diferences are not as large as in Fig 7, and in most cases the sizes do not difer.
In a second set of experiments, we selected formulas from
500 of the Adimen SUMO CWA problems with the SInE
selection [
Since the E configuration, which combines symbol weights with the auto parameter, performed poorly in our ifrst experiments, we do not include this configuration in the following experiments.
In Fig. 9 we can see that nearly the same number of proofs can be found by the diferent configurations of E. The low number of around 200 found proofs can be explained by the incompleteness of the SInE selection.
Fig. 10 shows the average number of clauses which were processed during proof construction. We observe that the average number of clauses processed by E with the auto parameter is the highest value with 1213.85. The average number of clauses processed by E without parameters is slightly lower with 1103.68. In comparison, E with the 10 best similarity-based symbol weights processes on average only 473.10 clauses, which is much less.
Fig. 10 shows that the similarity-based weights lead to a reduction in the average number of clauses processed. However, it is not clear how this reduction is distributed across the individual problems. Therefore, in Fig. 11 we directly compare the number of processed clauses of E without any parameters (y-axis) with the number of processed clauses of E with the symbol weights of the 10 symbols most similar to the goal (x-axis). For each proof we see a point in the graph. We observe that, with a few exceptions, the number of processed clauses is significantly lower for the E configuration with goal similarity-based symbol weights than for E without parameters.
As in the previous experiments, we also compare the sizes of the found proofs. Fig. 12 and Fig. 13 show the corresponding results. We observe that for the problems considered in the experiments with preselected formulae, the diferences in proof size are not that large. There are many proofs where the proof sizes are the same. Furthermore, for both E configurations, there are proofs where the proof size is smaller and proofs where the proof size is larger. Comparing the proof sizes of E without any parameters with the configuration using 10 similarity-based symbol weights, we observe slightly more cases where the proof size is lower using symbol weights. But the diferences are really small.
Compared to the experiments with the non preselected formulas (see Fig. 7 and Fig. 8), the diferences in the proof sizes are much smaller here. A possible explanation for this could be the pre-selection of formulae with SInE. This preselection means that there are significantly fewer formulae available, which considerably limits the choices when constructing the proofs. We intend to investigate this in more detail in future work.
In this paper we have developed an approach to clause selection in automated theorem provers that aims to make the selection of the clause for the next inference step more goal-directed. The approach is based on the assumption that symbol names in knowledge bases have meaningful names that can be mapped to natural language words. If this assumption is correct, techniques from natural language processing can be used to determine the similarity between the proof goal and the symbols in the knowledge base. These similarities are then used to derive symbol weights that guide the selection of clauses for the next inference step. The approach has been implemented and evaluated using the theorem prover E. Our experimental results show a significant reduction in the number of clauses processed during proof construction, indicating a more goal-directed and eficient proof process.
In our experiments, we further observed that the use of similarity-based symbol weights has an impact on proof size (especially compared to the configuration using the auto parameter). In future work, we would like to analyze the diferences in the proofs we found in more detail and investigate whether there are also diferences in the comprehensibility of the proofs.