eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-09
9411
1
18
10.4230/DagSemProc.09411.1
article
09411 Abstracts Collection – Interaction versus Automation: The two Faces of Deduction
Ball, Thomas
Giesl, Jürgen
Hähnle, Reiner
Nipkow, Tobias
From 04.10. to 09.10.2009, the Dagstuhl Seminar 09411
``Interaction versus Automation: The two Faces of Deduction'' was held
in Schloss Dagstuhl~--~Leibniz Center for Informatics.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar as well as abstracts of
seminar results and ideas are put together in this paper. The first section
describes the seminar topics and goals in general.
Links to extended abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09411/DagSemProc.09411.1/DagSemProc.09411.1.pdf
Formal Logic
Deduction
Artificial Intelligence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-09
9411
1
4
10.4230/DagSemProc.09411.2
article
09411 Executive Summary – Interaction versus Automation: The two Faces of Deductions
Ball, Thomas
Giesl, Jürgen
Hähnle, Reiner
Nipkow, Tobias
This seminar was the ninth in the series of the
Dagstuhl "Deduction" seminars held biennially since 1993. Its goal
was to bring together the closely related but
unnecessarily disjoint communities of researchers working in
interactive and automatic program
verification.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09411/DagSemProc.09411.2/DagSemProc.09411.2.pdf
Formal Logic
Deduction
Artificial Intelligence
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-09
9411
1
33
10.4230/DagSemProc.09411.3
article
Automated reasoning in extensions of theories of constructors with recursively defined functions and homomorphisms
Sofronie-Stokkermans, Viorica
We study possibilities of reasoning about extensions of base theories
with functions which satisfy certain recursion and homomorphism
properties. Our focus is on emphasizing possibilities of hierarchical
and modular reasoning in such extensions and combinations thereof.
\begin{itemize}
item[(1)] We show that the theory of absolutely free constructors is local,
and locality is preserved also in the presence of selectors. These results are
consistent with existing decision procedures for this theory (e.g. by Oppen).
item[(2)] We show that, under certain assumptions, extensions of the theory of
absolutely free constructors with functions satisfying a certain type of recursion axioms
satisfy locality properties, and show that for functions with values in an ordered domain
we can combine recursive definitions with boundedness axioms without sacrificing locality.
We also address the problem of only considering models whose data part is
the {em initial} term algebra of such theories.
item[(3)] We analyze conditions which ensure that similar results can be obtained
if we relax some assumptions about the absolute freeness of the underlying
theory of data types, and illustrate the ideas on an example from cryptography.
end{itemize}
The locality results we establish allow us to reduce the task of reasoning about the
class of recursive functions we consider to reasoning in the underlying theory of
data structures (possibly combined with the theories associated with
the co-domains of the recursive functions).
As a by-product, the methods we use provide a possibility of presenting in a different light
(and in a different form) locality phenomena studied in cryp-to-gra-phy; we believe that
they will allow to better separate rewriting from proving, and thus to give simpler proofs.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09411/DagSemProc.09411.3/DagSemProc.09411.3.pdf
Decision procedures
recursive datatypes
recursive functions
homomorphisms
verification
cryptography
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-09
9411
1
4
10.4230/DagSemProc.09411.4
article
Inductive Theorem Proving meets Dependency Pairs
Swiderski, Stephan
Parting, Michael
Giesl, Jürgen
Fuhs, Carsten
Schneider-Kamp, Peter
Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for TRS termination with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09411/DagSemProc.09411.4/DagSemProc.09411.4.pdf
Termination
Term Rewriting
Dependency Pairs
Inductive Theorem Proving
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2010-03-09
9411
1
4
10.4230/DagSemProc.09411.5
article
Termination of Integer Term Rewriting
Fuhs, Carsten
Giesl, Jürgen
Plücker, Martin
Schneider-Kamp, Peter
Falke, Stephan
Recently, techniques and tools from term rewriting have been successfully applied to prove termination automatically for different programming languages. The advantage of rewrite techniques is that they are very powerful for algorithms on user-defined data structures. But in contrast to techniques for termination analysis of imperative programs, the drawback of rewrite techniques is that they do not support data structures like integer numbers which are pre-defined in almost all programming languages.
To solve this problem, we extend term rewriting by built-in integers and adapt the dependency pair framework to prove termination of integer term
rewriting automatically. Our experiments show that this indeed combines the power of rewrite techniques on user-defined data types with a powerful treatment of pre-defined integers.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol09411/DagSemProc.09411.5/DagSemProc.09411.5.pdf
Termination analysis
integers
term rewriting
dependency pairs