In this study, we propose a method for applying a temporal relation identification model to functional requirements. We discuss the limited availability of data in the requirements engineering domain compared to other fields when used for supervised learning, and therefore employ a corpus from the news domain for training. The experimental results demonstrate that the types of temporal relations present in functional requirements are limited, indicating that focusing on learning with a narrowed set of labels is effective. Additionally, We incorporate Dependency Path (DP) into the temporal relation identification model and report, through comparative experiments, that leveraging DP is effective, but minor modifications to DP do not lead to significant improvements in accuracy. By demonstrating specific application methods of temporal relation identification in requirements engineering, we anticipate contributing to the analysis of functional requirements in software development.

In software development, ambiguities in requirements described in natural language (NL) prevent the application of formal approaches, posing a difficulty that has heretofore been avoided in two main ways: discovery based on formal specifications generated from NL requirements, and the creation of non-ambiguous NL requirements. In the former, NL is more expressive and does not rely on the user‘s expertise, but instead makes the automatic generation of formal specifications difficult. The latter facilitates the automatic generation of formal specifications and has the advantage of reduced syntactic complexity, but in exchange for reduced expressiveness of NL. In this paper, we take an approach that allows users to describe highly expressive NL requirements and reduces syntactic complexity to support the automatic generation of formal specifications from NL requirements. We also propose an information extraction method using syntactic patterns of low syntactic complexity. Applying our method to practical requirement sentences reveals that it is effective in reducing the complexity of information extraction rules. We expect that our method can support the automatic generation of formal specifications from NL requirements without compromising the expressive power of the language.

Model checking with a time aspect is often used in verification on hardware and embedded systems. Timed automata are often used for such models. UPPAAL is a world-wide famous model checking tool for timed automata; however, UPPAAL is a Computational Tree Logic (CTL)-based model checking tool and cannot use Linear Temporal Logic (LTL) properties. Bounded model checking uses LTL (Linear Time Logic) for a checking formula. Bounded model checking specifies a boundary k and obtains counterexamples by searching from the initial state of a system to states reachable by k-steps. There are several studies on bounded model checking. Sorea has proposed a concrete algorithm for a timed automaton. There are, however, no clear details on how to implement bounded model checking tools for timed automata, and study the performance. Another problem is that the timed automaton covered by the method does not support general variables except for clock variables. The objective of this study is to implement a bounded model checking tool using LTL for timed automata. We also improve Sorea's method so that it can handle extended timed automata that handle general variables. This paper also presents some LTL examples from texts on requirement specifications for embedded systems and the results of applying the tool to them.

Despite the success of language models using neural networks, it remains unclear to what extent neural models have the generalization ability to perform inferences.In this paper, we introduce a method for evaluating whether neural models can learn systematicity of monotonicity inference in natural language, namely, the regularity for performing arbitrary inferences with generalization on composition.We consider four aspects of monotonicity inferences and test whether the models can systematically interpret lexical and logical phenomena on different training/test splits.A series of experiments show that three neural models systematically draw inferences on unseen combinations of lexical and logical phenomena when the syntactic structures of the sentences are similar between the training and test sets.However, the performance of the models significantly decreases when the structures are slightly changed in the test set while retaining all vocabularies and constituents already appearing in the training set.This indicates that the generalization ability of neural models is limited to cases where the syntactic structures are nearly the same as those in the training set.(1) P : Some [puppies ↑] ran.H: Some dogs ran.(2) P : No [cats ↓] ran.H: No small cats ran.(3) P : Some [puppies which chased no [cats ↓]] ran.H: Some dogs which chased no small cats ran.(5) P : Some small dogs ran ⇒ H: Some dogs ran (6) P : Several dogs ran ⇒ H: Several animals ran (7) P : No animals ran ⇒ H: No dogs ran (8) P : Several small dogs ran ⇒ H: Several dogs ran (9) P : No dogs ran ⇒ H: No small dogs ranHere, we consider a set of inferences D Q,R

In formal semantics, there are two well-developed semantic frameworks: event semantics, which treats verbs and adverbial modifiers using the notion of event, and degree semantics, which analyzes adjectives and comparatives using the notion of degree. However, it is not obvious whether these frameworks can be combined to handle cases in which the phenomena in question are interacting with each other. Here, we study this issue by focusing on natural language inference (NLI). We implement a logic-based NLI system that combines event semantics and degree semantics and their interaction with lexical knowledge. We evaluate the system on various NLI datasets containing linguistically challenging problems. The results show that the system achieves high accuracies on these datasets in comparison with previous logic-based systems and deep-learning-based systems. This suggests that the two semantic frameworks can be combined consistently to handle various combinations of linguistic phenomena without compromising the advantage of either framework.

