Keynote Speakers

ISAIM 2010 features three distinguished invited speakers:

Larry Manevitz University of Haifa, Israel
    Windows on the Mind: Some recent aspects of modeling and pattern recognition of cognition
Recently modeling techniques combined with machine learning have helped elucidate various aspects on Cognition. In this talk, we will illustrate this with some recent examples; such as modeling human reading, temporal based neurons, and memory models.

If time permits we may also talk about some recent technical developments in one class machine learning techniques that allow the classification of cognitive states from purely physiological signals (i.e. "reading the mind").

Warren Hunt University of Texas, Austin, USA
    Using Mathematics on an Industrial Scale
We describe our approach for analyzing commercial microprocessor designs by using the ACL2 theorem-proving system. Our approach involves deeply embedding a hardware description language (HDL) within the ACL2 logic, and then translating commercial designs into our HDL. We also use the ACL2 logic to specify desired properties, and we mechanically check such properties using the ACL2 theorem-proving system.

We demonstrate our approach through its use on VIA's X86-compatible Nano microprocessor. We translate the Nano's 570,000-line design description into our formal HDL, which provides a mathematical model of the design. We use mathematical techniques, implemented within the ACL2 system, to mechanically verify or refute asserted properties.

Georg Gottlob St. Anne's College, Oxford, UK
    Datalog±: A Unified Approach to Ontologies and Integrity Constraints
We report on a recently introduced family of expressive extensions of Datalog, called Datalog±, which is a new framework for representing ontological axioms in form of integrity constraints, and for query answering under such constraints. Datalog± is derived from Datalog by allowing existentially quantified variables in rule heads, and by enforcing suitable properties in rule bodies, to ensure decidable and efficient query answering. We first present different languages in the Datalog family, providing tight complexity bounds for all cases but one (where we have a low complexity AC0 upper bound). We then show that such languages are general enough to capture the most common tractable ontology languages. In particular, we show that the DL-Lite family of description logics and F-Logic Lite are expressible in Datalog±. We finally show how stratified negation can be added to Datalog while keeping ontology querying tractable in the data complexity. Datalog± is a natural and very general framework that can be successfully employed in different contexts such as data integration and exchange. This survey mainly summarizes two recent papers. This talk reports about joint work with Andrea Calì. Michael Kifer, and Thomas Lukasiewicz.

Last updated: December 7, 2009.