Campus Event Calendar
Event Entry
What and Who
On Properties of Local Theory Extensions: Hierarchical and Modular Reasoning, Interpolation
Viorica Sofronie-Stokkermans
MPI, RG1
Talk
AG 1, AG 2, AG 3, AG 4, AG 5, SWS
AG Audience
English
Note: We use this to send email in the morning.
Date, Time and Location
Friday, 27 October 2006
11:00
30 Minutes
E1 4
Rotunda 6th floor
Saarbrücken
Abstract
Many problems in mathematics and computer science - in
particular, problems involving reasoning in and about
complex systems - can be reduced to proving the satisfiability
of conjunctions of literals modulo some background theory.
This theory can be a standard theory, the extension of a base
theory with additional functions, or a combination of theories.
It is therefore extremely important to find methods for efficient
reasoning in extensions and combinations of theories.
In this talk we consider a special type of theory extensions,
which we call local, where hierarchic reasoning - in which a
theorem prover for the base theory is used as a ``black box''
- is possible. We give several examples of theories important
for computer science or mathematics which are local extensions
of a base theory. We show that the decidability (and complexity)
of the universal fragment of a local theory extension can be
expressed in terms of the decidability (resp. complexity) of
a suitable fragment of the base theory. We also identify
possibilities of modular reasoning in combinations of local
theory extensions, as well as possibilities of obtaining
interpolants in a hierarchical manner, and discuss applications
in verification (especially in abstraction refinement) and in
knowledge representation.
particular, problems involving reasoning in and about
complex systems - can be reduced to proving the satisfiability
of conjunctions of literals modulo some background theory.
This theory can be a standard theory, the extension of a base
theory with additional functions, or a combination of theories.
It is therefore extremely important to find methods for efficient
reasoning in extensions and combinations of theories.
In this talk we consider a special type of theory extensions,
which we call local, where hierarchic reasoning - in which a
theorem prover for the base theory is used as a ``black box''
- is possible. We give several examples of theories important
for computer science or mathematics which are local extensions
of a base theory. We show that the decidability (and complexity)
of the universal fragment of a local theory extension can be
expressed in terms of the decidability (resp. complexity) of
a suitable fragment of the base theory. We also identify
possibilities of modular reasoning in combinations of local
theory extensions, as well as possibilities of obtaining
interpolants in a hierarchical manner, and discuss applications
in verification (especially in abstraction refinement) and in
knowledge representation.
Contact
Roxane Wetzel
-900
--email hidden
passcode not visible
logged in users only
Roxane Wetzel, 10/25/2006 11:36 -- Created document.