Translating a Fragment of Natural Deduction System for Natural Language into Modern Type Theory

In Rainer Osswald, Christian Retoré & Peter Sutton (eds.), Proceedings of the IWCS 2019 Workshop on Computing Semantics with Types, Frames and Related Structures. Stroudsburg, PA: Association for Computational Linguistics. pp. 10-18 (2019)

Ivo Pezlar
Czech Academy of Sciences, Institute of Philosophy
In this paper, we investigate the possibility of translating a fragment of natural deduction system (NDS) for natural language semantics into modern type theory (MTT), originally suggested by Luo (2014). Our main goal will be to examine and translate the basic rules of NDS (namely, meta-rules, structural rules, identity rules, noun rules and rules for intersective and subsective adjectives) to MTT. Additionally, we will also consider some of their general features.
Keywords proof-theoretic semantics  modern type theory  natural language semantics
Categories (categorize this paper)
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 43,999
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Structural Proof Theory.Jan von Plato & Sara Negri - 2006 - Philosophical Review 115 (2):255-258.
Formal Semantics in Modern Type Theories with Coercive Subtyping.Zhaohui Luo - 2012 - Linguistics and Philosophy 35 (6):491-513.

View all 7 references / Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Natural Language Inference in Coq.Stergios Chatzikyriakidis & Zhaohui Luo - 2014 - Journal of Logic, Language and Information 23 (4):441-480.
Harmony in Multiple-Conclusion Natural-Deduction.Nissim Francez - 2014 - Logica Universalis 8 (2):215-259.
A Proof-Theoretic Semantics for Adjectival Modification.Nissim Francez - 2017 - Journal of Logic, Language and Information 26 (1):21-43.
An Expressive First-Order Logic with Flexible Typing for Natural Language Semantics.Chris Fox & Shalom Lappin - 2004 - Logic Journal of the Interest Group in Pure and Applied Logics 12 (2):135--168.
A Note on Harmony.Nissim Francez & Roy Dyckhoff - 2012 - Journal of Philosophical Logic 41 (3):613-628.
A Natural Deduction System for First Degree Entailment.Allard Tamminga & Koji Tanaka - 1999 - Notre Dame Journal of Formal Logic 40 (2):258-272.
Free Semantics.Ross Thomas Brady - 2010 - Journal of Philosophical Logic 39 (5):511 - 529.


Added to PP index

Total views
9 ( #777,343 of 2,266,718 )

Recent downloads (6 months)
9 ( #115,976 of 2,266,718 )

How can I increase my downloads?


My notes

Sign in to use this feature