Topics
In the contemporary design of deduction systems there is a clearly
observable trend away from monolithic systems towards building integrated
tools. Thus, the vast combinatorial power of fully automatic theorem provers
might be opened for non-expert users through the interface of interactive
specification and verification tools. Also, real-world deduction problems
tend to be so complex that no single methodology is likely to be successful.
Although a high degree of maturity has been reached in various subfields
of automated deduction, the obstacles to integration are still
non-trivial and diverse. The aim of this workshop is to describe the
current state achieved in integration of deductive
systems.
Submissions are sought that describe ongoing or completed research in
the integration of deductive systems.
Investigations into theoretic alconcepts and calculi are solicited
as well as the exposition of systems and experimental
results. Areas of particular interest include but are not limited to:
-
combination of interactive with fully automated theorem provers
-
theorem provers that combine
-
different logics
-
different proof procedures
-
components on different levels
of expressiveness
-
theorem provers with non-deductive components (e.g. decision procedures,
model checking)
-
integrating theorem provers in other systems (e.g. in computer algebra
systems, systems for diagnosis, specification tools, etc.)