Applied Temporal Analysis: A Complete Run of the F ra C a S Test Suite (2021)

Abstract: In this paper, we propose an implementation of temporal semantics that translates syntax trees to logical formulas, suitable for consumption by the Coq proof assistant. The analysis supports a wide range of phenomena including: temporal references, temporal adverbs, aspectual classes and progressives. The new semantics are built on top of a previous system handling all sections of the FraCaS test suite except the temporal reference section, and we obtain an accuracy of 81 percent overall and 73 percent for the problems explicitly marked as related to temporal reference. To the best of our knowledge, this is the best performance of a logical system on the whole of the FraCaS.

## introduction the semantics of tense and aspect has been a long standing issue in the study of formal semantics since the early days of montague grammar and a number of different ideas have been put forth to deal with them throughout the years. recent proposals include the works of the following authors: @xcite ; @xcite ; @xcite ; @xcite ; @xcite . the semantics of tense and aspect have been also considered in the study of natural language inference (nli). the various datasets for nli that have been proposed by the years contain examples that have some implicit or explicit reliance on inferences related to tense and aspect. one of the early datasets used to test logical approaches, the fracas test suite @xcite ) contains a whole section dedicated to temporal and aspectual inference (section 7 of the dataset). this part of the fracas test suite has been difficult to tackle. that is, so far, no computational system has been capable to deal with it in its entirety: when authors report accuracy over the fracas test suite they skip this section. in fact, they also often skip the anaphora and ellipsis sections, the exception being the system presented by @xcite , which includes support for anaphora and ellipsis but still omit the temporal section. 1 in this paper, we take up the challenge of providing a computationally viable account of tense and aspect to deal with the section 7 of the fracas test suite. our account is not meant to be a theoretically extensive account of tense and aspect, but rather an account that is driven by the need to cover the test suite in a way that is general enough to capture the test suite examples, while still covering the rest of the fracas test suite. the account is evaluated on the entailment properties of various temporal and aspectual examples, as given by the test suite. as such, we are not getting into the discussion of how tense and aspect might affect grammaticality or infelicitousness of various sentences. we assume that the sentences of the fracas suite are syntactically and semantically correct, and strive to produce accurate logical representations given that assumption. we further assume that the entailment annotations of various problems are valid, and we use those to evaluate the correctness of the logical representations of sentences. the paper is structured as follows: in section 2, we give a brief summary of the computational frameworks whose various subsystems rely on. in particular, the grammatical framework is used to construct the syntactic parser, the coq proof assistant checks all the reasoning and a monad-based dynamic semantics deals with montague-style se1 one can consider that @xcite have made a run against the whole test suite. however, they do not deal with multi-premise cases. consequently only 36/75 cases in the temporal section are attempted. the general accuracy of the system is .59, and .61 for the temporal section. our system, as shown ## temporal-semantics in a logic-based nli system our temporal analysis places itself in the context of a complete nli system -which is why we can test it on the fracas suite. in this section we give a brief overview of the phases of the system, referring the reader to published work for details. ## our treatment of time in montagovian semantics, (intransitive) verbs are one-place predicates; in types, they are functions from entities to propositions (@xmath0. our basic approach is to generalise the interpretation of verbs, so that it takes two additional time parameters, one corresponding to the starting time of the action and one corresponding to its stopping time ((e × time × time) → t). for example, if john walked between t 0 and t 1 , we would have: walk(john, t 0 , t 1 ). from now on we will call an interval of time points [t 0 , t 1 ] a timespan, where t 0 and t 1 are elements of the time type, which is represented in coq as an abstract ordered ring. every timespan [t 0 , t 1 ] has the property t 0 ≤ t 1 : it starts no later than it stops. (we are thus using a simple newtonian model of time, corresponding to a layman intuition of a linear constant flow of time.) in principle, common nouns and adjectives should undergo the same procedure. for simplicity we will however only consider verbs from now on. (in fact, even in our implementation we chose not to extend nouns nor adjectives with timespan parameters. this choice limits the increase in complexity of the formulas compared to non-temporal semantics, at the expense of inaccuracy for a couple of problems in the fracas test suite: problems 271 and 272 use a an adjective as a copula which is subject to temporal reasoning.) (271) a unknown p1 smith was present. p2 jones was present. p3 smith was present after jones was present. h jones was present before smith was present. temporal context we adjust the montagovian semantics so that the interpretation of every category (propositions, verb phrases, etc.) takes a temporal context as an additional parameter, which serves as a time reference for the interpretation of all time-dependent semantics within the phrase. tenses the principal non-trivial manipulators of timespans are tense markers. in our syntax, inherited from gf, tenses are represented syntactically as an attribute of clauses. an illustration of a pasttense clause and its interpretation follows in example (1). notice in particular the past argument to the usecl constructor. in our semantics we deal only with present and past tenses (simple and continuous). indeed we find that fracas does not exercise additional specific tenses. (when a more complicated tense is used, the additional information is also carried by adverbs or adverbial phrases, in a more specific way). while we believe that many other tenses can be captured under the same general framework, we leave a detailed study to further work. even though we discuss a refinement to handle the past continuous at the end of this section, the procedure to handle tense annotations is as follows: temporal adverbs the other single most important source of interesting timespans are adverbs. most of the temporal adverbs fall in either of the following categories: in the fracas test suite, we normally do not find several time-modifying adverbs modifying a single verb phrase. indeed, sentences such as "in 1992, in 1991 john wrote a novel" are infelicitous. this justifies ignoring the input timespan in the above interpretation -we are in particular not interested in modelling felicity with our semantics, only giving an accurate semantics when the input is felicitous. if there is no explicit time context, then "always" has no constraint on the interval, otherwise the quantified interval must be included in it: note that here we do use the input interval, resulting in a correct interpretation for phrases such as "in 1994, itel was always on time." . aside: aspectual classes in the literature in this paper we borrow several notions from classical temporal semantics such as "stative", "achievement", "activity", etc., even though our definitions do not perfectly match the classical ones. we explain our precise meaning for these terms in the body of the paper. nevertheless, we refer the reader to @xcite for an extensive review of formal temporal semantics. for the cognoscenti, we can already point out some differences in terminology: we use the term activity as a general term which encompasses the three classical notions of activites, achievements and accomplishments. indeed, insofar as the test suite is concerned, we find that these three categories can be collapsed into a single one (they are subject to eq. ( 1 )). that is, it is sufficient for the testsuite to distinguish between events and states. (in this paper, we always assume that the problems in the fracas testsuite are correctly annotated.) time references and aspectual classes a common theme in the testsuite is the reference to previous occurrences of an event: p2 jones left after anderson left. ## worked out example to give a sense of the additional details necessary to deal with the precision demanded by a proofassistant such as coq we show how problem (279) is worked out in full details. we start with input trees in gf format, given by @xcite . they can be rendered as follows: of particular note is the use of the pronoun "it", and the fact that adverbial expressions such that "in 1992" are lexicalized. we also follow the gf convention to postfix lexical items with the name of their category. most of the other categories follow usual naming conventions. we remind the reader that "slash" categories are used to swap the order of arguments (compared to non-slashed categories of similar names). our dynamic and temporal semantics gives the following interpretation for s_279_1_p implies s_279_3_h. forall (fun @xmath1: time), ((exists (c: time), in the above, one should remark the top-level quantification over the novel (as explained in section 3), the quantification over time intervals as individual timepoints, and the use of custom operators for several constructions (forall, not, is_interval, apptime). this use of custom operators is useful for several generalisations (for example, we have quantifiers such as most in addition to forall -see @xcite ) unfolding the definitions for these operators yield the following proposition: this is very close to our idealised representation of the problem eq. ( 2 ). one difference is the use of abstract coq integers for timepoints. using a discrete time allows us to use predefined coq tactics. the discrete nature of integers does not interfere with the reasoning. finally, we can show a coq proof for the above proposition: theorem problem279 : problem279afalse. cbv. intros novel issmithsnovel p1 h. destruct p1 as [t0 [t1 [ct1 [ct2 [ct3 p1]]]]]. destruct h as [u0 [u1 [cu1 [cu2 [cu3 h]]]]]. specialize writeunique with (x := novel)(y := smith) as a. unfold uniqueactivity in a. specialize (a _ _ _ _ p1 h) as b. lia. qed. the intros and destruct tactics serve bookkeeping purposes. the critical part is the use of the writeunique axiom, which witnesses the aspectual class of the predicate write v2. the proof is completed by the use of the lia tactic, which is embeds a decision procedure for linear arithmetic problems foot_0 . fortunately, lia can take care of all the problems which arise in the fracas testsuite. ## results and evaluation our target is the fracas testsuite, which aims at covering a wide range of common natural-language phenomena. the suite is structured according to the semantic phenomena involved in the inference process for each example, and contains nine sections: quantifiers, plurals, anaphora, ellipsis, adjectives, comparatives, temporal, verbs and attitudes. the system described here focuses on the temporal section. however, it also supports the other eight sections. to our knowledge this is the first system which attempts to target the temporal section in full. but in fact, our system even provides support for all the other sections. thus, a couple of decades interaction with anaphora one reason explaining the lower performance of our system on some sections of the testsuite is that our interpretation of time interacts imperfectly with anaphora and ellipsis. consider the following example: in the first premise, our system essentially resolves the ellipsis to get the following reading: "itel won x orders and apcom won y orders and @xmath2.". one would need each of the verb phrases "won x orders" and "won y orders" to introduce their own timespans with existential quantifiers. however, the organisation of our system is such that the existentials are introduced before the ellipsis is expanded. consequently we get a wrong interpretation and the inference cannot be made. ## conclusions and future work we have presented a first attempt for a computational approach dealing with the temporal section of the fracas test suite. to do this, we have provided a simplified taxonomy of aspectual classes for verb phrases, guided by the applicability of the unicity of action and temporal subsumption properties. while part of this simplification is accidental (conflation of activity and accomplishment), we find that other parts (the automatic distinction between repeatable and unrepeatable achievements) constitute theoretical improvements. besides inference, formal interpretation of tense is found in natural-language interfaces to databases. of note is the work of @xcite , which handles many of the time-aware adverbial clauses that we address. however, we cover many more logical aspects of inference, such as coreference via unity of action and interaction with quantifiers. bernardy and chatzikyriakidis (2019 ) presented a logical system for handling 8 of the 9 sections of the fracas test suite, but excluded section 7, suggesting that it requires many examples that need an ad hoc treatment. here, we took up this challenge and have shown that a system similar to theirs can be extended to cover the remaining section of the test suite, without considerably decreasing the performance of the rest of the sections. this is indeed a common problem with logical approaches, namely the fact that one can have theoretically motivated implementations of individual phenomena, e.g. anaphora, ellipsis, quantifiers, temporal reference etc., but when one tries to put all these together into a unified system, this proves to be a daunting task. we believe that this paper presents an exception, and provides a system that can deal with all these different semantic phenomena under a unified system with very good results. we use the same combination of a number of well-studied tools as @xcite : type theory, parsing using the grammatical framework (gf), monadic dynamic semantics and proof assistant technology (coq). the system achieves an accuracy of 0.73 on the temporal section and 0.81 overall. the whole system, including data sets, is available at the following url: https://github. com/gu-clasp/fracoq/tree/iwcs2021 . one of the things to be looked at is fixing the issues associated with parts of the test suite that "broke" when the temporal analysis was introduced. some of these have been already mentioned: interaction of the temporal variables with anaphora. another extension of this work is to reflect more temporal semantic inference properties in an extended test suite. indeed, there as properties which are not captured in the fracas test suite, such as fine-grained examples of lexical and grammatical aspect, as well as the interaction between those two, for example cases where one needs to actually distinguish between achievements and accomplishments on the basis of their inferential properties: h john was finding his keys (unk). in the first of the two examples involving an achievement verb, the inference is unk, since there is no guarantee that the action is noninstantaneous. to the contrary, for accomplishment verbs, the inference follows. further cases to be included in an extended fra-cas future suite involve examples where the interaction between different tenses needs to be captured: foot_1 ( * 3) p1 when the phone rang, john had entered the house. h john entered the house before the phone rang (yes). finally it would be desirable to improve automation of the system, and evaluate it on a larger test set. as it stands coq fully checks the proof of entailment for each (provable) problem. however, the construction of such proofs has demanded human intervention. it would be desirable to fully automate the proof construction step. for this to make sense however we need a much larger test suite, properly separated into a development and a (secret) test set. otherwise, only the limited power of the logic prevents us (or any followup work) to fine-tune the rules of the system until one gets full coverage. this kind of observation holds in general of any rule-based system, and thus applies not only to the proof-construction phase, but also to the underlying dynamic semantics and parsing phase (which is limited only by the power of the language and frameworks used for its implementation). in sum, contrary to statistical approaches to language understanding, the value of the present work lies not in the bare accuracy numbers which we are able to achieve, but in the details of how we do so: the of set of rules which we use, which is described in detail here and in the work which we base ourselves upon @xcite .