CafeOBJ is a new generation industrial strength algebraic specification language, which is a modern succesor of OBJ incorporating several new developments in algebraic specification theory and practice, most notably behavioural (concurrent) specification and rewriting logic.
CafeOBJ definition is rigorously based on a system of several logics, such as equational logic, rewriting logic, hidden algebra, and their combinations. We briefly survey the logical foundations of CafeOBJ including both the basic specification and the structured specification level by highlighting some novel theoretical contributions of CafeOBJ such as extra theory morphisms for institutions and the concept of behavioural coherence for operations. Then we present the current specification and verification methodologies with emphasis on the behavioural ones.  Finally, we concentrate on a component-based specification and verification methodology supporting high reusability of specification code but also reusability of verifications. This methodology provides a basis for a CafeOBJ developement tool under construction.
The presentation includes demonstrations of the CafeOBJ interpreter, compiler, and (web based) proof assistant.
 

ACLP is a system which combines abductive reasoning and constraint solving by integrating the framework of Abductive Logic Programming (ALP) with that of Constraint Logic Programming (CLP). In ACLP the role of abductive reasoning is that of providing an automatic reduction of the high-level problem representation and goals to lower level computational tasks of a general problem independent form. It thus provides a bridge between the high-level problem domain properties and domain-independent solving methods.
The ACLP framework has been applied to the problems of planning and scheduling in order to test its flexibility and computational effectiveness compared with the direct use of the (lower level) constraint solving framework of CLP on which this is built. These experiments provide evidence that the abductive framework of
ACLP does not compromise significantly the computational efficiency of the solutions thus indicating the computational viability of the framework for the development of flexible solutions to complex applications.
The ACLP framework is currently implemented on top of the ECLiPSe language of ECRC as a meta-interpreter using explicitly its low-level constraint solver that handles constraints over finite domains (integer and atomic elements).
 

Abductive Concept Learning is a learning framework that extends the one of Inductive Logic
Programming by considering both the background and the target theories as abductive theories and by adopting an abductive notion of entailment as the coverage relation. In this extended framework, it is possible to learn with incomplete background information about the training examples by exploiting the hypothetical reasoning of abduction. Moreover the possibility of making assumptions about one predicate while learning another is also useful for multiple predicate learning. We present two systems that learn in this extended framework:

• ACL: learns a new abductive theory starting from an abductive theory as background knowledge and positive and negative examples.
• M-ACL: is a specialization of the ACL system for the case of multiple predicate learning.