This paper deals with a formalization of a natural language dialogue using transparent intensional logic and predicate linear logic. In the beginning, it is necessary to choose the dialogue in a natural language. Subsequently, this dialogue is analyzed by transparent intensional logic, that allows it to capture the meaning of sentences in logical structures. At this stage, a three-step method of an analysis will be applied to the dialogue: at rst, there will be a type analysis of the lexical units, which is the base for the logical constructions that capture the meaning of the sentences and then we apply a type checking to verify the correctness of the solution. In the second part of the paper, the same dialogue is analyzed by the Ludics theory, which represents the superstructure of the predicate linear logic. In a technical presentation of Ludics theory, the dialogue is placed in a logical space and time what allows model interactions between its actors.
Ludics Theory
Computer programs require people to communicate with them in a formal programming language that is accurate, unambiguous, and structured. Human speech does not have these attributes. The natural language has not been discovered, but gradually developed spontaneously over the centuries in communicative practice and adapted to changing conditions in the society. This causes that people mostly understand themselves, but sometimes their understanding of meaning is di erent. The meaning of the natural language expressions is often ambiguous because its logical structure is not identical to the grammatical structure. Explaining the meaning of natural language expressions is dealt by the logic analysis of natural language (LANL), which also allows to discovery the mistakes that arise from misinterpretations of the premises.
The most important requirement for a logical system examining the natural
language semantics is the expressivity. An extensional logic systems
(propositional logic, predicate logic...) are not enough expressive - for LANL needs it is
necessary to work with an intensional logical systems. This paper is built on the
following research results:
{ in [
In the future research, the goal is to create the formal speci cation of a new
logic linking TIL with PLL. It will be the basis for the implementation of a
semantic machine [
The founder of TIL is Pavel Tichy [
Basic Objects in TIL Logical analysis of natural language is related to a speci c object base. The basic objects of TIL which represent non-functional element types are: { set of truth value (true, false) o, { set of individuals , { set of time points (real numbers) , { set of logically possible worlds !.
Functional types are sets partial functions ( 1,....... m), with arguments b1,.....bm of type 1,......., m and values in . Intensions are objects of type ( !), i.e. functions from a possible worlds for any type . Most often, these are functions of type (( )!), for simplicity it is stated in TIL as !. Some examples of frequently used intensions are shown in Table 1. 2.2
Constructions in TIL
Tichy introduced the concepts of construction [
In TIL , these sentences are analyzed in three steps - type analysis (to each object of sentence is assigned a corresponding type), synthesis (create a construction which represents the meaning of a sentence) a type checking (verify if the synthesis was correctly done).
Let's analyze the rst sentence: \If you (son) behave well , you'll either be (choose) playing at home with ball or toy, or going out to the cinema or shopping.\ 1 1. Type analysis: son/ , behave well/(oo ) !, )/ooo, choose/(o ) !, home/(o ) !, _/ooo, out/(o ) !. 2. Synthesis:
w t [[0behave wellw t ) [0choose w t [0home w t _ 0out w t]]] 0son] 3. Type checking: (Fig. 1) 1 This analysis is simpli ed. The disjunctions of which the objects home and out are composed were not analyzed. w t [[0behave well w t ( [0choose w t [0home w t N ! (oo ) ! ! ooo (o ) ! ! (o ) ! !
ooo (o ) ! ! (oo ) o ! oo o o (o ) o o (o ) o oo o o (o ) o
Other sentences can be analyzed in the same way. A sentence, the meaning of which is correctly expressed, is always a proposition with type (o) ! (same as in Fig. 1). From this example it is clear that even though TIL is an e ective tool of LANL, the individual sentences of the natural language are analyzed separately, and so it is not adequate for its application on natural language dialogues. In the next section, the same dialogue will be explored through the PLL. 3
Linear logic, introduced in 1987 by J.Y. Girard [
Since a intensions in the natural language expressions can be described by
using predicates, we need to introduce PLL. The formula ' in a PLL can be
formulated by the following production rule [
Ludics Theory
The Ludics theory [
Time and space in linear logic To change the polarity of the blocks (called clusters) in proof tree means an increment of time. PLL connectives are divided into positive and negative, which also determines the polarity of the PLL formula. There are: { positive - ; , 1,0, !, 9, { negative - N; O, >; ?, ?, 8, { special - ( represents dependent polarity, (:)? causes the ipping of polarity.
The rules of invertibility and focalization are used to make one-step from few follow-up steps in proof tree. In invertibility, a cluster of negative formulas is formed, in focalization a cluster of positive formulas is originated.
Talking about space in Ludics, the truth nor the content of formula, but its location, is essential in the proof tree, known as the . The proof tree that contains only location data is called a design. Immediate subformulas of the A formula are enumerable, while the number of immediate subformulas can be labelled as Bi, Bij , Bijk:::, where i; j; k are positive integers - biases and i; ij; ijk are concatenation of particulate biases i; j; k. If all the data, except the formula addresses, is removed in the sequences used in argument, we call it a pitchfork: where represents one address, and context pitchfork calculus, the following rules are applied:
Axiom daimon is a nite set of addresses. In ` ; ` Positive and negative rule :::
i ` i::: ` ; (+; `; ; I) ::: ` I ;
I::: ` ( ; ` N) (2) (3) With PLL will be analyzed the same dialogue as with TIL. The PLL formula of the sentence: \If you behave well (W ), you'll either be playing at home with ball (B) or toy (T ), or going out to the cinema (C) or shopping. (S)\ is:
W ( ((BNT )N(C S))2 (5)
From this PLL formula is possible to create a proof tree, where the following rules of the PLL sequent calculus are used:
A ` A (id) ` '; ` ;
` 'N ; ` '; 4 ((:)?) ; '? ` 4 (N) ` '; ` ' ; ; A ` B; 4 ` A ( B; 4
(() ( r1 )
In proof tree, the change of the polarity is marked with the signs + a what creates the polarized tree, shown in Fig. 2. (6) (-)
(id) W; W ? ` C; C? ` W; W ?; C; C? ((:)?)
( ) ` (C S); 2; W; W ? W; W ? ` (C
((:)?) S); 2 ( )
N (+)
W; W ? ` ((BNT )N(C ` W ( ((BNT )N(C
S)); 1 (() S));
N - the choice depends on the son (outer non-determinism), depend on the son (inner non-determinism). - the choice does not ` W; W ?; B; B? :0 ` (+; `; ; f0g) ` :0:4:1 ` :0:1 ((@+); `; :0:4; f1g) ` :0:1; :0:4 ( ; :0; ` ff1g; f2g; f3g; f4gg)
From the address tree it is possible to create the dialogue strategies. The mother has three strategies - she always sets out the o er (positive action ( ; f0g)) and after its execution she is ready to allow her son to play with the ball (negative action ( :0; f1; 2g)), or the toy (negative action ( ; :0; f1; 3g)), or to go out with him (negative action ( ; :0; f1; 4g)). If a son wants to go out, his mother chooses from two other strategies - cinema (positive action ( :0:4; f1g)) or shopping (positive action ( :0:4; f2g)).
The son has four strategies - he always accepts the mother's o er (negative action ( ; f0g)) and either wants to play with the ball (positive action ( :0; f1; 2g)), or the toy (positive action ( ; :0; f1; 3g)), or wants to go out and he is ready for both eventualities (two negative actions ( :0:4; f1g) and ( :0:4; f1g)), or is ready only for going to the cinema (negative action ( :0:4; f2g)).
The strategies of the dialogue actors make it possible to explore their interactions by using principles from the game semantics. PLL allows to describe natural language dialogues more e ectively than TIL. 4
In this paper the possibilities of analyzing natural language dialogues through TIL and PLL logic systems are explored. From the presented results is clear that each of mentioned logic systems has a certain de ciency - TIL analyzes the sentences separately, whether they are in dialogue or not; PLL is not usually used in LANL, because it does not allow ne-grained semantics analysis of natural language expressions.
In order to achieve the declared goals of the research, it will be necessary to divide it into two parts, where each represents an original contribution in the processing of the natural language. The rst phase of the project will be based on existing and already published results in which a transparent intensional logic has been identi ed as the logical system for LANL with the highest express power. Because of several serious disadvantages (the absence of formal de nitions of syntax and semantics of the system, the impossibility of specifying a complex deductive calculus, the impossibility of creating a fully automated practical implementation, etc.) an original logical system of source-oriented character will be created. Its ambition will be overcome mentioned disadvantages. Following the rst phase of the research, its capabilities will be tested and compared with existing solutions not only through exact logical proo ng, but also through its implementation of a semantic machine.
This work was supported by the following projects: { Faculty of Electrical Engineering and Informatics, Technical University of Kosice under the contract No. FEI-2018-59: Semantic Machine of SourceOriented Transparent Intensional Logic. { Slovak Research and Development Agency under the contract No. SK-AT2017-0012: Semantics technologies for computer science education.