Wyniki wyszukiwania - BazTech

1

Skolem’s Theorem in Coherent Logic

Bezem Marc, Coquand Thierry

Fundamenta Informaticae

|

2019

|

Vol. 170, nr 1-3

1--14

EN

We give a constructive proof of Skolem's Theorem for coherent logic and discuss several applications, including a negative answer to a question by Wraith.

2

A proof-theoretic approach to scope ambiguity in compositional vector space models

Wijnholds G. J.

Journal of Language Modelling

|

2018

|

Vol. 6, No. 2

261--286

EN

We investigate the extent to which compositional vector space models can be used to account for scope ambiguity in quantified sentences (of the form Every man loves some woman). Such sentences containing two quantifiers introduce two readings, a direct scope reading and an inverse scope reading. This ambiguity has been treated in a vector space model using bialgebras by Hedges and Sadrzadeh (2016) and Sadrzadeh (2016), though without an explanation of the mechanism by which the ambiguity arises. We combine a polarised focussed sequent calculus for the non-associative Lambek calculus NL, as described in Moortgat and Moot (2011), with the vector-based approach to quantifier scope ambiguity. In particular, we establish a procedure for obtaining a vector space model for quantifier scope ambiguity in a derivational way.

3

Proof-graphs: a Thorough Cycle Treatment, Normalization and Subformula Property

Alve G.V., Oliveira A.G.,de, Queiroz R., de

Fundamenta Informaticae

|

2011

|

Vol. 106, nr 2-4

119-147

EN

A normalization procedure is presented for a classical natural deduction (ND) proof system. This proof system, called N-Graphs, has a multiple conclusion proof structure, where cycles are allowed. With this, we have developed a thorough treatment of cycles, including cycles normalization via an algorithm. We also demonstrate the usefulness of the graphical framework of N-Graphs, where derivations are seen as digraphs. We use geometric perspective techniques to establish the normalization mechanism, thus giving a direct normalization proof. Moreover, the subformula and separation properties are determined.

4

A Semantic Analysis of a Logic for Pragmatics with Assertions, Obligations, and Causal Implication

Ranalter K.

Fundamenta Informaticae

|

2008

|

Vol. 84, nr 3-4

443-470

EN

One of the aims of a logic for pragmatics is to provide a logical framework that formalizes reasoning about speech acts. In this paper we investigate the semantics of a fragment of the logic for pragmatics proposed by Bellin and Dalla Pozza in "A pragmatic interpretation of substructural logics" (Feferman Festschrift, ASL Lecture Notes in Logic 15, 2002). The logic deals with acts of assertion and acts of obligation, and it incorporates a rule that relates acts of obligation to acts of assertion via a notion of causal implication. As our main result we show that the logic is sound and complete with respect to a class of algebraic, Kripke, and categorical models.

5

Investigating the Logical Aspects of the Pi-calculus

Bernard N.

Schedae Informaticae

|

2003

|

Vol. 12

57-66

EN

The relations between the p-calculus and logic have been less extensively studied than for the l-calculus. We give an account on what can be found in the literature, in two distinct directions: model-checking, and typing. We propose a Curry-Howard correspondence taking into account the dynamic properties of the p-calculus. This is a first presentation of a work in progress.

6

Graphs and Colorings for Answer Set Programming with Preferences

Konczak K., Schaub T., Linke T.

Fundamenta Informaticae

|

2003

|

Vol. 57, nr 2-4

393--421

EN

The integration of preferences into answer set programming constitutes an important practical device for distinguishing certain preferred answer sets from non-preferred ones. To this end, we elaborate upon rule dependency graphs and their colorings for characterizing different preference handling strategies found in the literature. We start from a characterization of (three types of) preferred answer sets in terms of totally colored dependency graphs. In particular, we demonstrate that this approach allows us to capture all three approaches to preferences in a uniform setting by means of the concept of a height function. In turn, we exemplarily develop an operational characterization of preferred answer sets in terms of operators on partial colorings for one particular strategy. In analogy to the notion of a derivation in proof theory, our operational characterization is expressed as a (non-deterministically formed) sequence of colorings, gradually turning an uncolored graph into a totally colored one.