Parsing as Deduction Revisited: Using an Automatic Theorem Prover to Solve an SMT Model of a Minimalist Parser

Proceedings of the 26th Conference on Computational Natural Language Learning (CoNLL), pages 157 - 175 December 7-8, 2022 ©2022 Association for Computational Linguistics Parsing as Deduction Revisited: Using an Automatic Theorem Prover to Solve an SMT Model of a Minimalist Parser Sagar Indurkhya Massachusetts Institute of Technology 32 Vassar St. Cambridge, MA 02139 indurks@mit.edu Abstract We introduce a constraint-based parser for Min- imalist Grammars (MG), implemented as a working computer program, that falls within the long established “Parsing as Deduction” frame- work. The parser takes as input an MG lexicon and a (partially specified) pairing of sound with meaning – i.e. a word sequence paired with a semantic representation – and, using an axiom- atized logic, declaratively deduces syntactic derivations (i.e. parse trees) that comport with the specified interface conditions. The parser is built on the first axiomatization of MGs to use Satisfiability Modulo Theories (SMT), en- coding in a constraint-based way the princi- ples of minimalist syntax. The parser operates via a novel solution method: it assembles an SMT model of an MG derivation, translates the inputs into SMT formulae that constrain the model, and then solves the model using the Z3 SMT-solver, a high-performance automatic the- orem prover; as the SMT-model has finite size (being bounded by the inputs), it is decidable and thus solvable in finite time. The output derivation is then recovered from the model so- lution. To demonstrate this, we run the parser on several representative inputs and examine how the output derivations differ when the in- puts are partially vs. fully specified. We con- clude by discussing the parser’s extensibility and how a linguist can use it to automatically identify: (i) dependencies between input inter- face conditions and principles of syntax, and (ii) contradictions or redundancies between the model axioms encoding principles of syntax. 1 Introduction Minimalist theories of syntax consider the Human Language Faculty (HLF) as a computational sys- tem capable of deriving from a finite lexicon and a single combinatorial operation, an unbounded set of hierarchical syntactic structures, pairing sounds (typically word sequences) with meaning repre- sentations (Chomsky, 1995). (In more technical language, the HLF pairs Phonological Forms [PF], where a PF is an encoding of information relevant to how a brain-internal structured expression gets pronounced, signed, etc, with Logical Forms [LF], where an LF is a structured semantic representation, e.g. predicate-argument structure.) This study in- troduces a novel computational model for the HLF, implemented as a working computer program,1 that takes the form of a constraint-based parser for Min- imalist Grammars (MG), grounded in the (first) axiomatization of minimalist syntax using Satisfi- ability Modulo Theories (SMT).2 Working within the “Parsing as Deduction” framework (Pereira and Warren, 1983), the parser is a logic program that uses an automatic theorem prover to answer the question: can a given lexicon yield a syntactic structure that encodes a given LF and/or PF? More specifically, the parser takes as input an MG lexicon and a (partial) specification of LF and PF interface conditions (i.e. constraints over …

Content truncated to 500 words