Studies have shown that some Natural Language Processing (NLP) systems encode and replicate harmful biases with potential adverse ethical effects in our society. In this article, we propose an approach for identifying gender and racial stereotypes in word embeddings trained on judicial opinions from U.S. case law. Embeddings containing stereotype information may cause harm when used by downstream systems for classification, information extraction, question answering, or other machine learning systems used to build legal research tools. We first explain how previously proposed methods for identifying these biases are not well suited for use with word embeddings trained on legal opinion text. We then propose a domain adapted method for identifying gender and racial biases in the legal domain. Our analyses using these methods suggest that racial and gender biases are encoded into word embeddings trained on legal opinions. These biases are not mitigated by exclusion of historical data, and appear across multiple large topical areas of the law. Implications for downstream systems that use legal opinion word embeddings and suggestions for potential mitigation strategies based on our observations are also discussed.

We present a non-factoid QA system that provides legally accurate, jurisdictionally relevant, and conversationally responsive answers to user-entered questions in the legal domain. This commercially available system is entirely based on NLP and IR, and does not rely on a structured knowledge base. WestSearch Plus aims to provide concise one sentence answers for basic questions about the law. It is not restricted in scope to particular topics or jurisdictions. The corpus of potential answers contains approximately 22M documents classified to over 120K legal topics.

We show how labelled deductive systems can be combined with a logical framework to provide a natural deduction implementation of a large and well-known class of propositional modal logics (including K, D, T, B, S4, S4.2, KD45, S5). Our approach is modular and based on a separation between a base logic and a labelling algebra, which interact through a fixed interface. While the base logic stays fixed, different modal logics are generated by plugging in appropriate algebras. This leads to a hierarchical structuring of modal logics with inheritance of theorems. Moreover, it allows modular correctness proofs, both with respect to soundness and completeness for semantics, and faithfulness and adequacy of the implementation. We also investigate the tradeoffs in possible labelled presentations: we show that a narrow interface between the base logic and the labelling algebra supports modularity and provides an attractive proof-theory but limits the degree to which we can make use of extensions to the labelling algebra.

Generic proof systems like Isabelle provide some limited but useful metatheoretic facilities for declared logics; in particular, users can prove simple derived rules and also ‘solve’ formulae that contain metavariables—a technique useful for program synthesis. We show how an arbitrary first-order theory can be conservatively extended to provide similar facilities, without a supporting metatheory, and examine what the limitations of this approach are.