In logic-based approaches to reasoning tasks such as Recognizing Textual Entailment (RTE), it is important for a system to have a large amount of knowledge data. However, there is a tradeoff between adding more knowledge data for improved RTE performance and maintaining an efficient RTE system, as such a big database is problematic in terms of the memory usage and computational complexity. In this work, we show the processing time of a state-of-the-art logic-based RTE system can be significantly reduced by replacing its search-based axiom injection (abduction) mechanism by that based on Knowledge Base Completion (KBC). We integrate this mechanism in a Coq plugin that provides a proof automation tactic for natural language inference. Additionally, we show empirically that adding new knowledge data contributes to better RTE performance while not harming the processing speed in this framework.

We propose a new domain adaptation method for Combinatory Categorial Grammar (CCG) parsing, based on the idea of automatic generation of CCG corpora exploiting cheaper resources of dependency trees. Our solution is conceptually simple, and not relying on a specific parser architecture, making it applicable to the current best-performing parsers. We conduct extensive parsing experiments with detailed discussion; on top of existing benchmark datasets on (1) biomedical texts and (2) question sentences, we create experimental datasets of (3) speech conversation and (4) math problems. When applied to the proposed method, an off-the-shelf CCG parser shows significant performance gains, improving from 90.7% to 96.6% on speech conversation, and from 88.5% to 96.8% on math problems.

Sequence-to-sequence models have shown strong performance in a wide range of NLP tasks, yet their applications to sentence generation from logical representations are underdeveloped.In this paper, we present a sequence-to-sequence model for generating sentences from logical meaning representations based on event semantics.We use a semantic parsing system based on Combinatory Categorial Grammar (CCG) to obtain data annotated with logical formulas.We augment our sequence-to-sequence model with masking for predicates to constrain output sentences.We also propose a novel evaluation method for generation using Recognizing Textual Entailment (RTE).Combining parsing and generation, we test whether or not the output sentence entails the original text and vice versa.Experiments showed that our model outperformed a baseline with respect to both BLEU scores and accuracies in RTE.

Hitomi Yanaka, Koji Mineshima, Pascual Martínez-Gómez, Daisuke Bekki. Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume 1 (Long Papers). 2018.

Pascual Martínez-Gómez, Koji Mineshima, Yusuke Miyao, Daisuke Bekki. Proceedings of the 15th Conference of the European Chapter of the Association for Computational Linguistics: Volume 1, Long Papers. 2017.

Determining semantic textual similarity is a core research subject in natural language processing.Since vector-based models for sentence representation often use shallow information, capturing accurate semantics is difficult.By contrast, logical semantic representations capture deeper levels of sentence semantics, but their symbolic nature does not offer graded notions of textual similarity.We propose a method for determining semantic textual similarity by combining shallow features with features extracted from natural deduction proofs of bidirectional entailment relations between sentence pairs.For the natural deduction proofs, we use ccg2lambda, a higherorder automatic inference system, which converts Combinatory Categorial Grammar (CCG) derivation trees into semantic representations and conducts natural deduction proofs.Experiments show that our system was able to outperform other logicbased systems and that features derived from the proofs are effective for learning textual similarity.

This paper presents a system that compositionally maps outputs of a wide-coverage Japanese CCG parser onto semantic representations and performs automated inference in higher-order logic.The system is evaluated on a textual entailment dataset.It is shown that the system solves inference problems that focus on a variety of complex linguistic phenomena, including those that are difficult to represent in the standard first-order logic.

We present a higher-order inference system based on a formal compositional semantics and the wide-coverage CCG parser.We develop an improved method to bridge between the parser and semantic composition.The system is evaluated on the FraCaS test suite.In contrast to the widely held view that higher-order logic is unsuitable for efficient logical inferences, the results show that a system based on a reasonably-sized semantic lexicon and a manageable number of non-first-order axioms enables efficient logical inferences, including those concerned with generalized quantifiers and intensional operators, and outperforms the state-of-the-art firstorder inference system.