|
|
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.
|
|
|
