18

**
University of Pennsylvania
Philadelphia, USA
**

**Scientific Sponsorship**
*Interest Group in Pure and Applied Logics (IGPL)*
*The Association for Logic, Language and Information (FoLLI)*
*Association for Symbolic Logic (ASL)*
*European Association for Theoretical Computer Science (EATCS)*
*European Association for Computer Science Logic (EACSL)*
*Sociedade Brasileira de Computação (SBC)*
*Sociedade Brasileira de Lógica (SBL)*

**Organisation**

*
Department of Mathematics, University of Pennsylvania, USA
Centro de Informática, Universidade Federal de Pernambuco, Brazil
*

*Streaming string transducers* dene (partial) functions from input strings to
output strings. A streaming string transducer makes a single pass through the
input string and uses a finite set of variables that range over strings from the
output alphabet. At every step, the transducer processes an input symbol, and
updates all the variables in parallel using assignments whose right-hand-sides are
concatenations of output symbols and variables with the restriction that a variable
can be used at most once in a right-hand-side expression. The expressiveness
of streaming string transducers coincides with the class of "regular" transduc-
tions that can be equivalently defined using two-way deterministic finite-state
transducers and using monadic second-order logic. The problems of checking
functional equivalence of two streaming transducers, and of checking whether
a streaming transducer satisfies pre/post verification conditions specified by finite automata, are solvable in Pspace. These decision procedures also generalize
to the model of streaming transducers over data strings|strings over symbols
tagged with data values over a potentially infinite data domain that supports
only the operations of equality and ordering. We identify a class of imperative
and a class of functional programs, manipulating lists of data items, which can
be effectively translated to such streaming data-string transducers. Our results
lead to algorithms for assertion checking and for checking functional equivalence
of two programs, written possibly in different programming styles, for commonly
used routines such as insert, delete, and reverse.

This talk is based on results reported in [2] and [1].

**References**

1. Alur, R., Cerny, P.: Expressiveness of streaming string transducers. In: *Proc.
30th FSTTCS*, pp. 1-12 (2010)

2. Alur, R., Cerny, P.: Streaming transducers for algorithmic verification of single-
pass list-processing programs. In: *Proc. 38th POPL*, pp. 599-610 (2011).

This invited talk will describe a formal logic for reasoning about security properties of network protocols with proof rules indicating exact security bounds that could be used to choose key lengths or other concrete security parameters. The soundness proof for this logic, a variant of previous versions of Protocol Composition Logic (PCL), shows that derivable properties are guaranteed in a standard cryptographic model of protocol execution and resource-bounded attack. We will discuss the general system and present example axioms for dig- ital signatures and random nonces, with concrete security properties based on concrete security of signature schemes and pseudorandom number generators (PRG). The quantitative formal logic supports first-order reasoning and reasoning about protocol invariants, taking exact security bounds into account. Proofs constructed in this logic also provide conventional asymptotic security guarantees because of the way that exact bounds accumulate in proofs. As an illustrative example producing exact bounds, we use the formal logic to prove an authentication property with exact bounds of a signature-based challenge-response protocol.

This talk presents joint work with Anupam Datta (Carnegie Mellon University), Joseph Y. Halpern (Cornell University), and Arnab Roy (IBM Thomas J. Watson Research Center).

**Acknowledgements.** This work was partially supported by the National Science Foundation,
the Air Force Oce of Scientific Research, and the Office ofNaval Research.

Over the last two years deep and unexpected connections have been discovered between constructive type theories and classical homotopy theory. These connections open a way to construct new foundations of mathematics alternative to the ZFC. These foundations promise to resolve several seemingly unconnected problems|provide a support for categorical and higher categorical arguments directly on the level of the language, make formalizations of usual mathematics much more concise and much better adapted to the use with existing proof assistants such as Coq and finally to provide a uniform way to approach constructive and "classical" mathematics. I will try to describe the basic construction of a model of constructive type theories which underlies these innovations and provide some demonstration on how this model is used to develop mathematics in Coq.

Research in logical semantics of natural language has extensively studied the functions denoted by expressions like
*each other*, *one another* or *mutually*. The common analysis takes such **reciprocal expressions** to denote
$\langle 1,2\rangle$ generalized quantifiers over a given domain $E$, i.e. relations between subsets of $E$ and binary relations over $E$.
One of the reoccurring problems has been that reciprocal expressions seem to denote different quantifiers in different sentences.
For instance, the reciprocal expression *each other* means the different quantifiers $Q_1$ and $Q_2\subseteq \wp(E)\times\wp(E^2)$ in
sentences (1) and (2), respectively.

(1) The girls know each other.

$Q_1 = \{\langle A,R\rangle : |A|\geq 2 \; \wedge \; \forall x,y \in A\,[x\not=y\rightarrow R(x,y)]\, \}$

(2) The girls are standing on each other.

$Q_2 = \{\langle A,R\rangle : |A|\geq 2 \; \wedge \; \forall x \in A\,\exists y\in A \, [x\not=y\wedge (R(x,y)\vee R(y,x))]\, \}$

