We discuss what is known about implementations of logical systems whose syntax is either a small fragment of natural language, or alternatively is a formal language which looks more like natural language than standard logical systems. Much of this work in this area is now carried out under the name of natural logic. Just as in modal logic or description logic, there are many systems of natural logic; indeed, some of those systems have features reminiscent of modal logic and description logic. For the most part, quantification in natural logics looks more like description logic or term logic (i.e., syllogistic logic) than first-order logic. The main design criteria for natural logics are that (1) one can be able to use them to carry out significant parts of reasoning; and (2) they should be decidable, and indeed algorithmically manageable. All of the questions that we ask about the implementation of any logics can be asked about natural logics. This paper surveys what is known in the area and mentions open questions and areas.
The natural logic program talks:
This is a summary of the program of natural logic, taken from papers and 1. Show the aspects of natural language inference that can be modeled at all can be modeled using logical systems which are decidable. 2. To make connections to proof-theoretic semantics, and to psycholinguistic studies about human reasoning. 3. Whenever possible, to obtain complete axiomatizations, because the resulting logical systems are likely to be interesting, and also complexity results. 4. To implement the logics, and thus to have running systems that directly work in natural language, or at least in formal languages that are closer to natural language than to traditional logical calculi. 5. To re-think aspects of natural language semantics, putting inference at the center of the study rather than at the periphery.
F O2 P e a n o -F r e g e A ristotle
S≥
S† S
F OL R† R
R∗†(tr)
R∗(tr) R∗† R∗
Church -Tu
ring
R∗†(tr, opp) R∗(tr, opp) first-order logic
† adds full N -negation R∗(tr) + opposites R∗ + (transitive)
comparative adjs R + relative clauses S + full N -negation R = relational syllogistic S≥ adds |p| ≥ |q|
S: all/some/no p are q
Goal (4) is the topic of this paper, but goal (3) is also relevant. Most of the work on natural logic has pursued goals (1) and (3). Concerning (3), there are now a myriad of logical systems which are complete and decidable and which have something to do with natural language. Some of them are listed in a chart in Figure 1. Here is a guide to those systems, starting with the three boundary lines.
The line called “Church-Turing” at the top separates the logics which are undecidable (above the line) from those which are not. FOL is first-order logic. FO2 is two-variable first-order logic; this is well-known as a decidable logic. This logic is not directly relevant to our study, but since many logics can be expressed in FO2, they inherit the decidability.
The line called Peano-Frege separates the sub-logics of FOL (to the right) from the one logic on this chart which is not sub-logic of FOL. These logics are “non-classical”, being unrelated to FOL. And they deal with “quantity” (but not “quantification” in the usual sense). I would hope that people in the ARQNL community will find them interesting. I discuss them in Section 3. It should be mentioned that there are other logics to the left of the Peano-Frege boundary. Space didn’t permit a larger display.
The line called Aristotle separates the logics with a syllogistic formulation from those which lack such a formulation. This line is much less “firm” than the other lines, for two reasons. First, there is no accepted definition of what a syllogistic proof system even is. For us, it means a logic with a finite set of rules, each of which is essentially a Horn clause, and also allowing reductio ad absurdum. The second noteworthy feature of the Aristotle line is that sometimes a logic L which is provably above the line has a super-logic L0 which is below the line. That is, sometimes, adding vocabulary to a logical system enables one to find a syllogistic presentation. This feature has made some doubt whether there is much of a point to the Aristotle boundary. Be that as it may, there certainly is work to do in clarifying the line which we name for Aristotle. Specific logics We go into details on the syntax and semantics of some of the logics in the chart, starting with S at the bottom. This is the classical syllogistic. The syntax starts with a collection of nouns; we use lower-case letters like p, q, x, and y for nouns. The syntax just has sentences of the form all x are y, some x are y, and no x are y. These sentences are not analyzed as usual in first-order logic. The sentences of S do not involve recursion. Also, there are no propositional connectives in this tiny logic.
For the semantics, we consider models M consisting of a set M and subsets [[x]] ⊆ M for all nouns x. We then declare
M |= all x are y iff [[x]] ⊆ [[y]] M |= some x are y iff [[x]] ∩ [[y]] 6= ∅
M |= some x are y iff [[x]] ∩ [[y]] 6= ∅ Please note that we are not rendering sentences like all x are y into first-order logic. Instead, we are giving a semantics to syllogistic logic.
Then we ask some very traditional questions. For a set Γ of sentences in this language, and for another sentence ϕ, we say that Γ |= ϕ if every model M which satisfies all sentences inΓ also satisfies ϕ. This is the notion of semantic consequence from logic. There is a matching proof system, defining a relation Γ ` ϕ. For example, here are two rules all x are y all y are z all x are z
BARBARA all x are y some x are z some y are z
DARII One feature of the logics in this area is that frequently there are many rules.
As expected, there is a Completeness Theorem. For the purposes of this paper, the important point
is that the relation Γ ` ϕ (for Γ a finite set) is in NLOGSPACE (see [
We return to the chart to briefly discuss the other logics. The logic R above S adds transitive verbs (such as see, love, and hate), interpreted as arbitrary binary relations on the universe. The syntax of R is bit complicated, so we won’t go into full details. But the following are examples of sentences of it: all x see some y and no x see all y. In English, sentences like the first of these are ambiguous, and to make a proper logical study we take just the standard reading, where all has wide scope. Moving up, R∗ adds terms in a recursive way to R. We present the syntax of two related systems formally in Section 2. So all (see all (love all dogs)) (hate some cat) is a sentence of R∗; its usual rendering in English would be all who see all who love all dogs also hate some cat. R∗(tr) adds comparative adjectives such as taller than, interpreted again as binary relations, but insisting that those interpretations be transitive (hence the tr) and irreflexive. Adding converse relations such as shorter than takes us up to R(tr, opp). For example, a logical rule in this logic would be to assume all x are taller than all y and conclude all y are shorter than all x.
The logics with the dagger † add full negation on all nouns. So in S†, one can say some non-x are non-y. This sentence is not part of the classical syllogistic. We interpret “non” in a classical way, so [[non-x]] = M \ [[x]]. If one wanted to be “non-classical” here, one certainly could.
More on natural logic may be found in the Handbook article [
Complexity A great deal is known about the complexity of the consequence relation Γ ` ϕ. The
logics at the bottom of the chart, S, S†, R, and S≤ are in NLOGSPACE (see [
Of special interest for implementations Most of these logics have not been implemented, but of course it would be interesting to do so. Further, we do not even have approximation algorithms for these logics. All of this would be good to do. The smallest logics in the chart have been implemented, and there are some interesting features. First, once a logic has negation, contradictions are possible. Perhaps the most natural way to handle these is by adding reductio ad absurdum to the proof system. However, this complicates the proof search in a big way. And in general, allowing reductio ad absurdum in syllogistic logics raises the complexity beyond PTIME. To circumvent reductio ad absurdum, one can use ex falso quodlibet. This principle allows us to derive an arbitrary conclusion from a contradiction.
Another interesting thing about the implementations of logics “low in the chart” is that completeness and model-building are closely related. Here is how this works. Suppose we are given Γ and ϕ and want to know whether or not Γ ` ϕ; if this hold, we want a proof, and if not, we want a counter-model. One proves a kind of conservativity fact about these logics: if there a derivation of Γ ` ϕ, then there is one with the property that all terms in it are subterms of the premises or of the conclusion. This is a distant relative of the subformula property, and it make proof search efficient. One simply generatesall of the consequences of Γ and looks for ϕ. If ϕ is not found, then the sentences which are consequences of it usually gives us a model in a canonical way. The upshot is that one does not need a separate model finder.
Predecessors There are two main predecessor areas to the work that I am discussing, one from
Artificial Intelligence, the other from Philosophy. In AI, there is a long tradition of thinking about inference
from language. Sometimes this is even taken as a primary problem of natural language processing. But
most of that work does not propose small fragments the way we are doing it here. Still, some early
papers in the area do work (in effect) with fragments, such as [
For the semantics, we interpret nouns by subsets of the universe M of a model (as in the previous section), verbs by relations on M , noun and verb complements classically, and then inductively interpret terms by [[r all x]] = [[r some x]] = {n ∈ M : for all m ∈ [[x]], (m, n) ∈ [[r]]} {n ∈ M : for some m ∈ [[x]], (m, n) ∈ [[r]]}
In terms of the complexity, the consequence relation for R∗ is CO-NP COMPLETE (see [
It is possible to construct natural deduction style proof systems for this logic and related ones [
nouns verbs unary literal binary literal term R∗ sentence Variables p, q, x, y s l r c, d ϕ
p | p¯
s | s¯
l | r some c | r all c
some b+ d | some d b+ | all b+ d | all d b+
nobody has investigated or implemented proof search for the logics in [
Wennstrom [
Wennstrom also implemented all three strategies. He worked in miniKanren [
Other tableau systems and implementations Wennstrom [
This section discusses a topic that I think could be of interest at ARQNL, the logic S≤. This logic adds
to syllogistic logic some decidedly non-first order semantics, but with a simple syntax. We add to the
classical syllogistic two extra kinds of sentences: there are at least as many x as y, and there are more
x than y. The semantics is just what one would expect: use set theoretic models, and use the standard
notion of cardinality. In this discussion, we are going to restrict attention to finite models, since this is
most in the spirit of the subject. (But one can work on infinite sets; see [
Again, we should emphasize that these logical systems do not have quantifiers; for that matter, they do not have propositional connectives ∧, ∨, or ¬. The only sentences are the ones mentioned. In a sense, they are the cognitive module for reasoning about size comparison of sets, in the simplest possible setting.
It might come as a surprise, but reasoning about the sizes of sets does not by itself require a “big” logical system.
There is a complete proof system. It has 22 rules and so we won’t present them all. But let us show several of them: all p are q there are at least as many p as q all q are p
(CARD-MIX) there are more q than p there are more p than q (MORE-ANTI) ∃≥(p, p) ∃≥(q, q) ∃≥(p, q) (HALF) (CARD-MIX) requires that the universe be finite. In the last two rules, we use x as an abbreviation of non-x. In (CARD-MIX), we use ∃≥(x, y) as an abbreviation of there are at least as many x as y. So, here is an explanation of the (HALF) rule. If there are at least as many p as non-p, then the p’s are at least half of the universe. So if there are at most as many q as non-q, then q’s have at most half of the elements in the universe.
As we mentioned before, the logic does not have reductio ad absurdum, but it has the related principle of ex falso quodlibet. In more detail, reductio ad absurdum is an admissible rule, but it is not needed. One can use the following weaker forms ∃≥(p, q) ∃>(q, p) ϕ (X-CARD) some p are q no p are q ϕ (X) These basically say that anything follows from a contradiction. It is open to construct and implement meaningful natural logics which are paraconsistent. 3.1 Implementation The logic has been implemented in Sage1. This implementation is on the cloud, and the author shares it. See https://cocalc.com/. Other syllogistic logics have been implemented in Haskell.
For example, one may enter in the CoCalc implementation the following.
assumptions= [’All non-a are b’, ’There are more c than non-b’, ’There are more non-c than non-b’, ’There are at least as many non-d as d’, ’There are at least as many c as non-c’, ’There are at least as many non-d as non-a’] conclusion = ’All a are non-c’ 1As a programming language, Sage is close to Python. It is mainly associated with CoCalc (https://cocalc.com/); CoCalc incorporates a lot of mathematical software, all of it open source. It provides Jupyter notebooks and course management tools.
We are asking whether the conclusion follows from the assumptions. This particular set of assumptions is more complicated than what most people deal with in everyday life, even when they consider the sizes of sets. This is largely due to the set complements.
As we mentioned, the proof search algorithm basically gives counter-models to non-theorems. In the case of this logic, this fact takes special work. Returning to our example, the result appears instantly. (That is, for a set of assumptions of this type, the algorithm takes less than one second, running over the web.) We get back
We take the universe of the model to be {0, 1, 2, 3, 4, 5} noun semantics a b c d {2, 3} {0, 1, 4, 5} {0, 2, 3} {}
So the system gives the semantics of a, b, c, and d as subsets of {0, . . . , 5}. Notice that the assumptions are true in the model which was found, but the conclusion is false.
Here is an example of a derivation found by our implementation. We ask whether the putative conclusion below really follows:
All non-x are x Some non-y are z
There are more x than y In this case, the conclusion does follow, and the system returns a proof.
2 All y are x One 1 3 All non-x are x 4 All non-y are x
One 3
What about propositional logic? Propositional connectives make complex sentences from sentences. We did not add the propositional connectives to this particular logic to keep the complexity low, and also to illustrate the idea that one should find special-purpose logics for topics like sizes of sets. However, one certainly could add in the connectives. The resulting logic has been explored, but we lack the space to expand on this. It is open to implement such logics, or to connect the work to SAT solvers. 4
The ultimate goal of the work that I am reporting on is to have working systems that do inference in natural language, or something close. It is clear that the program of natural logic that I have discussed, where one works with ever more complicated fragments, has a long way to go. I hope that some of the languages which we have found so far will be of interest even to people outside of the area. It is equally clear that for natural language inference itself, the method of fragments has its limitation: to get started with it, one must have a language with a clear syntax and semantics.
Readers of this paper will be surprised by the title of this section. The standard assumptions in all areas of formal logic is that logical language come with a precisely defined semantics and especially a precisely defined syntax. This syntax is usually trivial in the sense that parsing a logical language is a non-issue. For natural language, the opposite is true. Parsing is a complex matter. (The semantics is even worse, of course.)
This section loosen this assumption in connection with sizes of sets. It is based on [
We are interested in polarity marking, as shown below:
More dogs↓ than cats↑ walk↓ Most↑ dogs= who= every= cat= chased= cried↑
Every dog↓ scares ↑ at least two↓ cats↑ The ↑ notation means that whenever we use the given sentence truthfully, if we replace the marked word w with another word which is “ ≥ w” in an appropriate sense (see below for an example), then the resulting sentence will still be true. So we have a semantic inference. The ↓ notation means the same thing, except that when we substitute using a word ≤ w, we again preserve truth. Finally, the = notation means that we have neither property in general; in a valid semantic inference statement, we can only replace the word with itself rather than with something larger or smaller. We call ↑ and ↓ polarity indicators.
For example, suppose that we had a collection of background facts like cats ≤ animals, beagles ≤ dogs, scares ≤ startles, and one ≤ two. This kind of background fact could be read off from WordNet, thought of as a proxy for word learning by a child from her mother. In any case, our ↑ and ↓ notations on Every dog↓ scares ↑ at least two↓ cats↑ would allow us to conclude Every beagle startles at least one animal. In general, ↑ notations permit the replacement of a “larger” word and ↓ notations permit the replacement of a smaller one.
The goal of work on the monotonicity calculus such as [
We must emphasize that [
My feeling is that people interested in the topics like “proof calculi, automated theorem proving systems and model finders for all sorts of quantified non-classical logics” will find much to like in the topic of natural logic. Although the systems in the area will be new, and so on a technical level one would be tempted to see differences, there is a close ideological kinship. Both are about automated reasoning, both are willing to consider new systems of various types.
We close with a review of the main points in this survey paper for people in the area.
First, first-order logic (FOL) is not the only approach to the topic of quantification: extended syllogistic logics in the natural logic family offer an alternative. That alternative is not nearly as well-studied as FOL. There are numerous computational problems related to extended syllogistic logics, and there are also a few working systems.
Even if one prefers FOL for the things that it can do, FOL cannot handle some manifestly secondorder phenomena such as reasoning about the sizes of sets. We mentioned logics which can cover this reasoning and showed a simple implementation.
An old effort in AI is to study inference from text using automated logic. This topic is currently under revision, due to the connection with the monotonicity calculus. From the point of view of this paper, automating monotonicity inference is an important next step in doing automated reasoning concerning quantification.