Author: mar08022

Computational Cognitive Modeling for Syntax and Semantics

Adrian Brasoveanu

I introduce a typical experimental task in psycholinguisticsself—paced reading—and show how to build end-to-end simulations of a human participant in such an experiment; end-to-end means that we model visual and motor processes together with specifically linguistic processes (syntactic and semantic parsing) in a complete model of the experimental task. The model embeds theoretical hypotheses about linguistic representations and parsing processes in an independently motivated cognitive architecture (ACT-R). In turn, the resulting cognitive models can be embedded in Bayesian models to fit them to experimental data, estimate their parameters and perform quantitative model comparison for qualitative theories.

Unveiling the constructive core of classical theories

Sara Negri

Unveiling the constructive core of classical theories: A contribution to 90 years of Glivenko’s theorem

Glivenko’s well known result of 1929 established that a negated propositional formula provable in classical logic is even provable intuitionistically. Similar later transfers from classical to intuitionistic provability therefore fall under the nomenclature of Glivenko-style results: these are results about classes of formulas for which classical provability yields intuitionistic provability. The interest in isolating such classes lies in the fact that it may be easier to prove theorems by the use of classical rather than intuitionistic logic. Further, since a proof in intuitionistic logic can be associated to a lambda term and thus obtain a computational meaning, such results have more recently been gathered together under the conceptual umbrella “computational content of classical theories.” They also belong to a more general shift of perspective in foundations: rather than developing constructive mathematics separately, as in Brouwer’s program, one studies which parts of classical mathematics can be directly translated into constructive terms.

We shall survey how Glivenko-style results can be easily obtained by the choice of suitable sequent calculi for classical and intuitionistic logic, by the conversion of axioms into inference rules, and by the procedure of geometrization of first order logic.