Campus Event Calendar
Event Entry
What and Who
Local Reasoning is Easy: On Hierarchic and Modular Therorem Proving
Dr. Viorica Sofronie-Stokkermans
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 3 November 2005
13:00
-- Not specified --
45 - FR 6.2 (E1 3)
016
Saarbrücken
Abstract
In the quest of identifying theories for which reasoning can be
done fast, Givan and McAllester introduced in 1992 the notion of
a local inference system. A local theory is a set of Horn clauses
$K$ with the property that if a ground Horn clause $C$ is provable
from $K$ then it can be proved ``locally'', by only using those
ground instances of $K$ in which all terms are subterms of ground
terms in either $K$ of $C$. For local theories, validity of ground
Horn clauses can be checked in polynomial time.
However, many theories which occur in computer science or mathematics
cannot be expressed simply as a set of (Horn) clauses. In addition,
one often has to consider extensions of a base theory by means of
additional function symbols (free, monotone, or recursively defined)
or even combinations of theories.
We will here address the problem of reasoning in extensions of theories
(and combinations thereof). We show that for a special type of extensions
of a base theory, which we call local, hierarchical reasoning, in which
a theorem prover for the base theory is used as a `black box', is possible.
Many theories important for computer science or mathematics are local
extensions of a base theory. Some examples are:
- theories of data structures, e.g. theories of lists or arrays,
- theories of constructors and selectors (important in program
verification, but also in cryptography),
- theories of monotone functions over an ordered domain
(applications in knowledge representation, or in verification),
- theories of (monotone) functions satisfying certain boundedness
conditions (relevant e.g. in the parametric verification of
real-time or hybrid systems),
done fast, Givan and McAllester introduced in 1992 the notion of
a local inference system. A local theory is a set of Horn clauses
$K$ with the property that if a ground Horn clause $C$ is provable
from $K$ then it can be proved ``locally'', by only using those
ground instances of $K$ in which all terms are subterms of ground
terms in either $K$ of $C$. For local theories, validity of ground
Horn clauses can be checked in polynomial time.
However, many theories which occur in computer science or mathematics
cannot be expressed simply as a set of (Horn) clauses. In addition,
one often has to consider extensions of a base theory by means of
additional function symbols (free, monotone, or recursively defined)
or even combinations of theories.
We will here address the problem of reasoning in extensions of theories
(and combinations thereof). We show that for a special type of extensions
of a base theory, which we call local, hierarchical reasoning, in which
a theorem prover for the base theory is used as a `black box', is possible.
Many theories important for computer science or mathematics are local
extensions of a base theory. Some examples are:
- theories of data structures, e.g. theories of lists or arrays,
- theories of constructors and selectors (important in program
verification, but also in cryptography),
- theories of monotone functions over an ordered domain
(applications in knowledge representation, or in verification),
- theories of (monotone) functions satisfying certain boundedness
conditions (relevant e.g. in the parametric verification of
real-time or hybrid systems),
- theories of mathematics, e.g. the theory of functions satisfying
the Lipschitz conditions at a given point.
We identify situations in which, for an extension ${\cal T}_1$ of a
theory ${\cal T}_0$, the decidability (and complexity) of the universal
theory of ${\cal T}_1$ can be expressed in terms of the decidability (resp.
complexity) of suitable fragments of the theory ${\cal T}_0$ (universal or
$\forall \exists$). We will also briefly discuss combinations of local
theory extensions, and possibilities of modular reasoning.
Contact
--email hidden
passcode not visible
logged in users only
Veronika Weinand, 10/28/2005 16:34
Veronika Weinand, 10/28/2005 12:30
Veronika Weinand, 10/19/2005 13:11
Veronika Weinand, 10/19/2005 13:08 -- Created document.
Veronika Weinand, 10/28/2005 12:30
Veronika Weinand, 10/19/2005 13:11
Veronika Weinand, 10/19/2005 13:08 -- Created document.