The area of commonsense reasoning aims at the creation of systems able to simulate the human way of rational thinking. This paper describes the use of automated reasoning methods for tackling commonsense reasoning benchmarks. For this we use a benchmark suite introduced in the literature. Our goal is to use general purpose background knowledge without domain speci c hand coding of axioms, such that the approach and the result can be used as well for other domains in mathematics and science. We furthermore report about a preliminary experiment for nding most plausible results.
2. The grass was cut. 13: The pond froze over for the winter. What happened as a RESULT?
For a long time, no benchmarks in the eld of commonsense reasoning were
available and most approaches were tested only using small toy examples. Recently,
this problem was remedied with the proposal of various sets of benchmark
problems. There is the Winograd Schema Challenge [
Even though for the COPA challenge capabilities for handling natural language are necessary, background knowledge and commonsense reasoning skills are crucial to tackle these problems as well, making them very interesting to evaluate cognitive systems. All existing systems tackling the COPA benchmarks focus on linguistic and statistical approaches by calculating correlational statistics on words.
Another set of benchmarks is the Triangle-COPA challenge2 [15]. This is a
suite of one hundred logic-based commonsense reasoning problems which was
developed speci cally for the purpose of advancing new logical reasoning
approaches. The structure of the problems is the same as in the COPA Challenge
however the problems in the Triangle-COPA challenge are not only given in
natural language but also in rst-order logic. Approaches to tackle the
TriangleCOPA challenge can be found in [15], [
In this paper we focus on the COPA challenge. However most parts of our approach can be used for the problems of the Triangle-COPA challenge as well. 1 Available at
dev.txt. 2 Available at https://github.com/asgordon/TriangleCOPA/.
http://people.ict.usc.edu/ gordon/downloads/COPA-questionsCOPA Problem formulae for problem description and two alternatives
Find Synonyms/ Hypernyms based on problem signature WordNet
Create Connecting Formulaes based on problem signature WordNet OpenCyc
Select Axioms from OpenCyc based on connecting formulae use SInE and k-NN
Create Background
Knowledge
combine
connecting formulae
selected axioms
As described afore, the creation of a system for commonsense reasoning requires
the combination of techniques from di erent areas [
Even gathering appropriate background knowledge for a speci c benchmark
problems requires the use of di erent techniques. Figure 2 depicts the di erent
steps necessary to gather suitable background knowledge for a given COPA
problem. When combining an example problem with background knowledge,
several problems have to be solved:
1. If the problem is given in natural language it has to be transformed into a
logical representation.
2. The predicate symbols used in the formalization of the example are unlikely
to coincide with the predicate symbols used in the background knowledge.
3. The background knowledge is too large to be considered as a whole.
The rst problem can be solved using the Boxer [
We address the second problem by using WordNet [16] to nd synonyms and
hypernyms of the predicate symbols used in the formalization of the example.
Note that the formalization of the example consists both of the formulae
describing the situation as well as the formulae for the two alternatives. In the
next step, predicate symbols used in OpenCyc [
The third problem is addressed using selection methods. For this, all predicate
symbols occurring in the formalization of the example and in the connecting set
of formulae are used. As selection methods, SInE as well as k-NN as they are
implemented in the E.T. metasystem [
The COPA challenge contains two di erent categories of problems. In the rst category, a sentence describing an observation is given and it is asked for COPA Problem formulae for problem description
Background Knowledge
Hyper
Model
Machine Learning
More plausible alternative is ...! COPA Problem formulae for problem description two alternatives the cause of this observation. Probem no. 1 given in Figure 1 is an example for a question in this category. In this case, the task is to determine which of the two provided alternatives is more likely to be the cause of the observation described in the sentence. We call this category the cause category.
In the other category a sentence describing an observation is given and it is asked about the result of this observation. In this case the task is to decide which of the two alternatives is more likely to result from the situation described in the sentence. We call this second category the result category. Even thought the category does not in uence the way the background knowledge is selected, it is necessary to use di erent approaches for the two categories when combining this background knowledge with automated reasoning methods.
Figure 3 depicts how to tackle a problem from the result category in
order to determine the more plausible alternative result. Please note that the
selected background knowledge does not only consist of axioms stemming from
the knowledge base used as a source for background knowledge but also contains
the connecting formulae which were created as depicted in Figure 2. First, this
background knowledge is combined with the logical formulae representing the
description of the benchmark problem. The resulting set of formulae serves as
input for a theorem prover, in our case the Hyper prover [
When dealing with problems in the cause category, we have to solve two reasoning problems. Figure 4 depicts the work ow for this category. In the rst step, the background knowledge is combined with the logical formulae representing the rst alternative. The resulting set of formulae serves as an input for the Hyper theorem prover, which constructs a model M1. In the second step, the background knowledge is combined with the logical formulae representing the second alternative and the resulting set is passed to Hyper which constructs a model M2. Then both models are inspected in order to determine which of the two models is closer to the formulae representing the description of the problem. This inspection of the models is still future work. We are planning to accomplish this with the help of machine learning. 4
We created a prototypical implementation of the work ow depicted in the previous Section. Our implementation is able to take a problem from the COPA challenge, selects appropriate background knowledge, generates a connecting set of formulae and feeds everything into Hyper. The machine learning component inspecting the generated model is in an experimental phase and is addressed in Section 5 below. 4.1
We performed a very preliminary experiment to test this work ow. From the COPA benchmark set we selected 100 problems. Feeding these examples into the work ow resulted nally in 100 prove tasks for Hyper and we learned a lot | about problems which have to be solved. Hyper found 37 proofs and 57 models; the rest are time-outs. One problem we encountered is that some contradictions leading to a proof are introduced by selecting too general hypernyms from WordNet. E.g. the problem description of example 1 given in Figure 1 is transformed into the following rst-order logic formula by Boxer: ^ vcast(B) ^ nshadow(C) ^ nbody(D) ^ rof (D; C) ^ nperson(C)))): From WordNet the system extracted the information, that `individual' is a hypernym of `shadow' and `collection' is a hypernym of `person' leading to the two connecting formulae: 8X(nshadow(X) ! individual(X)) 8X(nperson(X) ! collection(X)): The selection from OpenCyc resulted among others in the axiom 8X:(collection(X) ^ individual(X)):
These formulae together lead to a closed tableau |a proof of unsatis ability| because of a contradiction between a shadow which stems from a person, whereas WordNet gives that a shadow is an individual, a person is a collection and together with the Cyc axiom we get the contradiction. This has nothing to do with one of the alternatives that the sun was rising or the grass was cut.
To remedy this problem, we use a tool called KNEWS [
The one contradiction which still occurred in the second experiments stems directly from inconsistencies in the knowledge base used as source for background knowledge (in our case OpenCyc). E.g. the two formulae 8Xspeed (fqpquantityfnspeed (X)) 8X:speed (X) were selected immediately leading to a contradiction which again does not have to do anything with the two alternatives about the sun rising or the grass being cut. This illustrates that we have to nd a way to deal with inconsistent background knowledge. 4.2
Another challenge when combining problems with background knowledge is the lack of appropriate background knowledge. Consider the example number 13 3 Many thanks to Valerio Basile for being so kind to share his tool for disambiguation.
The tool is available at https://github.com/valeriobasile/learningbyreading 4 Available at: http://babelfy.org 5 Available at: http://babelnet.org from the COPA challenge which we presented in Figure 1. The background knowledge selected for this example contains formulae on skating like for example:
8X(skateboard (X) ! device usercontrolled (X)) and even on iceskating
8X(iceskate(X) ! isa(X; c iceskate)): However the information, that freezing of a pond in winter results in a surface suitable for skating, is missing. This explains, why not enough inferences were performed and therefore the constructed model does not contain information on ice skating.
In general there are two possible explanations for the lack of inferences: 1. The way the bridging between the vocabulary used in the benchmark problem and the vocabulary used in OpenCyc is still very prototypical. We heavily rely on Boxer's output to construct the connecting formulae. However sometimes Boxer marks adjectives as nouns and vice versa which misguides the search for synonyms and hypernyms in WordNet. We are planning to improve this by updating to the most recent Boxer version. 2. Currently, we are only using OpenCyc as a source of background knowledge.
However this is not su cient. We are planning to remedy this situation by
including di erent other sources of background knowledge like ConceptNet
[
winter {CausesDesire ! skate SUMO is a very large upper ontology containing knowledge which could be helpful as background knowledge. For example SUMO contains the knowledge, that icing is a subclass of freezing which could be helpful for our benchmark problem. One very interesting point is that there is a mapping from SUMO to WordNet synsets. This will be very helpful during the creation of formulae bridging from the vocabulary of the benchmark problem and the synonyms and hypernyms to the vocabulary used in SUMO. Due the fact that the structure of problems of the Triangle-COPA challenge is very similar to the structure of the problems of the COPA challenge, our approach can be used for the Triangle-COPA challenge without much changes. Since the problems given in the Triangle-COPA challenge consist of descriptions of small episodes on interpersonal relationships, the HEO and EMO ontology, both containing information on human emotions, provide useful background knowledge.
When using the automated reasoning system Hyper within the Deep Question
Answering system LogAnswer ([
Like depicted in Figure 4, for the cause category two models are generated. Each of these models corresponds to knowledge which was derived using one of the two alternatives. In future work we are planning to use these two models together with the formulae representing the description of the situation in order to nd out which alternative is the more plausible one. For this we are planning to use machine learning techniques to determine if the formulae describing the situation is rather a logical consequence of the rst or the second model. Up till now, we focused our research on the result category which is why we cannot provide further results for the cause category.
In the sequel we describe how to use machine learning techniques for problems of the result category and give results of a rst experiment. The situation is such that we have a problem description P , in our COPA example above the logical representation of `The pond froze over for the winter.' together with two possible answers E1 and E2.
In the work ow described until now, we constructed a tableau for P [ BG, where BG is the background knowledge as discussed in Section 3. This tableau may contain open and closed branches. The closed branches are parts of a proof and the open branches either are a model (and hence no closed tableau exists) or they are only open because of a time-out for this branch. With the help of this tableau, we try to decide which of the two alternatives E1 and E2 is `closer' to a logical consequence of P [ BG. In other words we try to decide if the constructed tableau can be rather closed by adding alternative E1 or by adding alternative E2.
In the LogAnswer system we gave the two answers to humans to decide which is closer to a logical consequence and we then used this information to train a machine learning system. For the scenario of the COPA and TriangleCOPA benchmarks we designed a preliminary study, which aims at using the information about the tableau created for P [ BG together with information from formulae of the problem and the background P [ BG to generate examples for training.
We restricted our preliminary study to propositional logic and analyzed tableaux created by the Hyper prover for randomly created sets of clauses. For each pair of propositional logic variables p and q occurring in a clause set, we were interested in the question if p or q is `closer' to a logical consequence. We reduced this question to a classi cation problem: for each pair of variables p and q, the task is to learn if p < q, p > q or p = q, where p < q means, that q is `closer' to a logical consequence than p and p = q means that p's and q's `closeness' to a logical consequence is equal. Consider the following set of clauses: p0 p4 ! p2 _ p3 _ p7 p0 ! p4 p3 ^ p5 ! p6 p3 ^ p5 ^ p8 ! p1
p2 ! ? Clearly, p0 and p4 are logical consequences of this clause set. Therefore p0 = p4 and p0 > q for all other variables q. On the other hand, from p2 it is possible to deduce a contradiction, which leads to p2 < q for all other variables q. Comparing p6 and p1 is a little bit more complicated. Neither of these variables is a logical consequence. However assuming p3 and p5 to be true, allows to deduce p6 but not p1. In oder to deduce p1 it is necessary to assume not only p3 and p5 to be true but also p8. Therefore p1 < p6.
To use machine learning techniques to classify these kind of examples, we represent each pair of variables (p; q) as an instance of the trainings examples and we provide the information, which of the three relations <; >; = is correct for p and q. Each of these instances contains 22 attributes. Some of these attributes represent information on the clause set like the proportion of clauses with p or q in the head as well as rudimentary dependencies between the variables in the clause set. In addition to that, we determine attributes representing information on the hypertableau for the set of clauses like the number of occurrences of p and q in open branches. Furthermore, we determine an attribute mimicking some aspects of abduction by estimating the number of variables which have to be assumed to be true in order to deduce p or q respectively. This allows us to perform comparisons like the one between p1 and p6 in the above example. Of course we also take into account whether one of the two variables is indeed a logical consequence.
For the rst experiments, 1,000 sets of clauses each consisting of about 10
clauses and containing about 12 variables were randomly generated. These sets of
clauses were analyzed and used to create a training set. For each pair of variables
occurring in one of the clause sets, an instance was generated. All in all this led to
123,246 examples for training purposes. In these examples, the classes < and >
each consists of 57,983 examples and the class = of 7,280 examples. We used the
J48 tree classi er implemented in the Weka [
We are aware that automatically classifying the test set might introduce errors into the test set and therefore tampers the results. Since it is very laborintensive to manually generate test data, we only created test instances from two clause sets manually. For this much smaller test set, depending on the classi er used, we reached percentages of correctly classi ed instances of up to 80 %.
In the next step, we are planning to expand our experiments to clause sets P [ BG and alternatives E1 and E2 given in rst-order logic. When creating the instances of the trainings examples for rst-order logic, attributes di erent from the ones in the previous experiment have to be considered. For example it is not su cient to have an attribute indicating the proportion of open branches containing a certain subgoal of E1. Since both the open branch and the subgoal of E1 are given in rst-order logic, uni cation has to be taken into account. In this case the proportion of open branches containing an atom which can be uni ed with one of the subgoals of E1 constitutes an interesting attribute. Another interesting attribute would take relaxation into account: for an open branch not containing any atom which can be uni ed with one of the subgoals of E1, it is interesting if this branch contains an atom which can be uni ed with a generalization of one of the subgoals in E1. This attribute allows us to mimic the relaxation like it is used in the LogAnswer system. 6
We presented an approach to tackle benchmarks for commonsense reasoning. This approach relies on large existing ontologies as a source for background knowledge and combines di erent techniques like theorem proving and machine learning with tools for natural language processing. With the help of a prototypical implementation of our approach, we conducted some experiments with problems from the COPA challenge. We presented our experiences made in these experiments together with possible solutions for the problems occurring in the examples considered.
Future work aims at the integration of additional sources of background knowledge as well as improving the bridging between the vocabulary used in the benchmarks and the background knowledge. 15. N. Maslan, M. Roemmele, and A. S. Gordon. One hundred challenge problems for logical formalizations of commonsense psychology. In Twelfth International Symposium on Logical Formalizations of Commonsense Reasoning, Stanford, CA, 2015. 16. G. A. Miller. WordNet: a lexical database for english. Commun. ACM, 38(11):39{ 41, 1995. 17. A. Moro, A. Raganato, and R. Navigli. Entity Linking meets Word Sense Disambiguation: a Uni ed Approach. Transactions of the Association for Computational Linguistics (TACL), 2:231{244, 2014. 18. R. Navigli and S. P. Ponzetto. BabelNet: The automatic construction, evaluation and application of a wide-coverage multilingual semantic network. Arti cial Intelligence, 193:217{250, 2012. 19. I. Niles and A. Pease. Towards a standard upper ontology. In Proceedings of the international conference on Formal Ontology in Information Systems-Volume 2001, pages 2{9. ACM, 2001. 20. A. Pease. Ontology: A Practical Guide. Articulate Software Press, Angwin, CA, 2011. 21. M. Roemmele, C. A. Bejan, and A. S. Gordon. Choice of plausible alternatives: An evaluation of commonsense causal reasoning. In AAAI Spring Symposium: Logical Formalizations of Commonsense Reasoning, 2011.