She first worked on some problems related to pattern recognition.
She worked on programming language semantics, program properties and their automatic proofs. She defined a semantics for PASCAL in LCF (Logic for Computable Functions) and machine checked several proofs of (nontrivial) properties.
She designed and implemented a theorem prover named PPC, Pisa Proof Checker; published some papers describing the (object oriented) programming paradigm used in its development, and its evaluator (an interpreter for the full lambda calculus).
She participated and contributed to the development and use of Wehyrauch's FOL system.
She did work in office automation, personal computing and text processing. She contributed to the first installation of TEX on a IBM machine in Italy and developed an environment similar to Latex.
She has investigated on the advantages of the use of meta-level knowledge in AI systems, both to control search and to do reasoning about reasoning in multi-agent systems.
In addition to some work in the area of Logic Programming and data bases, she carried on some experiments of application of Artificial Intelligence techniques to the development of Expert Systems for medical diagnosis; she has also done some work in Intelligent Tutorins Systems, both for supporting the learning of scientific disciplines, and of English as a second language for Italians.
She has done some work on nonmonotonic reasoning. Her interests have spanned from the characterization of default proofs, to tableau systems for default logic, to modal characterizations of defaul logic and definability of concepts of natural kinds.
She has more recently started projects on Cognitive Robotics, AI techniques applied to Security, and AI Planning.