0-36th month.
"Definition of mathematical service. Modeling CAS and DSs as mathematical services. Identification of the architectural and functional requirements for turning CASs and DSs into open systems capable of using and/or delivering mathematical services."
ITC-IRST, Trento (Leader of the task):
Gilles Audemard
(young visiting researcher from University of Provence, France)
Piergiorgio Bertoli
(researcher)
Marco Bozzano
(researcher)
Alessandro Cimatti
(researcher)
Tommi Junttila (young
visiting researcher from Helsinki University of Technology, Finland)
Gavin Keighren (young visiting researcher from University of Edumburgh,
Scotland)
Veselin Kirov (young visiting researcher from Bulgaria)
Artur Kornilowicz,
(young visiting researcher from University of Bialystok, Poland)
Roberto Sebastiani
(assistant professor)
Stephan
Schulz (young visiting researcher visiting IRST, from TU Muenchen)
Daniel
Sheridan (young visiting researcher from University of Edimburgh)
Peter van Rossum
(young visiting researcher from the Netherlands)
University of Saarland -- USAAR:
Christoph Benzmueller
(assistant professor)
Jürgen Zimmer (PhD
student)
University of Edinburgh -- UED:
Alan Bundy
(professor)
Simon Colton (former
research
associate)
Jürgen Zimmer (young
visiting researcher from USAAR)
University of Karlsruhe -- UKA:
Jacques Calmet
(professor)
Research Institute for Symbolic Computation, University of Linz
--- RISC:
Olga Caprotti
Wolfgang
Windsteiger
University of Genova -- UNIGE:
Alessandro Armando
(assistant professor)
Luca Compagna (PhD
student)
Pasquale De Lucia
(PhD Student)
Enrico Giunchiglia
(Associate Professor)
Silvio Ranise (PhD
student)
Sorin Stratulat (young
visiting researcher from INRIA-Lorraine, Nancy, France)
Jürgen Zimmer (young
visiting researcher from USAAR)
Gilles Audemard (University of Provence). Young visiting
researcher of IRST (Trento) from 1/11/01 to 31/8/02.
Gilles' work focused on the analysis, design and implementation of efficient algorithms that combine algebraic decision procedures (mathematical solving & computing services) and logical reasoning capabilities (proving services), with the main goal of automatically verifying timed systems. In particular, he took part to the requirement analysis, design and implementation of MathSAT [16], a system combining the (high-performances) boolean reasoning capabilities of the SAT procedure SIM with the mathematical solving capability of a home-made decision procedure for linear arithmetic formulas over the reals. He has taken in charge the development of the resulting system.
He contributed to the development of the general framework (logical foundations and basic algorithms) for combining boolean decision procedures and mathematical solvers, and to the definition of the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration [15]. To this extent, his contribution focused mainly on the requirements for boolean decision procedures.
Luca Compagna (University of Genova). Young visiting
researcher of UED (Edinburgh) from 07/01 to 08/01.
Luca's work focussed on the design, development, and efficient integration of decision procedures in formula simplification. He has contributed to the development of the RDL theorem prover.
Artur Kornilowicz (University of Bialystok). Young visiting
researcher of IRST (Trento) from 16/07/01 to 30/06/02.
Artur's work focused on the design and implementation of efficient algorithms that automatically establish the satisfiability of a specific class of mathematical formulae, which can be used to model timed systems. The algorithms are designed in order to closely integrate as a Math-Solver module of MathSAT [16]. He has taken in charge the development of the Math-Solver module.
He also contributed to the development of the general framework for combining boolean decision procedures and mathematical solvers, and to the definition of the main requirements that boolean and mathematical solvers must fulfill in order to achieve the maximum benefits from their integration [15]. To this extent, his contribution focused mainly on the requirements for mathematical solvers.
Silvio Ranise (University of Genova). Young visiting researcher of USAAR (Saarbruecken) from 11/01 to 12/01.
Silvio has actively participated in the definition of the control component of OMRS (Open Mechanized Reasoning Systems). Silvio's work focused also on the definition of Constraint Contextual Rewriting. He has contributed to the development of the RDL theorem prover.
Jürgen Zimmer (University of Saarlandes). Young visiting researcher of UNIGE (Genova) from 01/01/01 to 09/07/01. Young visiting researcher of UED (Edinburgh) from 1/10/01 to 31/3/02.
Jürgen's work focused on the investigation of a possible use of the work done in the Semantic Web Community and in the Distributed AI community for the purpose of describing reasoning services. During his stay as a YVR in Edinburgh, Jürgen Zimmer investigated a possible use of the Web Service Description Language (WSDL) developed by the semantic web community, and agent capability description languages, such as the LARKS specification language and DAML+OIL for the specification of mathematical services. It turned out that WSDL is only suitable for describing interfaces of web services but not the semantics of a service. The specification language LARKS, however, combines a high expressivity with the ability to reason about service specifications. Further information can be found on the MathWeb site.Daniel Sheridan (School of Informatics, University of Edumburgh). Young visiting researcher of IRST (Trento) from 13/2/03 to 6/4/03.
Stephan worked on four main topics during his CALCULEMUS stay: Communication protocols for reasoning systems, improvements for first-order deduction systems, automated domain exploration, and decision procedures for fragments of first order logic. Most of his work at ICT/irst was on the last topic. He developed and implemented a robust and efficient congruence closure algorithm that forms the equational solver of the latest version of MathSat. The system makes MathSat into an efficient decision procedure for the logic of equality with uninterpreted function symbols (EUF) and plays an important role in reasoning about other theories. In fall 2003, Stephan attended the Fourth International Workshop on the Implementation of Logics (as an invited speaker) and LPAR-2004. In summer 2004, he presented a number of results obtained during his CALCULEMUS work at IJCAR-2004 and the IJCAR-Workshop on Empirically Successful First-Order Reasoning. He published the papers [28,29,30,31].Tommi Junttila (Helsinki University of Technology, Finland). Young visiting researcher of IRST (Trento) from 15/1/04 to 31/8/04.
Tommi's work focused on the analysis, design and implementation of efficient algorithms that combine algebraic decision procedures (mathematical solving) and logical reasoning capabilities (proving services). In particular, he took part to the requirement analysis, design and implementation of the new version of MathSAT [2], a system combining the (high-performance) boolean reasoning capabilities with the mathematical solving capability. His main contributions were the designing and implementing the top-level solver module and the preprocessor for non-clausal formulae in the new version of the MathSAT solver. The top-level solver extends the Minisat Boolean satisfiability checker developed at Chalmers University by interfacing it with the data structures representing non-Boolean formulae and with theory specific solvers such as one for the theory of equality with uninterpreted functions and one for linear and non-linear arithmetics. The preprocessor for non-clausal formulae enables one to use more natural and compact form for describing problems. The formulae are then translated to the special conjunctive normal form accepted by the top-level solver by a series of satisfiability preserving steps. In addition, he has contributed to the bounded model checker module of the NuSMV symbolic model checker. He has improved the Boolean circuit package in NuSMV so that it now produces more compact representations of problems. Furthermore, he has designed and implemented a module for incremental satisfiability checking in NuSMV. Based on this module, he has implemented the temporal induction algorithms described by Een and Sorensen in [23] and integrated incremental SAT solving also to bounded model checking of linear time temporal properties. During his stay in Trento he has participated in two conferences, the International Conference on Application of Concurrency to System Design (ACSD 2004) in Hamilton, Canada, June 2004 and 25th International Conference on Application and Theory of Petri Nets (ATPN 2004) in Bologna, Italy, June 2004. In these conferences, he presented new results concerning the symmetry reduction method for explicit state space anylysis obtained prior to the visit at IRST. The presented papers are [24][25] The conference trips were funded by IRST through the CALCULEMUS project.Peter van Rossum (The Netherlands). Young visiting researcher of IRST (Trento) from 15/1/04 to 31/8/04.
The focus of his work has been towards the constant improvement of the model checker NuSMV. Initially this involved working on increasing the functionality provided by the program, by means of allowing input files to be automatically run through external preprocessors. He also made the modifications necessary to integrate the improved RBC encodings which Tommi Junttila had provided. He has been involved in the revision of the user-manual and tutorial to reflect the changes made to NuSMV. The other main area of his work has been to investigate the boolean encoding methods used by NuSMV, with the aim of improving the solution times for SAT-based bounded model checking. Primarily, it has focused on reducing the size of the formula which is passed to the external SAT solver. He has also been involved in the testing and benchmarking of the new incremental algorithms which have been added to the latest version of NuSMV.
Alessandro Armando (UNIGE): The Control Component of OMRS
Wolfgang Windsteiger (RISC): Definition of Mathematical Service
Olga Caprotti (RISC): The "MathBroker" Project at RISC
Jürgen Zimmer (USAAR): Description of Reasoning Services - A Progress Report
Alessandro Armando (UNIGE): Constraint Contextual Rewriting
Corrado Giromini (UNIGE): Logic Broker Architecture
Roberto Sebastiani (ITC-IRST): Integrating Boolean and Mathematical Solving. Foundations and Requirements
Sorin Stratulat: Incorporating Decision Procedures into Implicit Induction
Roberto Sebastiani chaired the session.
University of Genova, represented by Alessandro Armando, presented
the OMRS (Open Mechanized Reasoning Systems) specification framework.
An OMRS specification consists of three components: the logic
component, the control component, and the interaction component. In
this talk, Alessandro Armando focused on the control level and proposes
to specify the control component by first adding control knowledge to
the data structures representing the logic by means of annotations, and
then by specifying proof strategies via tactics. To show the adequacy
of the approach he presents and discusses a structured specification of
the top-level inference strategy of NQTHM as a set of cooperating
specialized reasoning modules (see [5,8]).
The slides of the presentation are available here.
RISC, represented by Wolfgang Windsteiger, proposes the following
definition of a service: a service is a set of implementations
running on a particular machine. An implementation is a particular
realization of an algorithm as executable software, possibly with
additional constraints on the input and additional possibilities for
the output.
In this view (see [6,7])
, Mathematical Services can be subdivided into "Proving
Services", "Solving Services", or "Computing Services". The process of
developing mathematical theories usually requires a great deal of
interaction between "Proving", "Solving", and "Computing". Therefore,
in a computer-supported mathematical environment, the support of
communication and interaction between these categories of mathematical
services is indispensable for tackling "real problems in mathematics".
The interaction between "Proving", "Solving",
and "Computing" may take place on at least two levels, called "coarse
grain interaction" and "fine grain interaction". An example of coarsely
grained interaction can be seen
when,
during the development of a mathematical theory, one has to prove
theorems. An example of finely grained interaction can be seen when,
during a proof, it becomes necessary to simplify expressions by
computation or to find instances of quantified formulae by solving.
RISC, represented by Olga Caprotti,
presents the MathBroker, a framework for brokering mathematical
services distributed among networked servers. MathBroker's mathematical
service description language extends WSDL, the web service description
language. Servers register their problem solving capabilities,
expressed in this language, to a ``semantic broker''. Clients submit
corresponding task descriptions to the semantic broker. The broker (in
cooperation with a deduction system) determines the suitable services
and returns them to the client for invocation. This mechanism thus
hides from the client the actual implementation of mathematical
services and focuses on the semantical aspects.
The slides of the presentation are available here.
USAAR, represented by Jürgen Zimmer, presents an ongoing work on
formal description of reasoning services. Reasoning service
descriptions are crucial for the MathWeb-SB in two ways: for
the online access of reasoning services and for a further
agentification of the MathWeb-SB. USAAR is investigating a possible use
of the work done in the Semantic Web Community and in the Distributed
AI community for their purposes. In the talk, Jürgen Zimmer presented
the capability description language LARKS and
described how reasoning services could be described using LARKS.
This work on the description of reasoning services (Mathematical
Services) addresses the first two points of the task specification. The
capability description language LARKS offers the means to describe the
semantics of a service. The description of the actual functionality of
a service (besides the specification of the input and output
parameters) is crucial for efficient brokering of services and
matchmaking between service advertisements and requests. USAAR tried to
model the CAS Maple and the DS Lambda-Clam as Mathematical Services
using the description language LARKS with their own ontology. It turned
out that modeling DSs is much easier than modeling CASs because the
problem solving knowledge of DSs is represented more explicitely while
CASs do not allow external access to the knowledge embedded in their
algorithms.
The slides of the presentation are available here.
University of Genova, represented by Alessandro Armando, presents a
work focusing on effective integration of decision procedures in
formula simplification, a fundamental problem in mechanical
verification. They address the problem by proposing a general pattern
of interaction between rewriting and decision procedures and by
providing an account of such a pattern of interaction which is precise
and concise at the same time. The first step amounts to a
generalization of contextual rewriting which allows the available
decision procedure to access and manipulate the rewriting context. They
call this generalized form of contextual rewriting Constraint
Contextual Rewriting (CCR for short). The second step amounts to
providing a rule-based presentation of CCR which is modular,
declarative, and formal at the same time. This allows them to give a
rigorous account of CCR and to formally state and prove its soundness
and termination (see [2,4]).
As deliverables they propose:
IRST, represented by Roberto Sebastiani, presents the mathematical
and logical foundations and basic algorithms for integrating boolean
reasoning and mathematical solving services (see [1]).
Algorithms are based on the DPLL algorithm, which is extended by
mathematical reasoner. The paper regards the satisfiability of
math-formulae, i.e., a boolean combination of propositional variables
and linear mathematical relations over real variables. It specifies
mandatory requirements (termination, correctness, completness) and
efficiency requirements (time efficiency, polynomial memory, ability to
produce failure information (conflict sets), ability to produce and to
propagate success information (consequence of previous reasoning),
incrementality) for such services.
The slides of the presentation are available here.
At the end of session a brainstorming over Task 1.2 took place; the following issues have been raised: