NDLI: Syntactic Calculus with Dependent Types

Content Provider	Springer Nature Link
Author	Ranta, Aarne
Copyright Year	1998
Abstract	The aim of this study is to look at the the syntactic calculus of Bar-Hillel and Lambek, including semantic interpretation, from the point of view of constructive type theory. The syntactic calculus is given a formalization that makes it possible to implement it in a type-theoretical proof editor. Such an implementation combines formal syntax and formal semantics, and makes the type-theoretical tools of automatic and interactive reasoning available in grammar.In the formalization, the use of the dependent types of constructive type theory is essential. Dependent types are already needed in the semantics of ordinary Lambek calculus. But they also suggest some natural extensions of the calculus, which are applied to the treatment of morphosyntactic dependencies and to an analysis of selectional restrictions. Finally, directed dependent function types are introduced, corresponding to the Π types of constructive type theory.Two alternative formalizations are given: one using syntax trees, like Montague grammar, and one dispensing with them, like the theory called minimalistic by Morrill. The syntax tree approach is presented as the main alternative, because it makes it possible to embed the calculus in a more extensive Montague-style grammar.
Starting Page	413
Ending Page	431
Page Count	19
File Format	PDF
ISSN	09258531
Journal	Journal of Logic, Language and Information
Volume Number	7
Issue Number	4
e-ISSN	15729583
Language	English
Publisher	Kluwer Academic Publishers
Publisher Date	1998-01-01
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Logic Artificial Intelligence (incl. Robotics) Semantics
Content Type	Text
Resource Type	Article
Subject	Philosophy Computer Science Linguistics and Language

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Cut-Rule Axiomatization of the Syntactic Calculus NL0

Cut-Rule Axiomatization of the Syntactic Calculus L0

The Resolution Calculus, Alexander Leitsch

Tolerance Logic

Unnatural Language Processing

Fragments of Language

Inference and Computational Semantics

Editorial: Modal Logic and Dynamic Semantics

Substructural Logics with Mingle

Syntactic Calculus with Dependent Types

Similar Documents

Cut-Rule Axiomatization of the Syntactic Calculus NL0

Cut-Rule Axiomatization of the Syntactic Calculus L0

The Resolution Calculus, Alexander Leitsch

Tolerance Logic

Unnatural Language Processing

Fragments of Language

Inference and Computational Semantics

Editorial: Modal Logic and Dynamic Semantics

Substructural Logics with Mingle

Syntactic Calculus with Dependent Types