Following previous work on reciprocals [1-4] I will suggest that the quantifier that a reciprocal expression denotes takes as
parameter certain logical/cognitive semantic properties of **relational concepts** -- intensions of two place predicates.
In simple cases this parametrization only involves familiar properties like asymmetry or acyclicity, cf. the relation *stand on* in (2).
However, in more complex cases, also preferences of use and other contextual parameters should be formally described as affecting the
logical semantics of reciprocity. The precise formalization of such parameters and their affects on the selection of reciprocal
quantifiers will be analyzed, based on recent joint work, logical as well as experimental, with Nir Kerem, Eva Poortman, Sivan Sabato
and Naama Friedmann.

**References**

[1] Dalrymple, M., Kanazawa, M., Kim, Y., Mchombo, S., Peters, S.: Reciprocal expressions and the concept of reciprocity.
*Linguistics and Philosophy* 21, 159--210 (1998).

[2] Kerem, N., Friedmann, N., Winter, Y.: Typicality effects and the logic of reciprocity. In: *Proceedings of SALT19 (Semantics and Linguistic Theory)*
(to appear).

[3] Sabato, S., Winter, Y.: From semantic restrictions to reciprocal meanings. In: *Proceedings of FG-MOL* (2005).

[4] Winter, Y.: Plural predication and the Strongest Meaning Hypothesis. *Journal of Semantics* 18, 333--365 (2001).

This paper analyses the classical automated reasoning problem---given a theory $\mathcal{T}$, a set $\mathcal{A}$ of ground atoms and a formula $\varphi$,
decide whether $(\mathcal{T}, \mathcal{A}) \models \varphi$---in the context of the \OWLT{} Web Ontology Language and ontology-based data access (OBDA).

In a typical OBDA scenario, $\mathcal{T}$ is an \OWLT{} `ontology' providing a user-oriented view of raw data $\mathcal{A}$, and
$\varphi(\vec{x})$ is a query with answer variables $\vec{x}$. Unlike classical automated reasoning, an important requirement for OBDA is that it
should scale to large amounts of data and preferably be as efficient as standard relational database management systems.

There are various ways of formalising this requirement, which give rise to different fragments of first-order logic suitable for OBDA.
For example, according to the \emph{query-rewriting approach} of [1], given $\mathcal{T}$, $\mathcal{A}$ and $\varphi(\vec{x})$,
one has to compute a new query $\varphi'(\vec{x})$, independently of $\mathcal{A}$, such that, for any tuple $\vec{a}$,
$(\mathcal{T}, \mathcal{A}) \models \varphi(\vec{a})$ iff $\mathcal{A} \models \varphi'(\vec{a})$. As a result, this approach can only be
applicable to the languages for which query-answering belongs to the class $\ACz$ for \emph{data complexity} (that is, if only $\mathcal{A}$
is regarded as input, whereas both $\mathcal{T}$ and $\varphi$ are regarded as fixed). In the \emph{combined approach} to OBDA [4,2],
given $\mathcal{T}$, $\mathcal{A}$ and $\varphi(\vec{x})$, one has to compute new (i) $\mathcal{A}'\supseteq \mathcal{A}$ in polynomial time in
$\mathcal{T}$ and $\mathcal{A}$, and (ii) $\varphi'(\vec{x})$ in polynomial tome in $\mathcal{T}$ and $\varphi$ such that, for any tuple $\vec{a}$,
$(\mathcal{T}, \mathcal{A}) \models \varphi(\vec{a})$ iff $\mathcal{A}' \models \varphi'(\vec{a})$.
The combined approach can be used for languages with polynomial query-answering.

One focus of this paper is on the fragments of first-order logic complying with such conditions imposed on OBDA.

Another focus is on the following problem: given theories $\mathcal{T}_1$, $\mathcal{T}_2$ and a signature $\Sigma$, decide whether, for all
$\mathcal{A}$ and $\varphi(\vec{x})$ formulated in the language of $\Sigma$, we have $(\mathcal{T}_1, \mathcal{A}) \models \varphi(\vec{a})$
iff $(\mathcal{T}_2, \mathcal{A}) \models \varphi(\vec{a})$ (that is: $\mathcal{T}_1$ and $\mathcal{T}_2$ give the same answers to any $\Sigma$-query
over the same $\Sigma$-data). In the \OWLT{} setting, an efficient solution to this problem would facilitate various stages of ontology developing and
maintenance such as ontology versioning, refining, reusing, or module extraction [3]

**References**

[1] Calvanese, D., De Giacomo, G., Lembo, D., Lenzerini, M., Rosati, R.: Tractable
reasoning and efficient query answering in description logics: The DL-Lite family.
*J. of Automated Reasoning* 39, 385{429 (2007).

[2] Kontchakov, R., Lutz, C., Toman, D.,Wolter, F., Zakharyaschev, M.: The combined
approach to query answering in DL-Lite. In: *KR* (2010)

[3] Kontchakov, R., Wolter, F., Zakharyaschev, M.: Logic-based ontology comparison
and module extraction, with an application to DL-Lite. *AI* 174, 1093-1141 (2010)

*Last modified: April 22, 12:04pm GMT-3.*