PL
 |
EN
Preferencje help
Polish version English version Język
Widoczny [Schowaj] Abstrakt
Liczba wyników

Znaleziono wyników: 9

Liczba wyników na stronie
first rewind previous Strona / 1 next fast forward last
Wyniki wyszukiwania
Wyszukiwano:
w słowach kluczowych:  type theory
help Sortuj według:

help Ogranicz wyniki do:
first rewind previous Strona / 1 next fast forward last
1
Content available Type Theories and Lexical Networks : using Serious Games as the basis for Multi-Sorted Typed Systems
Chatzikyriakidis S., Lafourcade M., Ramadier L., Zarrouk M.
Journal of Language Modelling
|
2017
|
Vol. 5, No. 2
229--272
EN
In this paper, we show how a rich lexico-semantic network which Has been built using serious games, JeuxDeMots, can help us in grounding our semantic ontologies in doing formal semantics using rich or modern type theories (type theories within the tradition of Martin Löf). We discuss the issue of base types, adjectival and verbal types, hyperonymy/hyponymy relations as well as more advanced issues like homophony and polysemy. We show how one can take advantage of this wealth of lexical semantics in a formal compositional semantics framework. We argue that this is a way to sidestep the problem of deciding what the type ontology should look like once a move to a many sorted type system has been made. Furthermore, we show how this kind of information can be extracted from a lexico-semantic Network like JeuxDeMots and inserted into a proof-assistant like Coq in order to perform reasoning tasks.
2
Content available An outline of type-theoretical approaches to lexical semantics
Cooper R., Retoré C.
Journal of Language Modelling
|
2017
|
Vol. 5, No. 2
165--178
EN
We take the opportunity of the publication of some of the papers of the ESSLLI workshop TYTLES (TYpe Theory and LExical Semantics, ESSLLI 2015, Barcelona) to provide an overview of the possibilities that type theory offers to model lexical semantics, especially the type-theoretical frameworks that properly model compositional semantics.
3
Content available remote About Parallel and Syntactocentric Formalisms: A Perspective from the Encoding of Convergent Grammar into Abstract Categorial Grammar
Groote P., de, Pogodalla S., Pollard C.
Fundamenta Informaticae
|
2011
|
Vol. 106, nr 2-4
211-231
EN
Recent discussions of grammatical architectures have distinguished two competing approaches to the syntax-semantics interface: syntactocentrism, wherein syntactic structures are mapped or transduced to semantics (and phonology), vs. parallelism, wherein semantics (and phonology) communicates with syntax via a nondirectional (or relational) interface. This contrast arises for instance in dealing with in situ operators. The aim of this paper is threefold: first, we show how the essential content of a parallel framework, convergent grammar (CVG), can be encoded within abstract categorial grammar (ACG), a generic framework which has mainly been used, until now, to encode syntactocentric architectures. Second, using such a generic framework allows us to relate the mathematical characterization of parallelism in CVG with that of syntactocentrism in mainstream categorial grammar (CG), suggesting that the distinction between parallel and syntactocentric formalisms is superficial in nature. More generally, it shows how to provide mildly context sensitive languages (MCSL), which are a clearly defined class of languages in terms of ACG, with a relational syntax-semantics interface. Finally, while most of the studies on the generative power of ACG have been related to formal languages, we show that ACG can illuminate a linguistically motivated framework such as CVG.
4
Content available remote Modeling Contexts with Dependent Types
Dapoigny R., Barlatier P.
Fundamenta Informaticae
|
2010
|
Vol. 104, nr 4
293-327
EN
In the area of knowledge representation, a challenging topic is the formalization of context knowledge on the basis of logical foundations and ontological semantics. However, most attempts to provide a formal model of contexts suffer from a number of difficulties, such as limited expressiveness of representation, restricted variable quantification, lack of (meta) reasoning about properties, etc. In addition, type theory originally developed for formal modeling of mathematics has also been successfully applied to the correct specification of programs and in the semantics of natural language. In this paper, we suggest a type theoretical approach to the problem of context and action modeling. Type theory is used both for representing the system’s knowledge of the discourse domain and for reasoning about it. For that purpose, we extend an existing dependent type theory having nice properties, with context-based rules and appropriate inductive types. We claim that the resulting theory exploiting the power of dependent types is able to provide a very expressive system together with a unified theory allowing higher-order reasoning.
5
Content available remote A Note on Forcing and Type Theory
Coquand T., Jaber G.
Fundamenta Informaticae
|
2010
|
Vol. 100, nr 1/4
43-52
EN
The goal of this note is to show the uniform continuity of definable functional in intuitionistic type theory as an application of forcing with dependent type theory.
6
Content available remote The Open Calculus of Constructions (Part I) : An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving
Stehr M-O.
Fundamenta Informaticae
|
2005
|
Vol. 68, nr 1/2
131--174
EN
The open calculus of constructions integrates key features of Martin-Löf's type theory, the calculus of constructions, membership equational logic, and rewriting logic into a single uniform language. The two key ingredients are dependent function types and conditional rewriting modulo equational theories. We explore the open calculus of constructions as a uniform framework for programming, specification and interactive verification in an equational higher-order style. By having equational logic and rewriting logic as executable sublogics we preserve the advantages of a first-order semantic and logical framework and we provide a foundation for a broad spectrum of applications ranging from what could be called executable mathematics, involving symbolic computations and logical proofs, to software and system engineering applications, involving symbolic execution and analysis of nondeterministic and concurrent systems.
7
Content available remote The Open Calculus of Constructions. Part 2, An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving
Stehr M.-O.
Fundamenta Informaticae
|
2005
|
Vol. 68, nr 3
249--288
EN
The open calculus of constructions integrates key features of Martin-Löf's type theory, the calculus of constructions, membership equational logic, and rewriting logic into a single uniform language. The two key ingredients are dependent function types and conditional rewriting modulo equational theories. We explore the open calculus of constructions as a uniform framework for programming, specification and interactive verification in an equational higher-order style. By having equational logic and rewriting logic as executable sublogics we preserve the advantages of a first-order semantic and logical framework and we provide a foundation for a broad spectrum of applications ranging from what could be called executable mathematics, involving symbolic computations and logical proofs, to software and system engineering applications, involving symbolic execution and analysis of nondeterministic and concurrent systems.
8
Content available remote UPSILON: Universal Programming System with Incomplete Lazy Object Notation
Postow B., Regan K., Smith C.H.
Fundamenta Informaticae
|
2002
|
Vol. 50, nr 3,4
325-359
EN
This paper presents a new model of computation that differs from prior models in that it emphasizes data over flow control, has no named variables and has an object-oriented flavor. We prove that this model is a complete and confluent acceptable programming system and has a usable type theory. A new data synchronization primitive is introduced in order to achieve the above properties. Subtle variations of the model are shown to fall short of having all these necessary properties.
9
Content available remote Formalizing context in intuitionistic type theory
Boldini P.
Fundamenta Informaticae
|
2000
|
Vol. 42, Nr 2
105-127
EN
The article discusses formal aspects of the notion of context as needed in AI applications. We advocate the use of Martin-Löf's intuitionistic type theory to formalize and implement contexts. Through many examples belonging to the domains of computational semantics and knowledge based systems, we show that the built-in notion of context in intuitionistic type theory is a structure rich enough for representing most of the features that characterize contexts in an AI perspective. The fact that many recent theorem provers are built on the different theories of types suggests new perspectives in the development of AI applications.
first rewind previous Strona / 1 next fast forward last
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.