Against the backdrop of the ever-improving Natural Language Inference (NLI) models, recent efforts have focused on the suitability of the current NLI datasets and on the feasibility of the NLI task as it is currently approached. Many of the recent studies have exposed the inherent human disagreements of the inference task and have proposed a shift from categorical labels to human subjective probability assessments, capturing human uncertainty. In this work, we show how neither the current task formulation nor the proposed uncertainty gradient are entirely suitable for solving the NLI challenges. Instead, we propose an ordered sense space annotation, which distinguishes between logical and common-sense inference. One end of the space captures non-sensical inferences, while the other end represents strictly logical scenarios. In the middle of the space, we find a continuum of common-sense, namely, the subjective and graded opinion of a “person on the street.” To arrive at the proposed annotation scheme, we perform a careful investigation of the SICK corpus and we create a taxonomy of annotation issues and guidelines. We re-annotate the corpus with the proposed annotation scheme, utilizing four symbolic inference systems, and then perform a thorough evaluation of the scheme by fine-tuning and testing commonly used pre-trained language models on the re-annotated SICK within various settings. We also pioneer a crowd annotation of a small portion of the MultiNLI corpus, showcasing that it is possible to adapt our scheme for annotation by non-experts on another NLI corpus. Our work shows the efficiency and benefits of the proposed mechanism and opens the way for a careful NLI task refinement.

This paper studies fundamental questions concerning category-theoretic models of induction and recursion. We are concerned with the relationship between well-founded and recursive coalgebras for an endofunctor. For monomorphism preserving endofunctors on complete and well-powered categories every coalgebra has a well-founded part, and we provide a new, shorter proof that this is the coreflection in the category of all well-founded coalgebras. We present a new more general proof of Taylor’s General Recursion Theorem that every well-founded coalgebra is recursive, and we study conditions which imply the converse. In addition, we present a new equivalent characterization of well-foundedness: a coalgebra is well-founded iff it admits a coalgebra-to-algebra morphism to the initial algebra.

We build and study dynamic versions of epistemic logic. We study languages parameterized by an action signature that allows one to express epistemic actions such as (truthful) public announcements, completely private announcements to groups of agents, and more. The language $\mathcal{L}$(Σ) is modeled on dynamic logic. Its sentence-building operations include modalities for the execution of programs, and for knowledge and common knowledge. Its program-building operations include action execution, composition, repetition, and choice. We consider two fragments of $\mathcal{L}(\mathbf{\Sigma })$. In ${\mathcal{L}}_1(\mathbf{\Sigma })$, we drop action repetition; in ${\mathcal{L}}_0(\mathbf{\Sigma })$, we also drop common knowledge. We present the syntax and semantics of these languages and sound proof systems for the validities in them. We prove the strong completeness of a logical system for ${\mathcal{L}}_0(\mathbf{\Sigma })$ and the weak completeness of one for ${\mathcal{L}}_1(\mathbf{\Sigma })$. We show the finite model property and, hence, decidability of ${\mathcal{L}}_1(\mathbf{\Sigma })$. We translate ${\mathcal{L}}_1(\mathbf{\Sigma })$ into PDL, obtaining a second proof of decidability. We prove results on expressive power, comparing ${\mathcal{L}}_1(\mathbf{\Sigma })$ with modal logic together with transitive closure operators. We prove that a logical language with operators for private announcements is more expressive than one for public announcements.

This article enlarges classical syllogistic logic with assertions having to do with comparisons between the sizes of sets. So it concerns a logical system whose sentences are of the following forms: All x are y and Some x are y, There are at least as many x as y, and There are more x than y. Here x and y range over subsets (not elements) of a given infinite set. Moreover, x and y may appear complemented (i.e., as ), with the natural meaning. We formulate a logic for our language that is based on the classical syllogistic. The main result is a soundness/completeness theorem. There are efficient algorithms for proof search and model construction.

We add Most X are Y to the syllogistic logic of All X are Y and Some X are Y. We prove soundness, completeness, and decidability in polynomial time. Our logic has infinitely many rules, and we prove that this is unavoidable.