The role of medial parieto occipital cortex in visuospatial attention and reach planning: electrophysiological studies in human and non-human primates

We usually perform actions in a dynamic environment and changes in the location of a target for an upcoming action require both covert shifts of attention and motor planning update. In this study we tested whether, similarly to oculomotor areas that provide signals for overt and covert attention shifts, covert attention shifts modulate activity in cortical area V6A, which provides a bridge between visual signals and arm-motor control. We performed single cell recordings in monkeys trained to fixate straight-ahead while shifting attention outward to a peripheral cue and inward again to the fixation point. We found that neurons in V6A are influenced by spatial attention demonstrating that visual, motor, and attentional responses can occur in combination in single neurons of V6A. This modulation in an area primarily involved in visuo-motor transformation for reaching suggests that also reach-related regions could directly contribute in the shifts of spatial attention necessary to plan and control goal-directed arm movements. Moreover, to test whether V6A is causally involved in these processes, we have performed a human study using on-line repetitive transcranial magnetic stimulation over the putative human V6A (pV6A) during an attention and a reaching task requiring covert shifts of attention and reaching movements towards cued targets in space. We demonstrate that the pV6A is causally involved in attention reorienting to target detection and that this process interferes with the execution of reaching movements towards unattended targets. The current findings suggest the direct involvement of the action-related dorso-medial visual stream in attentional processes, and a more specific role of V6A in attention reorienting. Therefore, we propose that attention signals are used by the V6A to rapidly update the current motor plan or the ongoing action when a behaviorally relevant object unexpectedly appears at an unattended location.

Relative influence of gaze and static arm position in the Superior Parietal Lobule of the macaque monkey during reaching

The superior parietal lobule (SPL) of macaques is classically described as an associative cortex implicated in visuospatial perception, planning and control of reaching and grasping movements (De Vitis et al., 2019; Galletti et al., 2003, 2018, 2022; Fattori et al., 2017; Hadjidimitrakis et al., 2015). These processes are the result of the integration of signals related to different sensory modalities. During a goal-directed action, eye and limb information are combined to ensure that the hand is transported at the gazed target location and the arm is maintained steady in the final position. The SPL areas V6A, PEc and PE contain cells sensitive to the direction of gaze and limb position but less is known about the degree of independent encoding of these signals. In this thesis, we evaluated the influence of eye and arm position information upon single neuron activity of areas V6A, PEc and PE during the holding period after the execution of arm reaching movement, when the gaze and hand are both still at the reach target. Two male macaques (Macaca fascicularis) performed a reaching task while single unit activity was recorded from areas V6A, PEc and PE. We found that neurons in all these areas were modulated by eye and static arm positions with a joint encoding of gaze and somatosensory signals in V6A and PEc and a mostly separate processing of the two signals in PE. The elaboration of this information reflects the functional gradient found in the SPL with the caudal sector characterized by visuo-somatic properties in comparison to the rostral sector dominated by somatosensory signals. This evidence well agree also with the recent reallocation of areas V6A and PEc in Brodmann’s area 7 depending on their similar structural and functional features with respect to PE belonging to Brodmann’s area 5 (Gamberini et al., 2020).

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Induction of Hebbian associative plasticity through paired non-invasive brain stimulation of premotor-motor areas to elucidate the network's functional role

The ventral premotor cortex (PMv) is believed to play a pivotal role in a multitude of visuomotor behaviors, such as sensory-guided goal-directed visuomotor transformations, arbitrary visuomotor mapping, and hyper-learnt visuomotor associations underlying automatic imitative tendencies. All these functions are likely carried out through the copious projections connecting PMv to the primary motor cortex (M1). Yet, causal evidence investigating the functional relevance of the PMv-M1 network remains elusive and scarce. In the studies reported in this thesis we addressed this issue using a transcranial magnetic stimulation (TMS) protocol called cortico-cortical paired associative stimulation (ccPAS), which relies on multisite stimulation to induce Hebbian spike-timing dependent plasticity (STDP) by repeatedly stimulating the pathway connecting two target areas to manipulate their connectivity. Firstly, we show that ccPAS protocols informed by both short- and long-latency PMv-M1 interactions effectively modulate connectivity between the two nodes. Then, by pre-activating the network to apply ccPAS in a state-dependent manner, we were able to selectively target specific functional visuo-motor pathways, demonstrating the relevance of PMv-M1 connectivity to arbitrary visuomotor mapping. Subsequently, we addressed the PMv-to-M1 role in automatic imitation, and demonstrated that its connectivity manipulation has a corresponding impact on automatic imitative tendencies. Finally, by combining dual-coil TMS connectivity assessments and ccPAS in young and elderly individuals, we traced effective connectivity of premotor-motor networks and tested their plasticity and relevance to manual dexterity and force in healthy ageing. Our findings provide unprecedent causal evidence of the functional role of the PMv-to-M1 network in young and elderly individuals. The studies presented in this thesis suggest that ccPAS can effectively modulate the strength of connectivity between targeted areas, and coherently manipulate a networks’ behavioral output. Results open new research prospects into the causal role of cortico-cortical connectivity, and provide necessary information to the development of clinical interventions based on connectivity manipulation.