Proof Assistants for Natural Language Semantics
From MaRDI portal
Publication:2963996
DOI10.1007/978-3-662-53826-5_6zbMath1483.68456OpenAlexW2554346448MaRDI QIDQ2963996
Stergios Chatzikyriakidis, Zhaohui Luo
Publication date: 22 February 2017
Published in: Logical Aspects of Computational Linguistics. Celebrating 20 Years of LACL (1996–2016) (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-662-53826-5_6
Natural language processing (68T50) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (3)
Propositional forms of judgemental interpretations ⋮ Theoretical and practical approaches to the denotational semantics for MDESL based on UTP ⋮ Adjectival and adverbial modification: the view from modern type theories
Uses Software
Cites Work
- Dependent event types
- Coercive subtyping: theory and implementation
- Natural language inference in Coq
- The Montagovian generative lexicon ΛTyn: a type theoretical framework for natural language semantics
- Contextual Analysis of Word Meanings in Type-Theoretical Semantics
- Records and Record Types in Semantic Theory
- Common Nouns as Types
- Representing Anaphora with Dependent Types
- Monotonicity Reasoning in Formal Semantics Based on Modern Type Theories
- Formal Semantics in Modern Type Theories: Is It Model-Theoretic, Proof-Theoretic, or Both?
- Homotopy Type Theory: Univalent Foundations of Mathematics
- An experimental library of formalized Mathematics based on the univalent foundations
- Importing HOL Light into Coq
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Proof Assistants for Natural Language Semantics
